A systematic approach to transform OMT diagrams to a B specification

Eric Meyer (1) , Jeanine Souquières (1)

1 DEDALE - Development of specifications

This paper presents a systematic transformation of semi-formal specifications expressed with OMT notations into formal specifications. The object model is first transformed into a specification composed of a set of B machines. Then each component of the dynamic model is transformed and integrated into the previous specification leading to a single specification. Transformations are presented as generic templates. When using these templates, the generated specification is automatically proved within the B prover relatively to the invariant preservation.

Mots clés: omt; formal and semi-formal methods; méthode formelle et semi-formelle; intégration

Domaines: Autre [cs.OH]

Eric Meyer, Jeanine Souquières. A systematic approach to transform OMT diagrams to a B specification. World Congress on Formal Methods in the Development of Computing Systems - FM'99, 1999, Toulouse, France, pp.875-895. ⟨inria-00098957⟩