An integrated object-oriented and formal modeling environment

Most popular object-oriented analysis (OOA) methods provide good support for creating abstract, understandable models of system behavior and structure, The lack of firm semantic bases for most of these methods makes it difficult to reason rigorously about modeled behavior, It also makes it difficult to check the compliance of implementations (designs and programs) against them. In this article we formalize the Fusion object-oriented analysis modeling techniques to make the models produced more amenable to formal analysis. We illustrate the formalization process by presenting some of the results of a case study carried out as part of our experiments on formalized Fusion models.