Abstract
The interleaved expansion presented in [QLP93] is a method to compute and represent the global events of a system preserving parallelism. As a side effect, this method provides important advantages in the technology of translation from LOTOS to Petri nets over static (direct) transformations and opens a simple process algebra form of representation for an important class of Petri nets. This work presents an algorithm that maps ITcalulus elements into labeled Petri nets and gives a comprehensive overview of different aspects of the translation from LOTOS to Petri nets using this intermediate form of representation.
Keywords
Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems. An Approach to the State Explosion Problem. PhD thesis, Faculté de Sciences Appliquées, University of Liege, (1995).
Hubert Garavel and Joseph Sifakis. Compilation and Verification of LOTOS Spec-ifications. In Luigi Logrippo, Robert L. Probert, and Hasan Ural, editors, Protocol Specification, Testing, and Verification X, pages 359–376, Ottawa, Ontario (CA), June 1990. IFIP, Elsevier Science B.V. (North-Holland).
ISO. Information Processing Systems - Open Systems Interconnection - LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Be-haviour. IS-8807. International Standards Organization, (1989). [published 15/feb/1989].
Günter Karjoth. Implementing Process Algebra Specifications by State Machines. In Sudhir Aggarwal and Krishan Sabnani, editors, Protocol Specification, Testing, and Verification VIII, pages 47–60, Atlantic City, New Jersey, USA, June 1988. IFIP, Elsevier Science B.V. (North-Holland).
H. Kremer. Derivation of efficient implementations from formal descriptions - is-sues, methods and conformance. In D. Hogrefe and S. Leue, editors, Formal Description Techniques, VII, pages 421–436, Berna (Switzerland), (1994). IFIP, Elsevier Science B.V. (North-Holland). Proceedings FORTE’94, 4–7 October, (1994).
R. Langerak. Transformations and Semantics for LOTOS. PhD thesis, Univ. of Twente, (1992).
David Larrabeiti. Contribucidn al Andlisis del Espacio de Estados de Especificaciones LOTOS. PhD thesis, Technical University of Madrid, Spain, (1996).
G. Leon, J. C. Dumas, J. A. de la Puente, N. Zakhama, and A. Alonso. The IPTES Environment: Support for Incremental Heterogeneous and Distributed Proto-typing. In Real-Time Systems. Kluwer Academic Press, may 1993.
Saturnino Marchena and Gonzalo Leon. Transformation from LOTOS specs to Galileo Nets. In Ken J. Turner, editor, Formal Description Techniques, I, pages 217–230, Stirling, Scotland, UK, (1989). IFIP, North-Holland. Proc. FORTE’88, (1988).
José A. Manas and Joaquin Salvachiia. Aß: A Virtual LOTOS Machine. In Gordon Rose and Ken Parker, editors, Formal Description Techniques, IV, Sydney (AU), (1992). IFIP, Elsevier Science B.V. (North-Holland). Proc.t FORTE’91, 19–22 November, (1991).
Santiago Payee. Contribuciôn al Andlisis y Transformation de Especificaciones LOTOS. PhD thesis, Technical Univ. of Madrid, (1990).
J. Quemada, D. Larrabeiti, and S. Pavon. Compressed State Space Representation of LOTOS Specifications. In Ken J. Turner, editor, Formal Description Techniques, VI, pages 19–34, Boston, Massachussetts, EEUU, (1993). IFIP, North-Holland. Pro-ceedings FORTE’93, 26–29 October, (1993).
Juan Quemada, Santiago Pavón, and Angel Fernandez. State Exploration by Transformation with LOLA. In Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989.
W. Reisig. Petri Nets, an Introduction. Springer, Berlin (DE), (1985).
W. Reisig. Place/Transition Systems. In Petri Nets: Central Models and Their Properties. Advances in Petri Nets 1986., volume 254 of LNCS, pages 117–141. Springer Verlag, Berlin (DE), (1987).
G. Rozenberg. Behaviour of Elementary Petri Nets. volume 254 of LNCS, pages 60–94. Springer-Verlag, Berlin (DE), (1987).
Riccardo Sisto and Adriano Valenzano. Mapping Petri nets with Inhibitor Arcs onto Basic LOTOS Behaviour Expressions. IEEE Transactions on Computers., 44(12):1361–1370, December 1995.
Antti Valmari. State Space Generation: Efficiency and Practicality. PhD thesis, Tampere University of Technology, Tampere, Finland, (1988).
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Larrabeiti, D., Quemada, J., Pavón, S. (1996). From LOTOS to Petri Nets through Iexpansion. In: Gotzhein, R., Bredereke, J. (eds) Formal Description Techniques IX. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35079-0_31
Download citation
DOI: https://doi.org/10.1007/978-0-387-35079-0_31
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2883-4
Online ISBN: 978-0-387-35079-0
eBook Packages: Springer Book Archive