Towards Rigorous Analysis of Fusion Models: The MIRG Experiences

Most popular graphical object-oriented methods (OOMs) provide good mechanisms for handling complexity and constructs that facilitate the creation of abstract, highly-structured models of systems. These qualities make the use of OOMs in the development of complex systems attractive. On the other hand, the models produced by these methods are not amenable to rigorous semantic analysis. Research carried out by the Methods Integration Research Group (MIRG) at Florida Atlantic University on integrating formal specification techniques (FSTs) with less-formal, but richly-structured, graphical OOMs is concerned primarily with developing precise and analyzable counterparts of the models produced by the OOMs. In this paper we give an overview of the current MIRG work on using FSTs to support rigorous analysis of OO models. Specifically, we outline our approach to formalizing Fusion's design and analysis models, and indicate how the formal models can be used to support semantic analysis across requirements and design development stages.