A LOTOS Simulator in OBJ

  • Kazuhito Ohmaki
  • Koichi Takahashi
  • Kokichi Futatsugi
Part of the Advances in Formal Methods book series (ADFM, volume 2)


In this paper, we show how to write a LOTOS simulator using OBJ. Both syntax rules and their inference rules (axioms) of LOTOS can be formally specified by operator definition part and equation definition part in OBJ, respectively.

When writing the simulator using a term rewriting system, we need a lazy evaluation mechanism, because rewriting operations for recursive process definitions in LOTOS would not terminate without lazy evaluation. We use this lazy evaluation mechanism of OBJ to realize the simulator. Powerful features like theory, view, and parameterized modules of OBJ are fruitfully used to write the simulator.

Using OBJ as an implementation language, we can also use the power of the abstract data type features of OBJ. This leads to the enhancement of LOTOS in future, especially for abstract data type enhancement. The introduction of subsort is one of the most distinguished point of using OBJ. This point is discussed using simple examples.

We also show an example to prove properties of a LOTOS specification.


Behavior Expression Inference Rule Operational Semantic Label Transition System Process Algebra 
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 8807.Information Processing Systms–Open System Interconnection – LOTOS – A formal description technique based on the temporal ordering of observational behavior. 1989–02–15.Google Scholar
  2. [2]
    Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud and José Meseguer. Principles of OBJ2. Proc. 12th ACM Symp. on POPL, pp. 52–66, 1985.Google Scholar
  3. [3]
    Kokicji Futatsugi, Joseph Goguen, José Meseguer and K. Okada. Parameterized Programming in OBJ2. Proc. 9th Int’l Conference on Software Engineering, pp. 51–60, 1987.Google Scholar
  4. [4]
    Joseph Goguen et al. Introducing OBJ3. This volume.Google Scholar
  5. [5]
    ISO 7498. Information Processing Systems - Basic Reference Model for Open System Interconnection. 1983.Google Scholar
  6. [6]
    Kazuhito Ohmaki and Kokichi Futatsugi. Specifications of Library and Lift Problems in LOTOS. Technical Report of Information Processing Society of Japan, SE 64–12, 1989.Google Scholar
  7. [7]
    T. Bolognesi and Ed Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, Vol. 14, pp. 25–59, 1987.Google Scholar
  8. [8]
    M. Diaz and C. Visser. SEDOS:Designing Open Distributed Systems. IEEE Software, November, pp. 24–33, 1989.Google Scholar
  9. [9]
    nd DP, ISO/IEC DP 10026–1,2,3. Information processing systems - Open systems interconnection - Distributed transaction processing, Part 1 (Model), Part 2 (Service definition), Part 3 (Protocol specification). ISO/IEC JTC 1/SC 21/WG5, 1988.Google Scholar
  10. [10]
    I. Ajubi and M. van Sinderen. High level synchronization services of OSI - Commitment, Concurrency and Recovery. University of Twente MEMORANDUM INF-88–35, 1988.Google Scholar
  11. [11]
    M. van Sinderen and I. Widya. On the Design and Formal Specification of a Transaction Protocol. Proc. Third International Conference of Formal Description Techniques (FORTE’90), pp. 515–532, November 1990.Google Scholar
  12. [12]
    P.H.J. van Eijk, C.A. Vissers and M. Diaz (eds.). The Formal Description Technique LOTOS. North-Holland, 1989.Google Scholar
  13. [13]
    Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 92, Springer-Verlag, 1980.Google Scholar
  14. [14]
    Hartmut Ehrich and Bernd Mahr. Fundamentals of Algebraic Specification. Springer Verlag, Berlin, 1985.CrossRefGoogle Scholar
  15. [15]
    Software Environment for Design of Open Distributed Systems, HIPPO-LOTOS Simulator. University of Twente, The Netherlands.Google Scholar
  16. [16]
    P.H.J. van Eijk. Software tools for the specification language LOTOS. PhD. thesis, University of Twente, 1988.Google Scholar
  17. [17]
    Joseph Goguen. OBJ as a Theorem Prover with Applications to Hardware Verification. Technical report SRI-SCL-88–4R2, August 1988.Google Scholar
  18. [18]
    Giuseppe Scollo. Some facilities for concise data type definition in LOTOS, Draft Version 1. ISO/TC 97/SC 21/N2015, Potential enhancements to LOTOS, 1987.Google Scholar
  19. [19]
    H. Ehrig, J. Buntrock, P. Boehm, K.-P. Hasler and F. Nuernberg. Towards an Algebraic Semantics of the ISO-Specification Language LOTOS,“ in [ 12] pp. 249–268.Google Scholar
  20. [20]
    J.A. Bergstra and J.W. Klop. Process algebra for Synchronous Communication. Information and Control, Vol. 60, pp. 109–137, 1984.MathSciNetzbMATHCrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2000

Authors and Affiliations

  • Kazuhito Ohmaki
    • 1
  • Koichi Takahashi
    • 1
  • Kokichi Futatsugi
    • 1
  1. 1.Electrotechnical Laboratory1-1-4 UmeZonoTsukubaIbaraki 305Japan

Personalised recommendations