×

An interpreter for LOTOS, a specification language for distributed systems. (English) Zbl 0646.68028

LOTOS is an executable specification language for distributed systems currently being standardized within ISO as a tool for the formal specification of open systems interconnection protocols and services. It is based on an extended version of Milner’s calculus of communicating systems (CCS) and on ACT ONE abstract data type (ADT) formalism. A brief introduction to LOTOS is given, along with a discussion of LOTOS operational semantics, and of the executability of LOTOS specifications.
Further, an account of a prototype LOTOS interpreter is given, which includes an interactive system that allows the user to direct the execution of a specification (for example, for testing purposes). The interpreter was implemented in YACC/LEX, C and Prolog. The following topics are discussed: syntax and static semantics analysis; translation from LOTOS external format to internal representation; evaluation of ADT value expressions and extended CCS behaviour expressions. It is shown that the interpreter can be used in a variety of ways: to recognize whether a given sequence of interactions is allowed by the specification; to generate randomly chosen sequences of interactions; in a user-guided generation mode, etc.

MSC:

68N25 Theory of operating systems

Software:

LOTOS; YACC
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Schwartz, IEEE Trans. Comm. COM-30 pp 2486– (1982)
[2] ’Specification technique’, in Formal Description Techniques for Network Protocols, Report No. ICST/HLNP-80–3, National Bureau of Standards, June 1980.
[3] ’Constructive and executable specifications of protocol services by using abstract data types and finite-state transducers’, in and (eds), Protocol Specification, Testing, and Verification III, North-Holland, 1983, pp. 111–124.
[4] and , ’Executable description of the OSI transport service in Prolog,’ in and (eds), Protocol Specification, Testing and Verification IV, North-Holland, 1985, pp. 279–293.
[5] ’Protocol verification via executable logic specifications’, in and (eds), Protocol Specification, Testing, and Verification, III, North-Holland, Amsterdam, 1983, pp. 431–436.
[6] Zimmermann, IEEE Trans. Comm. COM-28 pp 425– (1980)
[7] ’A tutorial on LOTOS’, in (ed.), Protocol Specification, Testing, and Verification, V, North-Holland, Amsterdam, 1986, pp. 171–194.
[8] , and , ’The OSI transport service and its formal description in LOTOS’, in and (eds), Computer Network Usage: Recent Experiences, North-Holland, 1986, pp. 465–488.
[9] and , ’A temporal ordering specification of some session services’, in Communications Architectures & Protocols, Proceedings of the 1984 SIGCOMM Conference, pp. 107–114.
[10] International Organization for Standardization (ISO), Information Processing Systems – Open Systems Interconnection – LOTOS – A Formal Description Technique based on the Temporal Ordering of Observational Behavior (DP 8807), March 1985.
[11] ’A comparison of behavioural language simulators’, in and (eds), Protocol Specification, Testing, and Verification VI, North-Holland, 1987, pp. 85–96.
[12] ’Le langage CCS et son interprete; une implantation experimentale de CCS’, Rapport Technique CNRS-LAAS, Toulouse, 1985.
[13] ’An interactive system for the analysis of communicating processes’, in (ed.), Protocol Specification, Testing, and Verification V, North-Holland, Amsterdam, 1986, pp. 91–102.
[14] ’Software tools for the design of protocol systems, part I’, Memorandum INF-85-21, Technical University of Twente, Department of Informatics.
[15] and , Fundamentals of Algebraic Specifications 1, Springer-Verlag, Berlin, 1985. · doi:10.1007/978-3-642-69962-7
[16] ’A calculus of communicating systems’, Lecture Notes in Computer Science, Springer-Verlag, 1980. · Zbl 0452.68027 · doi:10.1007/3-540-10235-3
[17] Carchiolo, IEEE Trans. Computers C-35 pp 949– (1986)
[18] Communicating Sequential Processes, Prentice-Hall, 1985. · Zbl 0637.68007
[19] Guttag, Comm. ACM 21 pp 1048– (1978)
[20] ’Confluent reductions: abstract properties and applications to term rewriting systems’, 18th IEEE Symposium on Foundations of Computer Science, 1977, pp. 30–45.
[21] and , ’A critique of LOTOS’, ISO/TC97/SC21/WG1/N51, 1985.
[22] and , The UNIX Programming Environment, Prentice-Hall, Englewood Cliffs, 1984.
[23] and , Programming in Prolog, Springer-Verlag, Berlin, 1984.
[24] and , ’The Mentor – V5 Documentation’, Rapport Technique INRIA, No. 43, January 1985.
[25] and , ’Simple word problems in abstract algebra’, in (ed.), Computational Problems in Abstract Algebra, Pergamon Press, 1969, pp. 263–297.
[26] ’Application of the inference rules of CCS and LOTOS’, Technical Report TR-85–14, University of Ottawa, Department of Computer Science.
[27] ’SINAPS: a simulator of communicating systems’, Technical Report TR-86–14, University of Ottawa, Department of Computer Science, 1986.
[28] , and , ’Executing LOTOS specifications’, in and (eds), Protocol Specification, Testing and Verification VI, North-Holland, 1987, pp. 73–84.
[29] , and , ’Structure of a LOTOS interpreter’. Communications Architectures and Protocols. SIGCOMM ’86 Symposium, pp. 167–175.
[30] Ural, Computer Networks and ISDN Systems 11 pp 183– (1986)
[31] ’Protocol validation by random state exploration’, in and (eds), Protocol Specification, Testing, and Verification VI, North-Holland, 1987, pp. 233–242.
[32] and , ’On the architectural design of the formal specification of the session standards in LOTOS’, in and (eds), Protocol Specification, Testing, and Verification VI, North-Holland, 1987, pp. 3–14.
[33] and , ’Elements for the revised draft proposal’, Unpublished Document (Document LOTOS/85/26, November 1985.
[34] ’A program for generating and analyzing term rewriting systems’, Master’s Thesis, MIT Lab. for Computer Science, Cambridge, Mass., 1984.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.