Modeling and Verifying Timed Event-Based Architectures

چکیده مقاله

Nowadays, large scale distributed and heterogeneous systems are increasingly developed using event-based architectures and in many of them, time plays an important and often a critical role. Loosely coupled feature can help us to add new components to the model without any reconfiguration. Hence, it is desirable to model and check the behavior of these architectures. In this paper, we present an approach to specify and verify timed event-based system using UPPAAL. Publish and subscribe events have been modeled by synchronization channels and components defined by timed automatons. Moreover, the bathroom problem as an example is introduced by means of UML state chart diagrams. Then we present its timed automatons in order to help designers to find the suitable conversion between these two models. As modeling per se is not enough, Timed Computation Tree Logic (TCTL) formulas are used to define the desired properties and verified them by UPPAAL. Finally, we verify some properties on the bathroom model