Database of Case Studies Achieved Using CADP

Plain Ordinary Telephone System (POTS)

Organisation: SICS (Sweden)
INRIA Rhone-Alpes and VERIMAG (France)

Method: LOTOS

Tools used: CADP (Construction and Analysis of Distributed Processes)

Domain: Telecommunications.

Period: 1995

Size: 1760 lines

Description: The POTS (Plain Ordinary Telephone System) is a model of the behaviour of classical telephony systems, often used as a basis for studying the consequences of the introduction of new telephony services.
A formal description in LOTOS of the POTS model was developed by Patrik Ernberg (Swedish Institute of Computer Science), together with a list of 17 requirements that the POTS should satisfy. These requirements have been verified by Laurent Mounier and Hubert Garavel using the CADP toolbox, using various verification techniques :
  • deadlock detection
  • bisimulation equivalences
  • temporal logic and mu-calculus formulas


Conclusions: The POTS case-study successfully illustrates the capabilities of model-based verification, provided by the CADP toolbox. The informal requirements stated by P. Ernberg have been verified using different techniques.

Publications:

Contact:

  1. Patrik Ernberg
    E-mail: [email protected]

  2. Hubert Garavel
    INRIA Rhone-Alpes
    655, Avenue de l'Europe
    F-38330 Montbonnot Saint Martin
    FRANCE
    Tel: +33 4 76 61 52 24
    Fax: +33 4 76 61 52 52
    E-mail: [email protected]

  3. Laurent Mounier
    Verimag
    Centre Equation
    2, avenue de Vignate
    F-38610 Gieres
    FRANCE
    Tel: +33 4 76 63 48 52
    Fax: +33 4 76 63 48 50
    E-mail: [email protected]


Further remarks: The LOTOS description as well as explanations on the verification with CADP are available on-line from: http://cadp.inria.fr/ftp/demos/demo_14

This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Last modified: Thu Feb 11 12:42:30 2021.

Back to the CADP case studies page