Limitations of Formal Methods and An Approach to
Shaoying Liu, Rolf Adams · 1995
Software development using formal methods is be- lieved to be a process of successive refinements from abstract specifications into concrete specifications. Re- finement rules may be used to demonstrate that the concrete specifications satisfy the corresponding ab- stract ones. However, there are serious limitations of the refinement rules in both theory and in prac- tical applications. This paper first uses examples to demonstrate the limitations, and then proposes a new software development model for amprovement based on our experience. The limitations include that (1) the refinement rules are not suficient to guarantee that a refined spec- ification (or concrete specification) satisfy the user's real requirements if it satisfies the abstract speci'ca- tion, (2 the existing refinement rules are not always (3) the refinement rules are difficult to be applied effec- tively an practice due to various kinds of uncertainties and resource constraints. The proposed model suggests that system develop- ment using formal methods should be divided into two phases: a static development phase and a dynamic de- velopment phase, the whole process in each phase in- volving requirements analysis. In order to suit the new model, the existing refinement rules are modified. applica l/ le in theory during the successive refinements,