Publication Type

Conference Proceeding Article

Version

publishedVersion

Publication Date

10-2008

Abstract

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.

Keywords

Model Check, Operational Semantic, Linear Temporal Logic, Parallel Composition, Strongly Connect Component

Discipline

Programming Languages and Compilers | Software Engineering

Research Areas

Software and Cyber-Physical Systems

Publication

Proceedings of the 10th International Conference on Formal Engineering Methods, ICFEM 2008, Kitakyushu-City, Japan, October 27-31

First Page

5

Last Page

24

ISBN

9783540881933

Identifier

10.1007/978-3-540-88194-0_4

Publisher

Springer Link

City or Country

Kitakyushu-City, Japan

Additional URL

https://doi.org/10.1007/978-3-540-88194-0_4

Download

Share

COinS