Contextual Net Unfolding and Asynchronous System Verification

摘要

A finite truncated unfolding of a Petri net is known to be a useful tool forverifying correctness of asynchronous systems. The paper proposes the use of contextual nets instead, by presenting an algorithm for constructing a finite contextual net unfolding segment. The method is applied to the verification of an asynchronous control structure implementing a four-slot synchronous communication mechanism, intended for use in real-time systems. The paper shows when the use of contextual net unfolding is most advantageous compared to the ordinary Petri net unfolding.