Developing Specifications by using Operators: a Process to guarantee 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 specifications based on the notions of multi-view state and of operators. A specification state consists of a UML view and a B expression of the same specification. Operators model design decisions as the simultaneous transformation of UML and B descriptions. A specification development is a sequence of applications of operators. We define a notion of coherence of a specification state which allows us to define formally a notion of correctness for operators. Thus, the development process guarantees that the specification can be safely verified and validated.

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

Domaines: Génie logiciel [cs.SE]

Dieu Donné Okalas Ossami, Jeanine Souquières, Jean-Pierre Jacquot. Developing Specifications by using Operators: a Process to guarantee correctness by construction. 2006. ⟨hal-00104266⟩