Abstract
In this paper, we investigate how to represent the behaviour of B abstract systems by finite labelled transition systems (LTS). We choose to decompose the state of an abstract system in several disjunctive predicates. These predicates provide the basis for defining a set of states which are the nodes of the LTS, while the events are the transitions. We have carried out a connection between the B environment (Atelier B) and the Caesar/Aldebaran Development Package (CADP) which is able to deal with LTS. We illustrate the method by developing the SCSI-2 (Small Computer Systems Interface) input-output system. Finally, we discuss about the outcomes of this method and about its applicability. © Springer-Verlag Berlin Heidelberg 2000.
Cite
CITATION STYLE
Bert, D., & Cave, F. (2000). Construction of finite labelled transition systems from B abstract systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1945 LNCS, pp. 235–254). Springer Verlag. https://doi.org/10.1007/3-540-40911-4_14
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
