| It is clearly evident that the impact of software is significantly increasing. Accordingly, the need to have high assurance in software's correctness increases for systems where its correct operation is imperative. As a means to facilitate the development of software, formal software specifications are gaining increasing attention as a means to rigorously document requirements and design information since the well-defined notations are amenable to automated processing for numerous analysis tasks, including verification of the correctness of resulting systems. However, attempting to construct a formal specification directly from an informal, high-level requirements document can be challenging. Formal descriptions potentially involve considerable syntactic details and may require careful planning and organization on the part of the developer in order to develop modular (easily-decomposed and amenable to reuse) specifications. In contrast, object-oriented analysis and development techniques, such as the Object Modeling Technique (OMT), comprising diagramming techniques that make use of intuitive and easy to understand graphical notations, are extensively used today. However, the informal nature of the diagramming notations and the lack of well-defined semantics pose the potential to introduce errors in the development process, particularly as the systems become more complicated. The objective of this research is to introduce formal semantics to the graphical notations of OMT, including a formal definition of their integration, and to propose a process to conduct a stepwise formal, rigorous refinement of the diagrams during the design phase. The development process should enable a semi-automated generation of executable formal specifications that can be used to simulate the behavior and check the consistency between levels of specification refinements. |
