TY - GEN
T1 - Specifying and verifying event-based fairness enhanced systems
AU - Sun, Jun
AU - Liu, Yang
AU - Dong, Jin Song
AU - Wang, Hai H.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=57049108259&partnerID=8YFLogxK
UR - https://link.springer.com/chapter/10.1007/978-3-540-88194-0_4
U2 - 10.1007/978-3-540-88194-0_4
DO - 10.1007/978-3-540-88194-0_4
M3 - Conference publication
AN - SCOPUS:57049108259
SN - 354088193X
SN - 9783540881933
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 5
EP - 24
BT - Formal Methods and Software Engineering - 10th International Conference on Formal Engineering Methods, ICFEM 2008, Proceedings
PB - Springer
T2 - 10th International Conference on Formal Engineering Methods, ICFEM 2008
Y2 - 27 October 2008 through 31 October 2008
ER -