Modeling and Verifying Timed Event-Based Systems

چکیده مقاله

A part of large scale distributed and heterogeneous systems are event-based in which temporal properties play a critical role. In this paper, considering the temporal properties we first present a semi-formal based specification model using UML statecharts and then address the conversion of this model to formal one called timed automata. Next, we deal with verification of properties stated in Timed Computation Tree Logic (TCTL) formulas in the automata. By proposing a case study, we show the application of our method.