Implementing LOTOS specifications by communicating state machines

  • Günter Karjoth
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 630)


This paper presents algorithms to translate a LOTOS specification into a network of extended finite state machines, a representation which is more tractable for simulation, verification by model checking, and code generation purposes. Objectives are efficient executability and the coverage of a wide range of LOTOS specifications.


State Machine Parallel Composition Process Algebra Selection Predicate Extended Finite State Machine 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    ISO. LOTOS — a formal description technique based on the temporal ordering of observational behaviour. IS 8807, 1988.Google Scholar
  2. 2.
    J.A. Mañas and T. de Miguel. From LOTOS to C. In K. Turner, editor, Formal Description Techniques I, pages 79–84. North-Holland, 1988.Google Scholar
  3. 3.
    S. Nomura, T. Hasegawa, and T. Takizuka. A LOTOS compiler and process synchronization manager. In Protocol Specification, Testing, and Verification X, pages 165–184. North-Holland, 1990.Google Scholar
  4. 4.
    C. Binding. Executing LOTOS behavior expressions. Research Report RZ 2118, IBM Research Division, 04/25/91.Google Scholar
  5. 5.
    R. Milner. A complete inference system for a class of regular behaviours. Journal of Computer and System Sciences, 28:439–466, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  6. 6.
    J.A. Bergstra and J.W. Klop. A complete inference system for regular processes with silent moves. In F.R. Drake and J.K. Truss, editors, Logic Colloquium. North-Holland, 1986.Google Scholar
  7. 7.
    D. Taubner. Finite Representations of CCS and TCSP Programs by Automata and Petri Nets, volume 369 of Lecture Notes in Computer Science. Springer Verlag, 1989.Google Scholar
  8. 8.
    G. Karjoth. Implementing process algebra specifications by state machines. In Protocol Specification, Testing and Verification VIII, pages 47–60. North-Holland, 1988.Google Scholar
  9. 9.
    E. Dubuis. An algorithm for translating LOTOS behavior expressions into automata and ports. In Formal Description Techniques, II, pages 163–177. North-Holland, 1989.Google Scholar
  10. 10.
    A. Valenzano, R. Sisto, and L. Ciminiera. Modeling the execution of LOTOS specifications by cooperating extended finite state machines. In IEEE Symp. on Parallel and Distributed Processing, Dallas, Tx, 9–13 December 1990.Google Scholar
  11. 11.
    G. Karjoth. XFSM: A formal model of communicating state machines for implementation specifications. Research Report RZ 2209, IBM Research Division, 09/12/1991.Google Scholar
  12. 12.
    ISO. Guidelines for the Application of Estelle, Lotos and SDL. Technical Report 10167, September 1991.Google Scholar
  13. 13.
    G. Karjoth, C. Binding, and J. Gustafsson. LOEWE: A LOTOS engineering workbench. Research Report RZ 2143, IBM Research Division, 06/17/91. A revised version will appear in Computer Networks and ISDN Systems, special issue on “Tools for FDTs”.Google Scholar
  14. 14.
    G. Karjoth. Generating Transition Graphs from LOTOS Specifications, Research Report RZ 2312, IBM Research Division, 05/18/1992.Google Scholar
  15. 15.
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8:244–263, April 1986.zbMATHCrossRefGoogle Scholar
  16. 16.
    J.F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. In M.S. Paterson, editor, ICALP 90, volume 443 of Lecture Notes in Computer Science, pages 626–638. Springer Verlag, 1990.Google Scholar
  17. 17.
    H. Garavel and J. Sifakis. Compilation and verification of LOTOS specifications. In Protocol Specification, Testing, and Verification X. pages 359–376, North-Holland, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Günter Karjoth
    • 1
  1. 1.IBM Research DivisionZurich Research LaboratoryRüschlikonSwitzerland

Personalised recommendations