Automatic compositional verification of timed systems

• Main Authors: LIN, Shang-Wei, LIU, Yang, SUN, Jun, DONG, Jin Song, ANDRÉ, Étienne
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2012
• Subjects: Model Check; Proof Rule; Monolithic Approach; State Space Explosion Problem; UPPAAL Model; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5016; https://ink.library.smu.edu.sg/context/sis_research/article/6019/viewcontent/automatic_compo.pdf
• Institution: Singapore Management University

Specification and verification of real-time systems are important research topics with crucial applications; however, the so-called state space explosion problem often prevents model checking to be used in practice for large systems. In this work, we present a self-contained toolkit to analyze real-time systems specified using event-recording automata (ERAs), which supports system modeling, animated simulation, and fully automatic compositional verification based on learning techniques. Experimental results show that our tool outperforms the state-of-the-art timed model checker.