An algorithm for compositional nonblocking verification using special events
Pilbrow, C., & Malik, R. (2015). An algorithm for compositional nonblocking verification using special events. Science of Computer Programming, 113, 119–148. http://doi.org/10.1016/j.scico.2015.05.010
Permanent Research Commons link: https://hdl.handle.net/10289/10586
This paper proposes to improve compositional nonblocking verification of discrete event systems through the use of special 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 remainder of the system and check how events are being used. Always enabled events, selfloop-only events, failing events, and blocked events are easy to detect and often help with simplification 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.
This is an author’s accepted version of an article published in the journal: Science of Computer Programming. © 2015 Elsevier.