A formal specifications maturity model
Martin D. Fraser, Vijay K. Vaishnavi · Communications of the ACM · 1997
A Formal Specifications MaturityModel software quality and reliability.Hall [8] finds that "[f]rom an economic point of view, therefore, the most important part of a formal development is the system specification."Leveson [9] recognizes the importance of specification: "The first step in any safety verification procedure is to verify that the software requirements are consistent with or satisfy the safety constraints."Later, Bowen and Stavridou [3] observe: "The use of formal methods is becoming important in the process-oriented approach and a basic level of their use would be at the requirements level." Quality, Formal Methods, and ScalabilityPressman [11] identifies four "useful indicators" of software product quality: correctness, maintainability, integrity, and usability.Independently, Hall [8] addresses the first three of these indicators as important characteristics of the software that formal specifications methods can assure.In treating correctness, Hall says that "the relation between a program and its [formal] specification is a formal one and can be proved to be correct."This does not mean that the program is perfect or that the specifications record all requirements but that, to the extent that mathematical modeling captures the essentials of the real world, the program can be assured to satisfy its formal specifications.Hall points to the maintainability benefits of formal specifications when he observes that "[o]ne of the main problems in maintaining software is knowing what it is supposed to do…what each part is supposed to do, and thus what must be preserved as the software is changed.Formal specifications are ideal for this purpose."Formal specifications also provide the opportunity to prove properties of the specification itself: "For safety and security, these may be certain kinds of integrity…requirements." Hall does not specifically address the software characteristic of usability defined by Pressman as "an attempt to quantify 'user friendliness'."Hall does, however, find that formal specifications assure the usability-related characteristic of visibility, that the clients understand what they are buying: "Formality offers ways to ensure the right software is being built."