Labelled Transition Systems of B specifications

Organisation:	LSR-IMAG, Grenoble (FRANCE)
Functionality:	Construction of finite labelled transition systems from B abstract systems
Tools used:	B prover CADP (Construction and Analysis of Distributed Processes)
Period:	2000
Description:	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.
Conclusions:	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.
Publications:	[Bert-Cave-00] 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 the CADP Web site in PDF or PostScript
Contact:	Didier Bert Laboratoire Logiciels, Systèmes, Réseaux (LSR-IMAG) Domaine Universitaire 681, rue de la Passerelle B.P. 72 F-38402 Saint Martin d'Hères Cedex France Tel: +33 (0)4 76 82 72 16 Fax: +33 (0)4 76 82 72 87 E-mail: Didier.Bert@imag.fr
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page