Formal foundations of object-oriented modeling notations
Material type:
Formato de archivo: PDF. -- Este documento es producción intelectual de la Facultad de Informática-UNLP (Colección BIPA / Biblioteca.) -- Disponible también en línea (Cons. 09/03/2009)
In this paper we describe and classifL the different solutions that have been proposed to realize the integration ofgraphic modeling languages, known and accepted by the software developers, with formal modeling languages having analysis and verification tools. Inspired from that classification we define a new integration proposal, based on first-order dynamic logic. The principal benefits ofthe proposedformalization can be summarized asfollows: - The different views on a system are integrated in a single formal model: this allows us to define rules of compatibility between the separate views, on syntactical and semantic level. -Using formal manipulation, it is possible to deduce further knowledge from the specification. -The faults of specifications expressed using a user-friendly notation can be revealed using analysis and verification techniques based on the formal kernel model. The principal diflerence between this model and other object-oriented formal models is that it integrates both of the levels in the architecture of modeling notations into a single conceptual framework. The integration of modeling entities and modeled entities into a single formalism allows us to express both static aspects and dynamic aspects of either the model or the modeled system within a first-order formalism.
3rd International Conference on Formal Engineering Methods, IEEE ICFEM 2000, IEEE Computer Society Press, 101-110, September 2000.