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.
This work was supported by the Office of Naval Research and SPAWAR.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
T. A. Alspaugh et al. Software requirements for the A-7 aircraft. Report 9194, Naval Research Lab, Wash. DC, 1992.
R. J. Anderson et al. “Model checking large software specifications.” Proc. 4th ACM SIGSOFT Symp. Foundations of Software Eng., October 1996.
R. Bharadwaj and C. Heitmeyer. “Model checking complete requirements specifications using abstraction.” Journal of Automated Software Eng. (to appear.
S. Easterbrook and J. Callahan. “Formal methods for verification and validation of partial specifications: A case study.” Journal of Systems and Software, 1997.
S. Faulk et al. “Experience applying the CoRE method to the Lockheed C-130J.” Proc. 9 th Annual Computer Assurance Conf. (COMPASS '94), June 1994.
M. P. E. Heimdahl and N. Leveson. “Completeness and consistency analysis of state-based requirements.” Proc. 17 th Int'l Conf. on Software Eng. (ICSE'95), Seattle, WA, Apr. 1995.
C. Heitmeyer, R. Jeffords, and B. Labaw. “Automated consistency checking of requirements specifications.” ACM Trans. Software Eng. and Method. 5(3), 1996.
C. Heitmeyer et al. “SCR: A toolset for specifying and analyzing requirements.” Proc. 10 th Annual Conf. on Computer Assurance (COMPASS '95), June 1995.
C. Heitmeyer, J. Kirby, and B. Labaw. “Tools for formal specification, verification, and validation of requirements.” Proc. 12 th Annual Conf. on Computer Assurance (COMPASS '97), June 1997.
C. Heitmeyer, J. Kirby, and B. Labaw. “Applying the SCR requirements method to a weapons control panel: An experience report.” Proc. 2nd Workshop on Formal Methods in Software Practice (FMSP'98), St. Petersburg, FL, March 1998.
K. L. Heninger. Specifying software requirements for complex systems: New techniques and their application. IEEE Trans. on Software Eng. SE-6(1), Jan. 1980.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1991.
R. R. Lutz and H.-Y. Shaw. “Applying the SCR requirements toolset to DS-1 fault protection.” Report D15198, Jet Propulsion Lab, Pasadena, CA, Dec. 1997.
S. Miller. “Specifying the mode logic of a flight guidance system in CoRE and SCR.” Proc. 2 nd Workshop on Formal Methods in Software Practice (FMSP'98), St. Petersburg, FL, March 1998.
D. Y. W. Park et al. “Checking properties of safety-critical specifications using efficient decision procedures.” Proc. 2 nd Workshop on Formal Methods in Software Practice (FMSP'98), St. Petersburg, FL, March 1998.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heitmeyer, C., Kirby, J., Labaw, B., Bharadwaj, R. (1998). SCR: A toolset for specifying and analyzing software requirements. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028775
Download citation
DOI: https://doi.org/10.1007/BFb0028775
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive