-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://cadp.inria.fr

[Last updated: Mon Nov  4 10:58:58 CET 2024]

This directory describes the verification of a CIM (Computer Integrated
Manufacturing) architecture specified in LOTOS.

The LOTOS specification is based on an ACP specification given in [Mauw-90],
which in turn is inspired from an early LOTOS specification [Biemans-Blonk-86].

   [Biemans-Blonk-86] F. Biemans and P. Blonk. "On the formal specification
   and verification of CIM architectures using LOTOS." Computers in Industry,
   7(6), pages 491-504, 1986.

   [Mauw-90] S. Mauw. "Process Algebra as a Tool for the Specification and
   Verification of CIM-architectures." In J.C.M. Baeten, editor, Applications
   of Process Algebra, pages 53-80, Cambridge University Press, 1990.

The verification presented in [Mauw-90] established that the CIM architecture
is branching equivalent to a desired external behaviour. Here we identified a
set of temporal properties of the CIM architecture, expressed in MCL and
verified using the EVALUATOR model checker.

The LOTOS specification was translated to LNT by Hubert Garavel, on the basis
of a student project done by Heinrich Ody (Saarland University, Germany).

The whole verification scenario is described and commented in the file
"demo.svl".  It can be executed by typing:
$       svl demo
or just
$       svl

After execution of the SVL scenario, all generated files can be removed by
typing:
$       svl -clean demo
or just
$       svl -clean