Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
2-2009
Abstract
Recent development on distributed systems has shown that a variety of fairness constraints (some of which are only recently defined) play vital roles in designing self-stabilizing population protocols. Current practice of system analysis is, however, deficient under fairness. In this work, we present PAT, a toolkit for flexible and efficient system analysis under fairness. A unified algorithm is proposed to model check systems with a variety of fairness effectively in two different settings. Empirical evaluation shows that PAT complements existing model checkers in terms of fairness. We report that previously unknown bugs have been revealed using PAT against systems functioning under strong global fairness.
Keywords
Model Check, Linear Temporal Logic, Label Transition System, Model Check Algorithm, Population Protocol
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2
First Page
709
Last Page
714
ISBN
9783642026577
Identifier
10.1007/978-3-642-02658-4_59
Publisher
Springer Link
City or Country
Grenoble, France
Citation
SUN, Jun; LIU, Yang; DONG, Jin Song; and PANG, Jun.
PAT: Towards flexible verification under fairness. (2009). Proceedings of the 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2. 709-714.
Available at: https://ink.library.smu.edu.sg/sis_research/5038
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-02658-4_59