Print

Kuppusamy, Jothi Malar

Computer Science

2004

M.S.

Software verification is increasingly important as more and more safety and security critical applications emerge and therefore creating a greater demand for high-quality software. Recent studies have shown that software quality problem occur most often during the early lifecycle phases of requirements and design, which can have a lasting impact on the reliability, cost and safety of a system. The most widely used notations to requirement analysis and design include numerous object-oriented techniques. These "informal" methods enable the rapid construction of a system model using intuitive graphics and user-friendly languages. While such techniques have proved to be useful tools, the graphical notations used with these methods are often ambiguous, resulting in diagrams that are easily misinterpreted. The Unified Modeling Language (UML) is a set of description techniques suited for specifying, visualizing, and documenting object oriented systems.
UML in its current version 1.5 is emerging as a de facto industry standard. Although there are approaches for checking the authenticity of UML diagrams, it is not possible to use automated analysis tools to check certain desired properties of an UML design. The overall objective of this research is to develop a mechanism for translating the bulk of a design described in UML into a relational specification. The target relational language is a second-order subset of Z Formal Specification Notation. This language, called np/UML, is a slight extension to the np language used by the automated design checkers nitpick and ladybug. The developed translation will allow structural properties of specifications to be checked by the automated checker, Ladybug. To ensure that the translation is tractable and well defined, some facets of UML are ignored.