Introduction to the ISO specification language LOTOS
Computer Networks and ISDN SystemsPublished 1 January 1987Open access
Tommaso Bolognesi, Ed Brinksma
Citations1,293
Generate an AI Snapshot to get a quick, structured summary of this paper.
Study Snapshot
ObjectiveStudy objective
MethodsResearch methodology
PopulationPopulation studied
Sample sizeSample sizes
OutcomesStudy outcomes here
ResultsStudy results comes here
LimitationsResearch study limitations comes here
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
Abstract
LOTOS is a specification language that has been specifically developed for the formal description of the OSI (Open Systems Interconnection) architecture, although it is applicable to distributed, concurrent systems in general. In LOTOS a system is seen as a set of processes which interact and exchange data with each other and with their environment. LOTOS is expected to become an ISO international standard by 1988.
Keywords
Computer Science
Mathematics and Computers in SimulationIntroduction to automata theory, languages and computation
10,827 Citations1981
Lecture notes in computer scienceConcurrency and automata on infinite sequences
1,861 Citations2005David Park
A general method for proving/deciding equivalences between omega-regular languages, whose recognizers are modified forms of Buchi or Muller-McNaughton automata, derived from Milner's notion of “simulation” is obtained.
Journal of the ACMAlgebraic laws for nondeterminism and concurrency
1,361 Citations1985Matthew Hennessy, Robin Milner
The paper demonstrates, for a sequence of simple languages expressing finite behaviors, that in each case observation congruence can be axiomatized algebraically and the algebraic language described here becomes a calculus for writing and specifying concurrent programs and for proving their properties.
Journal of the ACMA Theory of Communicating Sequential Processes
1,191 Citations1984Stephen Brookes, C. A. R. Hoare +1 more
A mathematical model for communicating sequential processes is given, and a number of its interesting and useful properties are stated and proved.
Theoretical Computer ScienceTesting equivalences for processes
1,151 Citations1984Rocco De Nicola, Matthew Hennessy
This work shows how to define in a natural way three different equivalences on processes that are applied to a particular language CCS and gives associated complete proof systems and fully abstract models.
Theoretical Computer ScienceCalculi for synchrony and asynchrony
898 Citations1983Robin Milner
It is shown that the author's Calculus of Communicating Systems (1980), which is an asynchronous model, is derivable from the calculus presented here, which models both synchronous and asynchronous computation.
Information and ControlProcess algebra for synchronous communication
880 Citations1984J.A. Bergstra, Jan Willem Klop
Within the context of an algebraic theory of processes, an equational specification of process cooperation is provided and some relationships are shown to hold between the four concepts of merging.
Fundamentals of Algebraic Specification 2
875 Citations1990Hartmut Ehrig, Bernd Mahr
In ABSTRACT ACT ONE the shared sub specification together with the corresponding morphisms has to be given explicitly, while it is implicitly constructed in ACT ONE.
Communications of the ACMAbstract data types and the development of data structures
462 Citations1977John V. Guttag
This paper presents and discusses the application of an algebraic technique for the specification of abstract data types and presents examples of a top-down development of a symbol table for a block structured language.
Journal of Computer and System SciencesA complete inference system for a class of regular behaviours
319 Citations1984Robin Milner
Les arbres consideres sont des arcs etiquetes par des symboles faits d'un ensemble ACT={a, b, ...}, que nous appellerons «actions».
Acta InformaticaExtensional equivalences for transition systems
254 Citations1987Rocco De Nicola
It will be shown that many equivalences, although defined very differently by following different intuitions about systems behaviour, turn out to be the same or to differ only in minor detail for a large class of transition systems.
ACM Transactions on Programming Languages and SystemsCIRCAL and the representation of communication, concurrency, and time
151 Citations1985George Milne
An operational semantics, acceptance semantics, is introduced, and it is in terms of this active experimentation that meaning is given to the CIRCAL syntax, thus allowing proof of system properties to be constructed.
Lecture notes in computer scienceTesting equivalences for processes
122 Citations1983Rocco De Nicola, Matthew Hennessy
This work shows how to define in a natural way three different equivalences on processes that are applied to a particular language CCS and gives associated complete proof systems and fully abstract models.
Notes on Algebraic Calculi of Processes
88 Citations1985Gérard Boudol
The intoduce a calculus called MEIJE built on a monoid of synchronized actions and illustrate some general semantic notions and the concept of subcalculus is illustrated through the description in the language of the class of rational parallel place machines.
Computers in IndustryOn the formal specification and verification of CIM architectures using LOTOS
30 Citations1986F.P.M. Biemans, Pieter Blonk
It is shown that the language LOTOS, developed by the International Organisation for Standardization, is suitable for this purpose and an architecture of a workcell comprising ‘workstations’, a ’workcell controller’ and a ‘transport system’ is specified using LOTOS.
IEEE Transactions on ComputersA LOTOS Specification of the PROWAY Highway Service
15 Citations1986Vincenza Carchiolo, Faro +3 more
The paper presents a LOTOS specification of the PROWAY interface for process control applicatioins, defined by IEC, the International Electrotechnical Commision, and shows how LOTOS supports formal reasoning aimed at establishing consistency between service and protocol specifications.