View article

In order to improve software quality, specifiers can take advantage of the use of formal methods in the software development process. With regard to requirements specifications, attempts in this sense have been successfully made. We claim that also in the design phase a formal approach could lead to several benefits, such as the possibility of formally checking if the produced documents satisfy initial requirements. To this purpose we emphasize the role of tools since they provide automatic support to verification. Because of the different aims of the requirements and design specification phases, we believe appropriate the use of two different formal languages for their definition. The above considerations are gathered in the Clepsydra methodology, where a relationship between these early phases of the software development process is introduced, by using Z and Larch as formal languages for requirements …