This project addresses the difficulties associated with requirements analysis and design by combining object-oriented analysis and design with formal methods. A formalization of an object-oriented diagramming method is being developed, and a framework of rules for reasoning about the meaning of its diagrams is being defined. Diagrams are treated as data type definitions, and the rules enable the automated checking of the consistency of the definitions. The diagramming method comprises three commonly used graphical notations that define the Object Modeling Techniques; (1) object models, (2) data flow diagrams, and (3) state charts, which have been used to perform requirements analysis. As such, the rules defined for these notations provide a formal basis for requirements analysis and allow the rigorously checked diagrams to be used as formal specifications. Diagram composition rules have corresponding proof obligations regarding consistency. Automated techniques are used to determine the consistency and completeness of a system's requirements as depicted by the diagrams. A set of transformation rules for diagrams and their corresponding formal specifications are used to derive designs, guide the implementation process, and validate the developed code. A graphics-based prototype environment is being developed that encapsulates the formalization process and existing specification and program development tools.
