The Object Modeling Technique (OMT), a commonly used object-oriented development technique, comprises the object, dynamic, and functional models to provide three complementary views that graphically describe different aspects of systems. The lack of a well-defined semantics for the integration of the three models hinders the overall development process, particularly during the design phase. Previously, we formalized the object model in terms of algebraic specifications. However, the algebraic specifications only capture the static, structural aspects of a system. They do not explicitly describe the behavior, which is critical for system development especially for the design phase. It is necessary to formalize the dynamic model in terms of the structural descriptions in order to specify and verify the system behavior using rigorous techniques. This paper presents a well-defined formal model for both the object and dynamic models and their integration. The formal model is described in terms of a well-known specification language, LOTOS. Formalization of the graphical notation enables numerous automated processing and analysis tasks, such as behavior simulation and consistency checks between levels of specifications.

As the impact of and demand for software increases, there is greater need for rigorous software development techniques that can be used by a typical software engineer. In order to integrate informal and formal approaches to software development, we added formal syntax and semantics definitions to existing object-oriented modeling notations. This formalization enables developers to construct object-oriented models of requirements and designs and then automatically generate formal specifications for the diagrams. This paper describes how the resulting diagrams via their specifications can be analyzed using automated techniques to validate behavior through simulation or to check for numerous properties of the diagrams, including inter- and intramodel consistency.

The data flow diagram (DFD), originally introduced for structured design purposes, depicts the functions that a system or a module should provide. The objective of a software system is to implement specific functionalities. The function-oriented decomposition strategy of DFDs in the conventional design process for structured design conflicts with the spirit of object-orientation. So far, there is no object-oriented method that has successfully integrated DFDs into the object-oriented development process. In this paper, we demonstrate how DFDs can be modified in order to be integrated into object-oriented development. The Object Modeling Technique (OMT) is used as the context for object-oriented development. In addition, a set of formalization rules are proposed to provide formal semantics for DFDs in order to integrate the functional model with the other two models of OMT, namely, the object and dynamic models, in terms of the underlying formal semantics.

The Object Modeling Technique (OMT), a commonly used object-oriented development technique, comprises the object, dynamic, and functional models to provide three complementary views that graphically describe different aspects of systems.The lack of a well-defined semantics for the integration of the three models hinders the overall development process, particularly during the design phase.Previously, we formalized the object model in terms of algebraic specifications.However, the algebraic specifications only capture the static, structural aspects of a system.They do not explicitly describe the behavior, which is critical for system development, especially for the design phase.It is necessary to formalize the dynamic model in terms of the structural descriptions in order to specify and verify the system behavior using rigorous techniques.This paper presents a well-defined formal model for both the object and dynamic models and their integration.The formal model is described in terms of a well-known specification language, LOTOS.Formalization of the graphical notation enables numerous automated processing and analysis tasks, such as behavior simulation and consistency checks between levels of specifications.

This paper describes a graphics-based software development environment that takes advantage of the visual nature of the Object Modeling Technique (OMT) notation and the benefits of formal methods. We have developed a prototype environment, VISUALSPECS, which enables a user to perform object-oriented analysis graphically using the OMT notation. VISUALSPECS generates a formal specification of the object-model, which can be systematically analyzed for completeness and consistency prior to implementation. The formal specifications can be used to guide the formal software. This graphical environment facilitates the development of reliable software using formal methods, enables automated of requirements and design information, and promotes software design reuse based on graphical notations.>