A LOTOS Simulator in OBJ
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.
KeywordsBehavior Expression Inference Rule Operational Semantic Label Transition System Process Algebra
Unable to display preview. Download preview PDF.
- 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
- 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
- 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
- Joseph Goguen et al. Introducing OBJ3. This volume.Google Scholar
- ISO 7498. Information Processing Systems - Basic Reference Model for Open System Interconnection. 1983.Google Scholar
- 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
- 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
- M. Diaz and C. Visser. SEDOS:Designing Open Distributed Systems. IEEE Software, November, pp. 24–33, 1989.Google Scholar
- 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
- 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
- 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
- P.H.J. van Eijk, C.A. Vissers and M. Diaz (eds.). The Formal Description Technique LOTOS. North-Holland, 1989.Google Scholar
- Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 92, Springer-Verlag, 1980.Google Scholar
- Software Environment for Design of Open Distributed Systems, HIPPO-LOTOS Simulator. University of Twente, The Netherlands.Google Scholar
- P.H.J. van Eijk. Software tools for the specification language LOTOS. PhD. thesis, University of Twente, 1988.Google Scholar
- Joseph Goguen. OBJ as a Theorem Prover with Applications to Hardware Verification. Technical report SRI-SCL-88–4R2, August 1988.Google Scholar
- 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
- 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