Ensuring specification correctness by construction

Dieu Donné Okalas Ossami (1) , Jeanine Souquières (1) , Jean-Pierre Jacquot (1)

1 DEDALE - Development of specifications

We propose a process model for the development of formal and semi-formal specifications based on the notions of multi-view states and development operators. A specification state is composed of a UML and a B view. The development of a specification is seen as a sequence of application of operators, which model design decisions and make both views evolve. To produce consistent specifications, we define a consistency relation between views, allowing to define and check operators' correctness. Thus, the development process guarantees that the specification can be safely verified.

Mots clés: correctness; verification; validation; operator; development process; multi-view; UML; B.; consistency

Domaines: Génie logiciel [cs.SE]

Dieu Donné Okalas Ossami, Jeanine Souquières, Jean-Pierre Jacquot. Ensuring specification correctness by construction. 2006. ⟨hal-00104722⟩