40 Years of Computing at Newcastle
Department Technical Report Series No. 572
Contextual Net Unfolding and Asynchronous System Verification
A. Semenov and A. Yakovlev
University of Newcastle upon Tyne. 1997.
Abstract
A finite truncated unfolding of a Petri net is known to be a useful tool for verifying correctness of asynchronous systems. It may however suffer from an unnecessary exponential explosion when applied to Petri net models of hardware with level-based signals (e.g., circuits built of logic gates). 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 asynchronous 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.
Department Technical Report Series - 1997
Department Technical Report Series Index
Contents Page - 40 Years of Computing at Newcastle
Technical Report Abstract No. 572, 30 June 1997