GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel

Abstract : The most expensive source of errors and the more difficult to detect in a formal development is the error during specification. Hence, the first step in a formal development usually consists in exhibiting the set of all behaviors of the specification, for instance with an automaton. Starting from this observation, many researches are about the generation of a B machine from a behavioral specification, such as UML. However, no backward verification are done. This is why, we propose the GeneSyst tool, which aims at generating an automaton describing at least all behaviors of the specification. The refinement step is considered and appears as sub-automatons in the produced SLTS.
Type de document :
Communication dans un congrès
Jacques Julliand. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), Jun 2004, besançon, France. pp.317--320, 2004
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00384212
Contributeur : Nicolas Stouls <>
Soumis le : mardi 13 avril 2010 - 09:07:46
Dernière modification le : jeudi 11 janvier 2018 - 06:14:33
Document(s) archivé(s) le : mardi 14 septembre 2010 - 17:06:01

Fichiers

AFADL04-AvecCopyright.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00384212, version 1
  • ARXIV : 1004.2178

Collections

IMAG | UGA

Citation

Xavier Morselli, Marie-Laure Potet, Nicolas Stouls. GénéSyst : Génération d'un système de transitions étiquetées à partir d'une spécification B événementiel. Jacques Julliand. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), Jun 2004, besançon, France. pp.317--320, 2004. 〈inria-00384212〉

Partager

Métriques

Consultations de la notice

107

Téléchargements de fichiers

257