Analyzing Hierarchical Complex Real-Time Systems

Specification and verification of real-time systems are important research topics which have practical implications. In this paper, the authors present a self-contained toolkit to analyze real-time systems, which supports system modeling, animated simulation and automatic verification (based on advanced model checking techniques like dynamic zone abstraction). In this tool, they adopt an event-based modeling language for describing real-time systems with hierarchical structure. Experiments show that their tool has compatible performance with the state-of-the-art verifiers, and complement them with additional capabilities like LTL model checking, refinement checking.