LSR-IMAG, Grenoble (FRANCE)
Construction of finite labelled transition systems from B abstract systems
CADP (Construction and Analysis of Distributed Processes)
Abstract systems were introduced in 1996 by J-R. Abrial in the
framework of the B method. Like abstract B machines, these systems have
a notion of state, with the difference that operations are replaced by
events, which can be enabled if their guard is true. One of the
enabled events may be fired and the state of the abstract system is
changed according to the event action. Abstract systems can be refined
and dynamic constraints can be specified to state various properties
that are not expressible as invariants. The work presented here aims to
represent the behaviour of B abstract systems and to extract useful
information from this representation. The approach adopted investigates
how behaviours can be interpreted by finite labelled transition systems
(LTSs), which can be analyzed using the CADP verification toolset.
The method consists of decomposing the state of an abstract B system in several cases, by means of disjunctive predicates. These predicates provide the basis for defining the set of states that are the nodes of the LTS, while the events are the transitions of the LTS. The key point of the approach is to compute the transitions which "abstract" the behaviour of the system. This can be done using the B prover, but since the problem is in general undecidable, the process may require human interaction. In practice, an approximation of the abstract system can be automatically computed, by assuming that a transition holds when it cannot be proved or disproved. The approach is illustrated on the B specification of a SCSI-2 input/output system.
The abstraction technique based on disjunctive decomposition provides a
useful way to construct the LTS modelling the behaviour of a B abstract
system. The first outcome is to obtain a graphical view of the system
by using the visualization and simulation facilities offered by CADP.
Another outcome is the possibility of verifying properties on the
finite model without a complete specification of the elements in the
proof by invariant and variant commonly used in B.
D. Bert and F. Cave.
"Construction of Finite Labelled Transition Systems From B Abstract
Systems". In W. Grieskamp, T. Santen, and Bill Stoddart, editors,
Proceedings of the 2nd International Conference on Integrated Formal
Methods IFM'2000 (Dagstuhl Castle, Germany), LNCS vol. 1945,
pp. 235-254, Springer-Verlag, November 2000.
Available on-line from our FTP site in PDF or PostScript
Laboratoire Logiciels, Systèmes, Réseaux (LSR-IMAG)
681, rue de la Passerelle
F-38402 Saint Martin d'Hères Cedex
Tel: +33 (0)4 76 82 72 16
Fax: +33 (0)4 76 82 72 87
|Further remarks:||This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software|