Abstract
Within the framework of concurrent systems, several verification approaches require as a preliminary step the complete derivation of the state space. Partial-order methods are efficient for reducing the state explosion due to the representation of parallelism by interleaving. The covering step graphs are introduced as an alternative to labelled transition systems. A transition step consists of several possibly concurrent events. In a covering step graph, steps of independent transitions are substituted as much as possible to the subgraph which would result from the firing of the independent transitions. Attention must be paid to the case of conflict and confusion. An algorithm for the “on the fly” derivation of step graphs is proposed. This algorithm is then extended to behaviour analysis by means of observational equivalence. A performance evaluation is made with respect to other methods.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Fernandez, L. Mounier Verifying Bisimulation on the Fly 3 rd. Int. Conf on Formal Description Techniques, Madrid, 1990
P. Godefroid, P. Wolper Using Partial Orders for efficient verification of deadlock freedom and safety properties In Computer Aided Verification, 1991, LNCS 575
P. Godefroid, D. Pirotin Refining Dependencies Improves Partial-Order verification methods In Computer Aided Verification. 1993, LNCS 697
J. Esparza Model Checking using net unfoldings In TAPSOFT'93, 1993. LNCS 668
M. Hennessy, R. Milner Algebraic Laws for Nondeterminism and Concurrency Journal of the A.C.M Volume 32 1985
K. Jensen Coloured Petri Nets. In Brauer, W., Reisig, W. & Rozenberg, G. (Ed.): Petri Nets: Central Models and their Properties. Advances in Petri Nets LNCS 254
D. H. Pitt, D. Freestone The derivation of conformance tests from lotos specifications IEEE Transactions on Software Engineering, 16(12), 1990
K. L. McMillan Trace theoretic verification of asynchronous circuits using unfoldings In Computer Aided Verification, 1995, LNCS 939
A. Mazurkiewicz Trace Theory In “Petri Nets: Applications and Relationship to other models of concurrency” LNCS 255
R. Milner Communication and Concurrency Prentice Hall.
W. Reisig Petri Nets: an Introduction EATCS, Monographs on Theoretical Computer Science, Springer Verlag, 1985
A. Valmari Stubborn Sets for reduced state space generation 10 th Int. Conf on Application and Theory of Petri Nets, Bonn, 1989, LNCS 483
P. Wolper, P. Godefroid Partial Order Methods for Temporal Verification Proceedings of CONCUR'93, LNCS 715
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vernadat, F., Azéma, P., Michel, F. (1996). Covering step graph. In: Billington, J., Reisig, W. (eds) Application and Theory of Petri Nets 1996. ICATPN 1996. Lecture Notes in Computer Science, vol 1091. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-61363-3_28
Download citation
DOI: https://doi.org/10.1007/3-540-61363-3_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-61363-3
Online ISBN: 978-3-540-68505-0
eBook Packages: Springer Book Archive