Specifying and verifying event-based fairness enhanced systems

• Main Authors: SUN, Jun, LIU, Yang, DONG, Jin Song, WANG, Hai H.
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2008
• Subjects: Model Check; Operational Semantic; Linear Temporal Logic; Parallel Composition; Strongly Connect Component; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5048; https://ink.library.smu.edu.sg/context/sis_research/article/6051/viewcontent/Specifying_and_Verifying_Event_Based_Fairness_Enhanced_Systems.pdf
• Institution: Singapore Management University

Liveness/Fairness plays an important role in software specification, verification and development. Existing event-based compositional models are safety-centric. In this paper, we describe a framework for systematically specifying and verifying event-based systems under fairness assumptions. We introduce different event annotations to associate fairness constraints with individual events. Fairness annotated events can be used to embed liveness/fairness assumptions in event-based models flexibly and naturally. We show that state-of-the-art verification algorithms can be extended to verify models under fairness assumptions, with little computational overhead. We further improve the algorithm by other model checking techniques like partial order reduction. A toolset named Pat has been developed to verify fairness enhanced event-based systems. Experiments show that Pat handles large systems with multiple fairness assumptions.