Integrating Informal and Formal Techniques: An Evolutionary Approach to Systems Development

A formal method consists of a well-defined specification language and a rigorously defined set of rules that can be used to reason about the specifications expressed in that language. The specification language is used to describe the intended system behavior. In order to facilitate the use of formal methods for software development, particularly for high-assurance systems, the objective of this project is to produce a set of integrated techniques that support the use of formal methods for all phases of software development. Towards this end, several new techniques and tools are being developed that support the application of formal methods for software engineering. These include tools to support correct program derivation from formal specifications, to formally specify requirements analysis and design information, to determine software reuse based on formal specifications, to reverse engineer existing software to obtain formal descriptions, and to statically analyze requirements specifications for completeness and consistency. Formal specifications can be checked for consistency and completeness using automated techniques. However, during the initial phases of a project, it may be difficult to construct formal specifications directly. In contrast, many developers find it more intuitive to create diagrams to model their systems. As a means to bridge the gap between formal and informal approaches to software development, this research investigates the formalization of a commonly used modeling notation, known as the Object Modeling Technique. The notation comprises three complementary diagrams: object (entity-relation) diagrams, state diagrams, and data flow diagrams. These three diagrams, respectively, model the architecture (static), behavior (dynamic), and data flow and services of a given system. The results of the formalization studies will enable the automated generation of formal specifications from diagrams. The next step is to investigate and develop formal semantics for the integration of the three models. Finally, design transformations are studied that can be applied to the diagrams and the corresponding specifications. ***