From 3rd IEEE International Symposium on Requirements Engineering.
IEEE Computer Society, Annapolis, MD.
January, 1997.
Pages 144–146.

Requirements elicitation is concerned with discovering what is wanted; it necessarily depends on social processes such as discussion, introspection, 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 is to be achieved by the system under consideration. Formal methods provide techniques and tools that allow some of these engineering questions to be analyzed through calculation.

The talk will describe how techniques such as very strong typechecking, completeness and consistency checking using powerful decision procedures, and model checking, can be applied to requirements engineering. By using these techniques to reduce certain questions of requirements analysis to automated (and therefore fast, cheap, and repeatable) calculations, we can liberate human reviewers to focus on more subtle issues. Experiments with recent Space Shuttle "Change Requests" and other avionics applications will illustrate these points.

@inproceedings{Rushby97:isre,
    AUTHOR = {John Rushby},
    TITLE = {Calculating with Requirements},
    BOOKTITLE = {3rd {IEEE} International Symposium on Requirements Engineering},
    YEAR = {1997},
    PAGES = {144--146},
    ADDRESS = {Annapolis, {MD}},
    MONTH = {jan},
    ORGANIZATION = {{IEEE} Computer Society},
    URL = {http://www.csl.sri.com/papers/isre97/}
}

• isre97-slides.ps.gz
• isre97.dvi.gz
• isre97.ps.gz