A case study on software development using formal methods

This project presents Formal Methods and their usage in the software development process. Formal methods are mathematically based techniques for describing a system. This project is focused on using the Z Specification Language to develop a software system. The Z Specification Language is a tool for defining a system using formal methods.;The software system developed in this project is called the Keyword in Context (KWIC) indexing system. The objective is to develop the system using modularization. This system was introduced by D.L. Parnas (14) as an example of decomposing a system into modules. The data types and the algorithms of the system were defined using the Z Specification Language at the abstract level. It was designed and coded in Pascal and tested using test tools. Refinements were made in order to improve the performance and fix the problems that existed in the system. The results indicated that specifying software system using formal methods is an ideal way to develop it at the abstract level. Using Z helped modularizing the system. Modularization not only improved the flexibility and comprehensibility of the system, but also shortened the development time. Using test tools for testing purposes automated the tests which also affected the development process in terms of time.