ﻻ يوجد ملخص باللغة العربية
The timed-based automata model, introduced by Alur and Dill, provides a useful formalism for describing real-time systems. Over the last two decades, several dense-time model checking tools have been developed based on that model. The paper considers the verification of real-time distributed commit protocols using dense-time model checking technology. More precisely, we model and verify the well-known timed two phase commit protocol in three different state-of-the-art real-time model checkers: UPPAAL, Rabbit, and RED, and compare the results.
Formal software verification techniques are widely used to specify and prove the functional correctness of programs. However, nonfunctional properties such as time complexity are usually carried out with pen and paper. Inefficient code in terms of ti
The assurance of quality of service properties is an important aspect of service-oriented software engineering. Notations for so-called service level agreements (SLAs), such as the Web Service Level Agreement (WSLA) language, provide a formal syntax
Artificial Neural Networks (ANNs) are being deployed for an increasing number of safety-critical applications, including autonomous cars and medical diagnosis. However, concerns about their reliability have been raised due to their black-box nature a
Avionics is one kind of domain where prevention prevails. Nonetheless fails occur. Sometimes due to pilot misreacting, flooded in information. Sometimes information itself would be better verified than trusted. To avoid some kind of failure, it has b
Requirements engineering is a key phase in the development process. Ensuring that requirements are consistent is essential so that they do not conflict and admit implementations. We consider the formal verification of rt-consistency, which imposes th