Visualization and interpretation of analysis results within the context of formalized UML diagrams

This project complements and extends previous work that has focused on attaching formal semantics to informal graphical object-oriented modeling notations in order to automatically generate formal specifications for a number of target languages (Bourdeau and Cheng, 1995; Wang et al., 1997). My research (Campbell and Cheng, 2000; Campbell et al., 2000; Cheng et al., 2000) builds upon the informal and formal integration work by investigating how commonly used automated analysis techniques, such as simulators, model checkers, rewriting systems, and theorem provers can be combined and used in tandem. The main artifacts that are being analyzed are the formal specifications generated from the informal diagrams. The automated analysis enables a developer to check the system design for various properties, such as freedom from deadlock or constraint satisfaction (i.e, specific conditions are satisfied). The formal semantics for the diagrams also makes it possible to execute the graphical models, via the formal specifications, in order to validate the behavior of the system design.