Formal Engineering Methods, International Conference on (1997)
Nov. 12, 1997 to Nov. 14, 1997
H. Habrias , IRIN, Nantes, France
B. Griech , IRIN, Nantes, France
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.
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
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.