Skip to Main content Skip to Navigation
Reports

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

https://hal.inria.fr/inria-00271164
Contributor : Nicolas Stouls <>
Submitted on : Tuesday, April 8, 2008 - 1:26:17 PM
Last modification on : Tuesday, December 8, 2020 - 10:18:09 AM
Long-term archiving on: : Friday, May 21, 2010 - 1:29:35 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00271164, version 1

Collections

CNRS | LIG | LARA | UGA

Citation

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

Share

Metrics

Record views

321

Files downloads

223