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

Nicolas Stouls 1, *
* Auteur correspondant
1 LIG Laboratoire d'Informatique de Grenoble - VASCO
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.
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00271164
Contributeur : Nicolas Stouls <>
Soumis le : mardi 8 avril 2008 - 13:26:17
Dernière modification le : jeudi 11 janvier 2018 - 01:49:06
Document(s) archivé(s) le : vendredi 21 mai 2010 - 01:29:35

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00271164, version 1

Collections

Citation

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

Partager

Métriques

Consultations de la notice

140

Téléchargements de fichiers

129