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 quantitativ...