Loading...
Thumbnail Image
Item

Compositional nonblocking verification with always enabled events and selfloop-only events

Abstract
This paper proposes to improve compositional nonblocking verification through the use of always enabled and selfloop-only events. Compositional verification involves abstraction to simplify parts of a system during verification. Normally, this abstraction is based on the set of events not used in the remainder of the system, i.e., in the part of the system not being simplified. Here, it is proposed to exploit more knowledge about the system and abstract events even though they are used in the remainder of the system. Abstraction rules from previous work are generalised, and experimental results demonstrate the applicability of the resulting algorithm to verify several industrial-scale discrete event system models, while achieving better state-space reduction than before.
Type
Conference Contribution
Type of thesis
Series
Citation
Pilbrow, C., & Malik, R. (2013). Compositional nonblocking verification with always enabled events and selfloop-only events. In C. Artho & P. C. Olveczky (Eds.), Preliminary Proceedings Second International Workshop on Formal Techniques for Safety-Critical Systems, Queenstown, NZ(pp. 147–162). Springer. http://doi.org/10.1007/978-3-319-05416-2_11
Date
2013-10-29
Publisher
Springer
Degree
Supervisors
Rights
© 2013 Springer.