Computation of Hierarchical Transition Systems to Document Refined Event-B Models - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Rapport (Rapport Technique) Année : 2008

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

Résumé

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.
Fichier principal
Vignette du fichier
main.pdf (211.12 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

inria-00271164 , version 1 (08-04-2008)

Identifiants

  • HAL Id : inria-00271164 , version 1

Citer

Nicolas Stouls. Computation of Hierarchical Transition Systems to Document Refined Event-B Models. [Technical Report] 2008, pp.10. ⟨inria-00271164⟩
142 Consultations
111 Téléchargements

Partager

Gmail Facebook X LinkedIn More