Formalizing the framework design language F-UML

Author

Bouassida, Nadia ; Ben-Abdallah, Hanêne ; Gargouri, Faïez ; Hamadou, A.B.

Author_Institution

Lab. LARIM, Inst. Superieur d´´Informatique et de Multimedias de Sfax, Tunisia

fYear

2003

fDate

22-27 Sept. 2003

Firstpage

164

Lastpage

172

Abstract

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.

Keywords

formal verification; object-oriented programming; programming language semantics; specification languages; theorem proving; CASE tool set; F-UML design; Object-Z semantics; design properties verification; formal semantics; syntactic well-formedness; theorem proving; unified modeling language; Application software; Computer aided software engineering; Concrete; Formal specifications; Impedance; Logic; Process design; Software architecture; Software engineering; Unified modeling language;

fLanguage

English

Publisher

ieee

Conference_Titel

Software Engineering and Formal Methods, 2003.Proceedings. First International Conference on

Conference_Location

Brisbane, Queensland, Australia

Print_ISBN

0-7695-1949-0

Type

conf

DOI

10.1109/SEFM.2003.1236218

Filename

1236218