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

[Last updated: Fri Apr 12 10:40:06 CEST 2024]

This directory contains an example for BCG_MIN, CAESAR, CAESAR.ADT,
BCG_STEADY, DETERMINATOR, EVALUATOR, CUNCTATOR, LNT2LOTOS, and SVL.
It describes the formal specification (both in LNT and LOTOS), the
model-checking verification and performance evaluation for the
SCSI-2 bus arbitration protocol.

This example is presented in:
   Hubert Garavel and Holger Hermanns. On Combining Functional
   Verification and Performance Evaluation using CADP.
   Proceedings of the 11th International Symposium of Formal
   Methods Europe FME 2002 (Copenhagen, Denmark), LNCS 2391,
   pages 410-429, July 2002. Full version available as INRIA
   Research Report 4492.

See
   http://cadp.inria.fr/publications/Garavel-Hermanns-02.html
and
   http://cadp.inria.fr/case-studies/02-f-scsi-2.html

In 2016, the specification was translated to LNT by Frederic Lang. The
original LOTOS specification was kept in directory LOTOS.

The functional verification and performance evaluation of the SCSI example
considers three scenarios, respectively noted `A', `B', and `C'. Each
scenario is described and commented in the file "demo.svl".

This demo recomputes the figures 2 and 3 of the Garavel-Hermanns paper,
with minor differences regarding the number of points, the range of
lambda values, etc. Also, the Determinator tool is used instead of
BCG_MIN to speed up computations: as the model generated by Determinator
is already a minimized Continuous-Time Markov Chain, it is no longer
needed to apply BCG_MIN for minimization. This reduces the execution time
by a factor of 8.

   Results/SCSI_*_*.thr throughput data computed by CADP (output)
   Results/SCSI.ps      PostScript file containing throughput figures

LNT files:
   CONTROLLER.lnt       LNT specification of a disk controller
   DISK.lnt             LNT specification of a disk
   NO_DEVICE.lnt        LNT specification of a void SCSI device
   TYPES.lnt            LNT specification of abstract data types
   SCSI_A.lnt           LNT specification (scenario A)
   SCSI_B.lnt           LNT specification (scenario B)
   SCSI_C.lnt           LNT specification (scenario C)
   erlang.lnt           LNT specification of an Erlang distribution
   *.tnt                hand-written C code (external types and functions)
   *.fnt                hand-written C code (external types and functions)
   demo.svl             SVL verification script
   results.pdf		PDF version of the generated file Results/SCSI.ps
 
LOTOS files:
   CONTROLLER.lib       LOTOS specification of a disk controller
   DISK.lib             LOTOS specification of a disk
   NO_DEVICE.lib        LOTOS specification of a void SCSI device
   TYPES.lib            LOTOS specification of abstract data types
   SCSI_A.lotos         LOTOS specification (scenario A)
   SCSI_B.lotos         LOTOS specification (scenario B)
   SCSI_C.lotos         LOTOS specification (scenario C)
   erlang.lotos         LOTOS specification of an Erlang distribution
   *.lib                LOTOS libraries
   *.t                  hand-written C code (external types and functions)
   *.f                  hand-written C code (external types and functions)
   demo.svl             SVL verification script (minimal)
 
The three scenarios can be run (in sequence) by typing
$       svl demo
or even simply
$       svl