Task T2.3: Experimentations and case studies

1. The paper [GJ01] (D1) describes an experiment in verifying a real industrial protocol for wireless ATM, called MASCARA. Several tools have been used. SDL has been chosen as the specification language and the commercial tool Object-Geode has been used for creating, maintaining and modifying SDL descriptions. The IF tool-set has been used for generation, minimization and comparison of system models and verification of expected properties. All specification and verification tools are connected via the IF language, which has been defined as an intermediate representation for timed asynchronous systems as well as an open validation environment. Due to the complexity of the protocol, static analysis techniques, such as live variable analysis and program slicing, were the key to the success of this verification experiment. The results obtained give some hints concerning a methodology for the formal verification of real systems.
2. The paper [CAS01] (D2) reports on the reachability analysis of fully parametrized models of the IEEE 1394 root contention protocol. This protocol uses timing constraints in order to elect a leader. The interesting point is that the timing constraints involve parameters (transmission delay, bounds of waiting intervals), and the behavior of the protocol strongly depends on the relation between these parameters. The authors use the symbolic reachability techniques implemented in the TReX tool in order to synthesize automatically the parametric constraints which ensure the correctness of the protocol.
3. In [ABS01] (D1), a parametric version of the Bounded Retransmission Protocol of Philips has been automatically analyzed using the tool TREX. The protocol was modeled by means of automata communicating through lossy FIFO channels, and manipulating integer counters and clocks with parametric guards. The analysis requires the manipulating nonlinear arithmetical constraints expressing complex relations between parameters, counters and clocks.
4. In [VR01] (D1), a specification of the PGM protocol is given using the language IF. This work has influenced the definition of the new version of IF [VER01] (D3). Experiments (e.g., simulations) with this specification have been carried out.