Formal Engineering Methods, International Conference on (1997)

Hiroshima, JAPAN

Nov. 12, 1997 to Nov. 14, 1997

ISBN: 0-8186-8002-4

pp: 304

H. Habrias , IRIN, Nantes, France

B. Griech , IRIN, Nantes, France

ABSTRACT

Deals with the formal specification of dynamic constraints. First of all, we introduce two dynamic constraints which we formally characterise using the B formal specification method. These two dynamic constraints, namely the faithfulness and existence dependency of a binary relationship, are defined using the three mathematical bases of B, viz. predicate logic, set theory and substitution theory. Moreover, we provide for each constraint what is called a proof obligation against which the system's operation specifications must be checked in order to determine whether or not they obey the constraint. This study has raised a general methodology for supporting the specification of a particular type of dynamic constraints in B. The outline of this methodology is presented. We finally show that the constraints we proposed have real-life applications and especially for formally defining the concept of composition in UML (Unified Modeling Language) as an example.

INDEX TERMS

constraint theory; B formal specification method; dynamic constraints; faithfulness; existence dependency; binary relationship; predicate logic; set theory; substitution theory; proof obligation; system operations specifications; composition; UML; Unified Modeling Language; NIAM; Nijssen Information Analysis Method; programming proofs

CITATION

B. Griech and H. Habrias, "Formal specification of dynamic constraints with the B method,"

*Formal Engineering Methods, International Conference on(ICFEM)*, Hiroshima, JAPAN, 1997, pp. 304.

doi:10.1109/ICFEM.1997.630437

CITATIONS