ﻻ يوجد ملخص باللغة العربية
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 to specify such assurances in terms of (legally binding) contracts between a service provider and a customer. On the other hand, formal methods for verification of probabilistic real-time behavior have reached a level of expressiveness and efficiency which allows to apply them in real-world scenarios. In this paper, we suggest to employ the recently introduced model of Interval Probabilistic Timed Automata (IPTA) for formal verification of QoS properties of service-oriented systems. Specifically, we show that IPTA in contrast to Probabilistic Timed Automata (PTA) are able to capture the guarantees specified in SLAs directly. A particular challenge in the analysis of IPTA is the fact that their naive semantics usually yields an infinite set of states and infinitely-branching transitions. However, using symbolic representations, IPTA can be analyzed rather efficiently. We have developed the first implementation of an IPTA model checker by extending the PRISM tool and show that model checking IPTA is only slightly more expensive than model checking comparable PTA.
Reliability, longevity, availability, and deadline guarantees are the four most important metrics to measure the QoS of long-running safety-critical real-time applications. Software aging is one of the major factors that impact the safety of long-run
Today we see the use of the Internet of Things (IoT) in various application domains such as healthcare, smart homes, smart cars, and smart-x applications in smart cities. The number of applications based on IoT and cloud computing is projected to inc
Providing compact and understandable counterexamples for violated system properties is an essential task in model checking. Existing works on counterexamples for probabilistic systems so far computed either a large set of system runs or a subset of t
The prevailing net-centric environment demands and enables modeling and simulation to combine efforts from numerous disciplines. Software techniques and methodology, in particular service-oriented architecture, provide such an opportunity. Service-or
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