LOTOS specifications of telephone systems
Simple POTS systems
These specifications are intendent for beginners as a tutorial only.
Resource oriented style
This specification style uses synchronization in order to determine
the appropriate temporal ordering of actions offered by different
components of the system. The components are a network with several
instances of phones.
State oriented style
This specification style is used to describe finite state machines.
In LOTOS, on specifies a single process that continuously recurses
changing state every time. Its structure is analogous to a C case statement.
Busy phones with gates
This specification uses gates for operations. It also shows how
one can determine that a phone is busy using the interleave construct.
Constraint oriented style
The constraint oriented style uses three type of constraints:
- the local cosntraints ( temporal ordering of actions of a phone)
- the end to end constraints( temporal ordering of actions of a network)
- the global constraints (verification if an action is allowed)
Advanced POTS systems
Status oriented POTS with multiple call terminations
This specification of a POTS system addresses the difficulties to specify different termination patterns as a result of the different states a phone is in when a termination occurs
Constraint oriented POTS specification
This specification of a POTS system uses the constraint oriented style that relies heavily on Abstract Data Types.
Specification of telephone features systems
Call Waiting, Call Forward and Originate Call Screening>
This is a LOTOS specification of a basic POTS system that has been modified to include the following features: call waiting, call forward, originate call screening and voice mail. It uses the resource or status oriented style.
LOTOS specification using extended Abstract Data Types
same LOTOS specification but with translated extended Abstract Data Types
Using Abstract Data Types to represent user intentions for telephone features>
This is a LOTOS specification of a basic POTS system that includes the call forward and originate call screening features but it includes also a user intentions description and verification part. It uses the resource or status oriented style to specify the telephone system but the user intentions are verify using a constraint oriented style.
The first specification corresponds to the one described in the paper presented to FIW'95 in Kyoto Japan.
LOTOS specification using processes to monitor user intentions described using Abstract Data Types
LOTOS specification using Abstract Data Types to monitor user intentions that are themselves represented using Abstract Data Types