BS ISO 8807:1989

0 Introduction
0.1 General
0.2 FDTs
0.3 The requirement for standard FDTs
0.4 The objectives to be satisfied by an FDT
0.5 The origin of LOTOS
0.6 The structure of this International Standard
1 Scope and field of application
2 References
3 Conformance
4 Basic mathematical concepts and notation
4.1 General
4.2 Sets
4.3 Lists
4.4 Strings
4.5 Relations and functions
4.6 Backus-Naur Form
4.7 Syntax-directed definitions
4.8 Derivation systems
5 Model
5.1 Introduction
5.2 Many-sorted algebras
5.3 Labelled transition systems
5.4 Structured labelled transition systems
6 Formal syntax
6.1 Lexical tokens
6.1.1 General
6.1.2 Basic characters
6.1.3 Reserved symbols
6.1.4 Identifiers
6.1.5 Requirement
6.1.6 Comments
6.1.7 Token separators
6.1.8 Requirement
6.2 Specification text
6.2.1 Specification
6.2.2 Definition-block
6.2.3 Data-type-definitions
6.2.4 P-expressions
6.2.5 Sorts, operations and equations
6.2.6 Process-definitions
6.2.7 Behaviour-expressions
6.2.8 Value-expressions
6.2.9 Declarations
6.2.10 Special-identifiers
7 Semantics
7.1 Introduction
7.1.1 Structure of the static semantics definition
7.1.2 Structure of the dynamic semantics definition
7.1.3 Structure of clause 7
7.2 General structures and definitions
7.2.1 Names and related functions
7.2.2 Algebraic specifications, terms and equations
7.2.3 Canonical specifications
7.3 Static semantics
7.3.1 Introduction
7.3.2 General structures and definitions
7.3.3 Reconstruction of terms
7.3.4 Flattening of a LOTOS specification
7.3.5 Functional structure of the flattening function
7.4 Semantics of data-presentations
7.4.1 General
7.4.2 The derivation system of a data-presentation
7.4.3 Congruence relation induces by a data-
        presentation
7.4.4 Quotient term algebra
7.5 Semantics of a canonical LOTOS specification
7.5.1 General
7.5.2 Auxiliary definitions
7.5.3 Transition derivation system
7.5.4 Structured labelled transition system
7.5.5 Formal interpretation of a canonical LOTOS
        specification
Annexes
A Standard library of data types
A.1 Introduction
A.2 Syntax of the data type library
A.3 Semantics of the data type library
A.4 The Boolean data type
A.5 Parameterized data type definitions
A.5.1 Element
A.5.2 Set
A.5.3 Strings
A.6 Unparameterized data type definitions
A.6.1 Natural number
A.6.2 Octet
A.6.3 Octet string
B Equivalence relations
B.1 Introduction
B.2 Weak bisimulation
B.2.1 Definitions
B.2.2 Laws for weak bisimulation congruence
B.2.3 Laws for weak bisimulation equivalence
B.3 Testing equivalence
B.3.1 Definitions
B.3.2 Laws for testing congruence
B.3.3 Laws for testing equivalence
B.4 References
C A tutorial on LOTOS
C.1 The specification of processes
C.2 Behaviour expressions in basic LOTOS
C.2.1 A basic process: inaction
C.2.2 Two basic operators
C.2.3 Recursion
C.2.4 Parallelism
C.2.5 Nondeterminism in LOTOS
C.2.6 Sequential composition of processes
C.2.7 Disruption of processes
C.2.8 An example in basic LOTOS
C.3 LOTOS data types
C.3.1 Introduction
C.3.2 Concepts of LOTOS data types
C.4 LOTOS with structured interactions
C.4.1 Structured event offers
C.4.2 Conditional constructs
C.4.3 Process abstraction with parameterization
C.4.4 Generalized choice and parallel expressions
C.4.5 Generalized sequential composition
C.4.6 Another example in LOTOS
C.5 LOTOS syntax table
D Syntax diagrams
E Informal basis for abstract data types
E.1 Introduction
E.1.1 Representations
E.2 Signatures
E.3 Terms and expressions
E.3.1 Generation of terms
E.4 Values and algebras
E.4.1 Equations and qualifications
E.5 Algebraic specification and semantics
E.6 Representation of values
Tables
1 Metalanguage symbols
2 Actualization function
3 Functional structure of flattening function
4 Interaction types
5 LOTOS syntax table
Figures
1 Structure of clause 7
2 Two interacting processes
3 Full duplex buffer
4 Composition of two buffer processes
5 Hiding

Technique that is in general use for the formal description of distributed concurrent information processing systems. In particular the service definitions and protocol specifications described in BS 6568 can be described formally in LOTOS.