Formal Engineering Methods, International Conference on (2000)
Sept. 4, 2000 to Sept. 7, 2000
Claudia Pons , Universidad Nacional de La Plata
Gabriel Baum , Universidad Nacional de La Plata
In the paper we describe and classify the different solutions that have been proposed to realize the integration of graphic 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 of the proposed formalization can be summarized as follows: - 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 difference 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.
C. Pons and G. Baum, "Formal Foundations of Object-Oriented Modeling Notations," Formal Engineering Methods, International Conference on(ICFEM), York, England, 2000, pp. 101.