Title :
Simulation and verification tool for hierarchical real-time systems
Author :
Sebestyénová, J.
Author_Institution :
Inst. of Informatics, Slovak Acad. of Sci., Bratislava, Slovakia
Abstract :
The computerized tool for statecharts based modeling and simulation of reactive systems with timing constraints is described in the paper. GUI enables to draw and edit the statecharts, and to specify the required behavior of the system. Useful types of properties, such as state reachability, safety, and response, can be specified and verified. The model-checking algorithm for statecharts verification works without constructing the flat state-transition graph. If the required property does not hold in the system, the counter-example can be found without searching the whole state space.
Keywords :
C++ language; digital simulation; formal verification; graphical user interfaces; object-oriented programming; real-time systems; GUI; computerized tool; hierarchical real-time systems verification tool; model-checking algorithm; reactive system simulation; state reachability; state-transition graph; statecharts based modeling; statecharts verification; timing constraints; Automata; Communication system control; Computational modeling; Computer simulation; Graphical user interfaces; Informatics; Real time systems; Safety; State-space methods; Timing;
Conference_Titel :
Engineering of Computer-Based Systems, 2004. Proceedings. 11th IEEE International Conference and Workshop on the
Print_ISBN :
0-7695-2125-8
DOI :
10.1109/ECBS.2004.1316707
