-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Fri Jan 5 17:30:56 CET 2024] This directory contains various descriptions in LNT and LOTOS of the link layer protocol (asynchronous part) of the IEEE-P1394 high performance serial bus ("Firewire"). * This example (written in E-LOTOS) is presented in: * Mihaela Sighireanu and Radu Mateescu. Validation of the Link Layer * Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment * with E-LOTOS. In Proceedings of the 2nd COST 247 International Workshop * on Applied Formal Methods in System Design (Zagreb, Croatia), June 1997. * Full version of this paper is available as INRIA Research Report RR-3172. See http://cadp.inria.fr/publications/Sighireanu-Mateescu-97.html and http://cadp.inria.fr/case-studies/97-b-firewire.html Files: scen_correct_[_].lnt protocol description (correct version) scen_orig_[_].lnt protocol description (original version) APPLI.lnt application layer description BUS.lnt bus layer description DATA.lnt data structures description LINK.lnt link layer description TRANS.lnt transaction layer description demos.svl verification scenario written in SVL macros.xtl definitions common to XTL properties req1.seq specification of a diagnostic sequence for property 1 (see notes below) LOTOS/scen_correct_[_].lotos protocol description (correct version) LOTOS/scen_correct_[_].t auxiliary file LOTOS/scen_orig_[_].lotos protocol description (original version) LOTOS/scen_orig_[_].t auxiliary file LOTOS/APPLI.lib application layer description LOTOS/BUS.lib bus layer description LOTOS/DATA.lib data structures description LOTOS/LINK.lib link layer description LOTOS/TRANS.lib transaction layer description The verification scenarios are described in the "demo.svl" file. By typing the command: $ svl demo or even simply $ svl all the LTSs are generated, reduced, and checked automatically. For each of these scenarios, the corresponding LTS is generated (using LNT2LOTOS, CAESAR and CAESAR.ADT), reduced modulo strong equivalence (using BCG_MIN), and the properties written in "spec.xtl" are checked using XTL. The SVL script also checks that LNT and LOTOS specifications are pairwise strongly bisimilar. Notes: - The size of the LTSs depends on the maximal number of nodes connected to the bus (denoted by ) and on the maximal number of requests made by the application layer (denoted by ). If is not present, its value is supposed to be 0 or 1. - In the "spec.xtl" file, the constant "N" must be initialized with the maximal value of (among all scenarios). - For scenario 3, in its original version, the property 1 (deadlock freedom) is false. A diagnostic sequence leading to the deadlock state can be obtained using the EXHIBITOR tool using the following command: $ bcg_open scen3_orig_2_3.bmin.bcg exhibitor < req1.seq which gives the sequence for scenario 3, in its original version, with =2 and =3. Cleanup of the current directory can be obtained by typing: $ svl -clean demo or even simply $ svl -clean