Calculating with Requirements

Requirements elicitation is concerned with discovering what is wanted; it necessarily depends on social processes such as discussion, introspection, review of documentation, and experimentation. Requirements engineering, on the other hand, is concerned with turning the products of elicitation into precise, unambiguous, and complete descriptions of what the system under consideration is to do. Although they shade into and complement each other, and may be part of a larger iterative process, requirements elicitation and engineering are different activities that need to be supported by different techniques and tools. I maintain that formal methods provide techniques and tools that are appropriate-and effective-for the requirements engineering activity. They are effective because they allow certain questions about requirements to be reduced to calculations, and this is valuable because it allows reviews to be supplemented or replaced by analyses. I am using these terms in the sense in which they are employed in the guidelines for software on commercial aircraft [lo, Section 6.31: reviews are processes that depend on human judgment and consensus, while analyses are objective “mechanical” processes such as testing or calculation. Of course, certain questions do require human judgment, and some decisions require consensus, but many other issues are better addressed by analyses than by reviews: analyses are systematic, can be checked by others, and can even be automated. Especially when automated, analyses can be more reliable and thorough than reviews, and cheaper. Formal methods are often advocated for the intellectual framework that they provide, and the methodological benefits that are believed to accompany their use.