HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation

Computation of Hierarchical Transition Systems to Document Refined Event-B Models

Nicolas Stouls 1, *
* Corresponding author
1 VASCO - Validation de Systèmes, Composants et Objets logiciels
LIG - Laboratoire d'Informatique de Grenoble
Abstract : To document a formal model and to explain it to non specialists in formal methods , the usual approach is to use another formalism which does not require any expert skill and which gives a second viewpoint of the same model. According to this approach, we proposed in a previous paper to build a symbolic labelled transition system (SLTS) to describe behaviours of a B model. Extending this work, we now introduce hierarchies in SLTS in order to take into account the refinement process and to exhibit links between description levels. In this paper, we propose a formal definition of hierarchical-SLTS (HSLTS) and we extend the SLTS generation method in order to build a HSLTS which represents behaviours of an even-B refined model.
Complete list of metadata

Cited literature [18 references]  Display  Hide  Download

Contributor : Nicolas Stouls Connect in order to contact the contributor
Submitted on : Tuesday, April 8, 2008 - 1:26:17 PM
Last modification on : Thursday, October 21, 2021 - 3:50:37 AM
Long-term archiving on: : Friday, May 21, 2010 - 1:29:35 AM


Files produced by the author(s)


  • HAL Id : inria-00271164, version 1



Nicolas Stouls. Computation of Hierarchical Transition Systems to Document Refined Event-B Models. [Technical Report] 2008, pp.10. ⟨inria-00271164⟩



Record views


Files downloads