A formal semantics for object model diagrams

Informal software development techniques, such as the object modeling technique (OMT), provide the user with easy to understand graphical notations for expressing a wide variety of concepts central to the presentation of software requirements. OMT combines three complementary diagramming notations for documenting requirements: object models, dynamic models, and functional models. OMT is a useful organizational tool in the requirements analysis and system design processes. Currently, the lack of formality in OMT prevents the evaluation of completeness, consistency, and content in requirements and design specifications. A formal method is a mathematical approach to software development that begins with the construction of a formal specification describing the system under development. However, constructing a formal specification directly from a prose description of requirements can be challenging. The paper presents a formal semantics for the OMT object model notations, where an object model provides the basis for the architecture of an object oriented system. A method for deriving modular algebraic specifications directly from object model diagrams is described. The formalization of object models contributes to a mathematical basis for deriving system designs