UML Formalization: A Position Paper

We take the position that the accessibility, usability and software engineering methodology advantages of modern CASE tools can be combined with the composability, consistency, verifiability and code generation advantages of formal methods. This can be accomplished by adapting the de facto standard CASE tool interface, the Unified Modeling Language (UML), as an open front-end to a formal methods system, Specware. The Specware system has an underlying mathematical model that supports software refinement, component model composability and specification-driven code generation. The integration of UML and Specware can be realized by formalizing UML semantics and automating the process of translating a UML repository into composable logical theories built into Specware. This integration could minimize the human effort needed to produce formalizations by generating them automatically using tools that are already in wide-spread use. Although formal methods can provide a foundation for specification and modeling environments that is more complete, consistent and unambiguous than that produced by traditional or object-oriented methods, they are not commonly used for software engineering. As Anthony Hall [7] states,