Abstract
In a companion paper [Barb 90a,b], we proposed a Place/Transition-net (P/T-net) semantics for a subset of Lotos. This subset is such that Lotos specifications can be translated into finite structure Petri nets. It is therefore possible to apply P/T-net verification techniques since they require finite structure. It this paper, we demonstrate that it is possible to apply P/T-net verification methods without an a priori construction of the P/T-net associated to the Lotos specification to be analysed. In particular we consider a well known reachability analysis technique for P/T-nets, namely, the Karp and Miller procedure.
This work has been funded by the Natural Sciences and Engineering Research Council of Canada, the Centre de recherche informatique de Montréal and Bell Northern Research.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
8 References
Barbeau, M., Bochmann, G. V. Deriving Analysable Petri Nets from Lotos Specifications, Research report no. 707, Dept. d'IRO, Université de Montréal, 1990.
Barbeau, M., Bochmann, G. V. Verification of Lotos Specifications: A Petri Net Based Approach, Proc. of Canadian Conf. on Elec. and Computer Eng., Ottawa, 1990.
Barbeau, M., Bochmann, G. V. Experiences with Automated Verification Tools: Application to Discrete Event Systems, Proc. of Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, 1989.
Bochmann, G. V. Finite State Description of Communication Protocols, Computer Network 2, (361–372), 1978.
Bolognesi, T., Brinksma, E. Introduction to the ISO Specification Language Lotos, Computer Networks and ISDN, Vol. 14, No. 1, (25–59), 1987.
Bolognesi, T., Smolka, S. A. Fundamental Results for the Verification of Observational Equivalence: A Survey, Proc. of PSTV VII, Zurich, 1987.
Finkel, A. A Minimal Coverability Graph for Petri Nets, Proc. 11th Int. Conf. on Application and Theory of Petri Nets, Paris, 1990.
Garavel, H., Najm, E. Tilt: From Lotos to Labelled Transition Systems, in P. H. J. van Eijk, C. A. Vissers and M. Diaz (Eds.): The Formal Descrip. Tech. Lotos, North-Holland, 1989.
Holzmann, G. J. [1989]. Algorithms for Automated Protocol Validation, Proc. of Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, 1989.
Karp, R. M., Miller, R. E. Parallel Program Schemata, J. Computer and System Sciences 3, (147–195), 1969.
Marchena, S., Leon, G. Transformation from Lotos Specs to Galileo Nets, in K. J. Turner (Ed.): Formal Description Techniques, North-Holland, 1989.
Olderog, E.-R. Operational Petri Net Semantics for CCSP, LNCS 266, Springer-Verlag, 1987.
Peterson, J. L. Petri Net Theory and the Modelling of Systems, Prentice Hall, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbeau, M., Bochmann, G.V. (1991). Extension of the Karp and miller procedure to lotos specifications. In: Clarke, E.M., Kurshan, R.P. (eds) Computer-Aided Verification. CAV 1990. Lecture Notes in Computer Science, vol 531. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0023747
Download citation
DOI: https://doi.org/10.1007/BFb0023747
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-54477-7
Online ISBN: 978-3-540-38394-9
eBook Packages: Springer Book Archive