Converting Natural Specifications to Z

Abstract

Formal specification of systems has been an active area of research for quiet some time. In software engineering, the formal specification of the requirement phase is of utmost importance to achieve rigorous development and maintenance of software systems. Despite extensive development over many years and significant demonstrated benefits, formal methods remain poorly accepted by industrial practitioners and natural language remains the first and practical choice of software engineers for specifying the system. The main reason behind the use of natural language for specification writing is the ease of use and power of expression, whereas formal methods are difficult to learn and master. This lack in ease of use is a hindrance to the use of formal methods to their full potential. But the use of formal methods is of utmost importance in safety critical systems. The formal specifications lead to development of high quality software systems. There is a large gap between the actual capability of the formal methods and the purposes for what they are presently being used This thesis presents an approach for conversion of software specifications written in natural language to a formal notation using Z. This will help in exploiting the strength of formal methods, such as their use in software reuse, verification and validation, while keeping intact the ease of use of natural language in specifications. The thesis gives an overview of natural language specifications and formal methods, discussing their respective benefits and drawbacks. Then a system for conversion of natural language specifications to Z is proposed.