Browse by author
Lookup NU author(s): Professor Alex Yakovlev
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.
Author(s): Semenov A, Yakovlev A
Publication type: Report
Publication status: Published
Series Title: Department of Computing Science Technical Report Series
Year: 1997
Pages: 26
Print publication date: 01/04/1997
Source Publication Date: April 1997
Report Number: 572
Institution: Department of Computing Science, University of Newcastle upon Tyne
Place Published: Newcastle upon Tyne
URL: .Contextual Net Unfolding and Asynchronous System Verification
