TitleSCR*: A Toolset for Specifying and Analyzing Software Requirements
Publication TypeConference Paper
Year of Publication1998
AuthorsHeitmeyer, C. L., J. Kirby, Jr, B. Labaw, and R. Bharadwaj
Conference NameComputer-Aided Verification, 10th Ann. Conf. (CAV'98)
Conference LocationVancouver, BC, Canada
Abstract

A controversial issue in the formal methods community is the degree to which mathematical sophistication and theorem proving skills should be needed to apply a formal method and its support tools. This paper describes the SCR (Software Cost Reduction) tools, part of a "practical" formal method--a method with a solid mathematical foundation that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts. The SCR method provides a tabular notation for specifying requirements and a set of "light-weight" tools that detect several classes of errors automatically. The method also provides support for more "heavy-duty" tools, such as a model checker. To make model checking feasible, users can automatically apply one or more abstraction methods.

Full Text

Heitmeyer etal1998.pdf

NRL Publication Release Number

08-1221.1-0878