Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Iso 8807.Information Processing Systms–Open System Interconnection – LOTOS – A formal description technique based on the temporal ordering of observational behavior. 1989–02–15.
Kokichi Futatsugi, Joseph Goguen, Jean-Pierre Jouannaud and José Meseguer. Principles of OBJ2. Proc. 12th ACM Symp. on POPL, pp. 52–66, 1985.
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.
Joseph Goguen et al. Introducing OBJ3. This volume.
ISO 7498. Information Processing Systems - Basic Reference Model for Open System Interconnection. 1983.
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.
T. Bolognesi and Ed Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Networks and ISDN Systems, Vol. 14, pp. 25–59, 1987.
M. Diaz and C. Visser. SEDOS:Designing Open Distributed Systems. IEEE Software, November, pp. 24–33, 1989.
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.
I. Ajubi and M. van Sinderen. High level synchronization services of OSI - Commitment, Concurrency and Recovery. University of Twente MEMORANDUM INF-88–35, 1988.
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.
P.H.J. van Eijk, C.A. Vissers and M. Diaz (eds.). The Formal Description Technique LOTOS. North-Holland, 1989.
Robin Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 92, Springer-Verlag, 1980.
Hartmut Ehrich and Bernd Mahr. Fundamentals of Algebraic Specification. Springer Verlag, Berlin, 1985.
Software Environment for Design of Open Distributed Systems, HIPPO-LOTOS Simulator. University of Twente, The Netherlands.
P.H.J. van Eijk. Software tools for the specification language LOTOS. PhD. thesis, University of Twente, 1988.
Joseph Goguen. OBJ as a Theorem Prover with Applications to Hardware Verification. Technical report SRI-SCL-88–4R2, August 1988.
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.
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.
J.A. Bergstra and J.W. Klop. Process algebra for Synchronous Communication. Information and Control, Vol. 60, pp. 109–137, 1984.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer Science+Business Media New York
About this chapter
Cite this chapter
Ohmaki, K., Takahashi, K., Futatsugi, K. (2000). A LOTOS Simulator in OBJ. In: Goguen, J., Malcolm, G. (eds) Software Engineering with OBJ. Advances in Formal Methods, vol 2. Springer, Boston, MA. https://doi.org/10.1007/978-1-4757-6541-0_8
Download citation
DOI: https://doi.org/10.1007/978-1-4757-6541-0_8
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4419-4965-3
Online ISBN: 978-1-4757-6541-0
eBook Packages: Springer Book Archive