An algorithm for compositional nonblocking verification using special events

Abstract

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.