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