Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download

https://hal.inria.fr/inria-00384212
Contributor : Nicolas Stouls <>
Submitted on : Tuesday, April 13, 2010 - 9:07:46 AM
Last modification on : Friday, November 6, 2020 - 3:45:19 AM
Long-term archiving on: : Tuesday, September 14, 2010 - 5:06:01 PM

Files

AFADL04-AvecCopyright.pdf
Files produced by the author(s)

Identifiers

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

Collections

IMAG | CNRS | 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. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL'04), Jun 2004, besançon, France. pp.317--320. ⟨inria-00384212⟩

Share

Metrics

Record views

145

Files downloads

338