-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Mon Nov 4 11:09:10 CET 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