HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Connect in order to contact the contributor
Submitted on : Tuesday, April 13, 2010 - 9:07:46 AM
Last modification on : Wednesday, June 30, 2021 - 10:14:02 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

71

Files downloads

181