Formalizing the framework design language F-UML

Frameworks offer reuse through the generality they have to encompass. This same property, however, often makes a framework design fairly complex, hard to understand and, hence, to reuse. This paper briefly presents the F-UML design. It then focuses on the definition of the formal semantics of F-UML. This latter is defined through a translation of the meta-model of F-UML to Object-Z. The Object-Z semantics allows a designer to prove the syntactic well-formedness of an F-UML design. In addition, it allows the verification of several design properties through a theorem prover.