PARTIAL UNFOLDING FOR COMPOSITIONAL NONBLOCKING VERIFICATION OF EXTENDED FINITE-STATE MACHINES

This working paper describes a framework for compositional nonblocking verification of reactivesystemsmodelled as extended finite-state machines. The nonblocking property can capture theabsence of livelocks and deadlocks in concurrent systems. Compositional verification is shownin previous work to be effective to verify this property for large discrete event systems. Here,these results are applied to extended finite-state machines communicating via shared memory.The model to be verified is composed gradually, simplifying components through abstraction ateach step, while conflict equivalence guarantees that the final verification result is the same as itwould have been for the non-abstracted model. The working paper concludes with an exampleshowing the potential of compositional verification to achieve substantial state-space reduction