Experiments with Formal Methods in Software Engineering

摘要

The industrial take-up of formal methods for software development has, so far,been rather slow. The thesis addresses the reasons for this phenomenon through a number of experiments, each involving the formal method Vienna Development Method (VDM), and its specification language: VDM-SL. The issue of standardization and tool support is discussed. The application of VDM in the framework of a widely used standard for software development is analyzed: DoD-STD-2167A. The relationship between formal methods and the commonly used 'structured' methods for software development is analyzed through examining mappings from data flow diagrams to VDM specifications, and through the construction of a prototype combined structured/formal method, called SVDM, based on one such mapping. SVDM is further illustrated through a case study in which a simple lift system is developed. The research in this thesis shows that the industrial take-up of formal methods can best be pursued through a gradual introduction of formal methods in software processes.