Abstract
A compositional verification method for Petri nets composed of place-bordered subnets is presented. The method assumes that the Petri net can be divided into an interesting and an environment component, and it facilitates the verification of all properties which can be stated in terms of the projections of the executions of the net onto its interesting component. For instance, one can check what is the lowest upper bound of the marking of any place in the interesting component, or whether some transition of the interesting component may ever occur. Also deadlocks and a certain class of livelocks can be detected. The method is based on the process-algebraic compositional approach, but is novel in that it can be used to produce state-oriented information, and it works in a framework with asynchronous communication. In the example used for demonstrating the method, an infinite number of systems of different size is analysed with a small finite amount of effort.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Berthelot, G.: Transformations and Decompositions of Nets. In Petri Nets: Central Models and Their Properties, Lecture Notes in Computer Science 254, Springer-Verlag 1987, pp. 359–376.
Brookes, S. D. & Roscoe, A. W.: An Improved Failures Model for Communicating Sequential Processes. In: Proceedings of the NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag 1985, pp. 281–305.
Cheung, S. C. & Kramer, J.: Enhancing Compositional Reachability Analysis with Context Constraints. Proceedings of ACM SIGSOFT '93: Symposium on the Foundations of Software Engineering, Los Angeles, USA, December 1993, ACM Software Engineering Notes Vol. 18 Nr 5, 1993, pp. 115–125.
Finkel, A.: The Minimal Coverability Graph for Petri Nets. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 210–243. (Earlier version in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 1–21.)
Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. In: Computer-Aided Verification '90 (Proceedings of a workshop), AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, American Mathematical Society 1991, pp. 57–73.
Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall 1985, 256 p.
Jensen, K.: Coloured Petri Nets. In: Petri Nets: Central Models and Their Properties, Lecture Notes in Computer Science 254, Springer-Verlag 1987, pp. 248–299.
Kaivola, R. & Valmari, A.: The Weakest Compositional Semantic Equivalence Preserving Nexttime-less Linear Temporal Logic. Proceedings of CONCUR '92, Lecture Notes in Computer Science 630, Springer-Verlag 1992, pp. 207–221.
Kaivola, R. Compositional Linear Temporal Logic Model-Checking for Concurrent Systems. Licentiate Thesis, University of Helsinki, Department of Computer Science, Report C-1993-1, Helsinki, Finland, 1993, 58 + 42 pp.
Lindqvist, M.: Parameterized Reachability Trees for Predicate/Transition Nets. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 301–324. (Earlier version in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 22–42.)
Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491–515. (Earlier version in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, West Germany 1989, Vol II, pp. 1–22.)
Valmari, A.: Compositional State Space Generation. Advances in Petri Nets 1993, Lecture Notes in Computer Science 674, Springer-Verlag 1993, pp. 427–457. (Earlier version in Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France 1990, pp. 43–62.)
Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with a Reduction Algorithm. In: Protocol Specification, Testing and Verification XI, North-Holland 1991, pp. 3–18.
Valmari, A.: Alleviating State Explosion during Verification of Behavioural Equivalence. Department of Computer Science, University of Helsinki, Report A-1992-4, Helsinki, Finland 1992, 57 p.
Valmari, A., Kemppainen, J., Clegg, M. & Levante, M.: Putting Advanced Reachability Analysis Techniques Together: the “ARA” Tool. Proceedings of Formal Methods Europe '93, Lecture Notes in Computer Science 670, Springer-Verlag 1993, pp. 597–616.
Valmari, A. & Tienari, M.: Compositional Failure-Based Semantic Models for Basic LOTOS. Tampere University of Technology, Software Systems Laboratory, Report 16, Tampere, Finland, July 1993, 25 p.
Valmari, A. & Setälä, M.: A Fast Reduction Algorithm for Failure-Based Semantics. Submitted for publication, 13 p.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A. (1994). Compositional analysis with place-bordered subnets. In: Valette, R. (eds) Application and Theory of Petri Nets 1994. ICATPN 1994. Lecture Notes in Computer Science, vol 815. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58152-9_29
Download citation
DOI: https://doi.org/10.1007/3-540-58152-9_29
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58152-9
Online ISBN: 978-3-540-48462-2
eBook Packages: Springer Book Archive