Limitations of Formal Methods and an Approach to Improvement

Software development using formal methods is believed to be a process of successive refinements from abstract specifications into concrete specifications. Refinement rules may be used to demonstrate that the concrete specifications satisfy the corresponding abstract ones. However, there are serious limitations of the refinement rules in both theory and in practical applications. This paper first uses examples to demonstrate the limitations, and then proposes a new software development model for improvement based on our experience. The limitations include that (1) the refinement rules are not sufficient to guarantee that a refined specification (or concrete specification) satisfy the user's real requirements if it satisfies the abstract specification, (2) the existing refinement rules are not always applicable in theory during the successive refinements, (3) the refinement rules are difficult to be applied effectively in practice due to various kinds of uncertainties and resource constr..