Evaluation of Formal Specification Languages: UML, Z and RESOLVE

Nalini Iyer

Summer 2003

Mathematics and Computer Science Department

Denison University

Advisor: Dr Joan Krone

Abstract: In today's world of heavy dependence on computer software applications in both domestic households and industries, accuracy and reliability of software systems are key issues. Software malfunctions in monitoring and control systems could lead to crippling blackouts brining life in urban regions to a grinding halt. In medical facilities, space programs and other organizations where safety-critical or mission-critical systems are used, an error could cost billions of dollars and even loss of human lives. Hence in order to ensure the smooth error-free running of operations and to avert catastrophe, it is extremely essential to guarantee that the required software specifications communicated by the client are understood and met with utmost precision by the software engineers. For this purpose the use of natural language alone is inadequate resulting in miscommunication and specifications that are often incomplete, inconsistent and ambiguous.

During the past decade new languages called 'specification languages' have been developed primarily to formalize the process of software specification, and to enable programmers to precisely and unambiguously write software specifications. The Formal Methods approach of Software Engineering uses mathematical notations and theories as a basis for its specification languages to accurately and unequivocally describe system properties and also verify their implementation. Currently two widely used formal specification languages in industry and academia is UML (Unified Modeling Language) and Z. RESOLVE is a newer, less well-known formal specification language that combines both specification and executable constructs into one language. But how successfully do UML, Z and RESOLVE meet the ultimate goals of formal specification languages and Formal Methods? In this research I explored and examined the syntax and semantics of UML, Z and RESOLVE. I then evaluated the capabilities and limitations of each language to specify and verify software system properties.