Verifying stateful timed CSP using implicit clocks and zone abstraction

• Main Authors: SUN, Jun, LIU, Yang, DONG, Jin Song, ZHANG, Xian
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2009
• Subjects: Model Check; Transition System; Operational Semantic; Label Transition System; Process Construct; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5042; https://ink.library.smu.edu.sg/context/sis_research/article/6045/viewcontent/verifying.pdf
• Institution: Singapore Management University

In this work, we study model checking of compositional real-time systems. A system is modeled using mutable data variables as well as a compositional timed process. Instead of explicitly manipulating clock variables, a number of compositional timed behavioral patterns are used to capture quantitative timing requirements, e.g. delay, timeout, deadline, timed interrupt, etc. A fully automated abstraction technique is developed to build an abstract finite state machine from the model. The idea is to dynamically create/delete clocks, and maintain/solve a constraint on the clocks. The abstract machine weakly bi-simulates the model and, therefore, LTL model checking or trace-refinement checking are sound and complete. We enhance our home-grown PAT model checker with the technique and show its usability via the verification of benchmark systems.