Skip to main content
SpringerLink
Log in

On the need for practical formal methods

  • Invited Lectures
  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1486))

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. A fundamental assumption of this paper is that formal methods research has produced several classes of analysis that can prove useful in software development. However, to be useful to software practitioners, most of whom lack advanced mathematical training and theorem proving skills, current formal methods need a number of additional attributes, including more user-friendly notations, completely automatic (i.e., pushbutton) analysis, and useful, easy to understand feedback. Moreover, formal methods need to be integrated into a standard development process. I discuss additional research and engineering that is needed to make the current set of formal methods more practical. To illustrate the ideas, I present several examples, many taken from the SCR (Software Cost Reduction) requirements method, a formal method that software developers can apply without theorem proving skills, knowledge of temporal and higher order logics, or consultation with formal methods experts.

This work was supported by the Office of Naval Research and SPAWAR.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. J. Anderson et al. “Model checking large software specifications.” Proc. 4 th ACM SIGSOFT Symp. Foundations of Software Eng., October 1996.

    Google Scholar 

  2. M. Archer, C. Heitmeyer, and S. Sims. “TAME: A PVS Interface to Simplify Proofs for Automata Models.” Proc. User Interfaces for Theorem Provers 1998 (UITP 98), Eindhoven, Netherlands, July 13–15, 1998.

    Google Scholar 

  3. S. Bensalem, Y. Lakhnech, and Hassen SaÏdi. “Powerful techniques for the automatic generation of invariants.” Proc. 8 th Intern. Conf. on Computer-Aided Verification, CAV ’96, New Brunswick, NJ, July 1996.

    Google Scholar 

  4. S. Bensalem, Y. Lakhnech, and S. Owre. “Computing abstractions of infinite state systems compositionally and automatically.” Proc. 10 th Intern. Conf. on Computer-Aided Verification, CAV ’98, Vancouver, BC, Canada, June–July 1998.

    Google Scholar 

  5. R. Bharadwaj and C. Heitmeyer. “Model checking complete requirements specifications using abstraction.” Automated Software Eng. Journal (to appear).

    Google Scholar 

  6. E. M. Clarke, E. A. Emerson and A. P. Sistla. “Automatic verification of finite-state concurrent systems using temporal logic specifications.” ACM Transactions on Programming Languages and Systems 8(2):244–263, 1986.

    Article  MATH  Google Scholar 

  7. S. Easterbrook and J. Callahan. “Formal methods for verification and validation of partial specifications: A case study.” Journal of Systems and Software, 1997.

    Google Scholar 

  8. 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.

    Google Scholar 

  9. D. Harel. “Statecharts: a visual formalism for complex systems.” Science of Computer Programming 8(1): 231–274, Jan. 1987.

    Article  MATH  MathSciNet  Google Scholar 

  10. M. P. E. Heimdahl and N. Leveson. “Completeness and consistency analysis in hierarchical state-based requirements.” IEEE Trans. on Software Eng. SE-22(6), pp. 363–377, Jun. 1996.

    Article  Google Scholar 

  11. C. Heitmeyer, R. Jeffords, and B. Labaw. “Automated consistency checking of requirements specifications.” ACM Trans. Software Eng. and Method. 5(3), 1996.

    Google Scholar 

  12. 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.

    Google Scholar 

  13. C. Heitmeyer, J. Kirby, B. Labaw, and R. Bharadwaj. “SCR*: A Toolset for specifying and analyzing software requirements.” Proc. 10 th Intern. Conf. on Computer-Aided Verification, CAV ’98, Vancouver, BC, Canada, June–July 1998.

    Google Scholar 

  14. C. Heitmeyer, J. Kirby, and B. Labaw. “Applying the SCR requirements method to a weapons control panel: An experience report.” Proc. 2 nd Workshop on Formal Methods in Software Practice (FMSP’98), St. Petersburg, FL, March 1998.

    Google Scholar 

  15. R. Jeffords and C. Heitmeyer. “Automatic generation of state invariants from requirements specifications.” Proc. 6 th ACM SIGSOFT Symposium Foundations of Software Eng., November 1998 (accepted for publication).

    Google Scholar 

  16. M. Kaufmann and J S. Moore. ACL2: An industrial strength theorem prover for a logic based on common Lisp. IEEE Trans. on Software Eng. SE-23(4), Apr. 1997.

    Google Scholar 

  17. R. Kurshan. Formal verification in a commercial setting. Proc. Design Automation Conference, June 1997.

    Google Scholar 

  18. D. Lending and N. L. Chervany. “CASE tools: Understanding the reasons for non-use,” ACM Computer Personnel 19(2), Apr. 1998.

    Google Scholar 

  19. C. Loiseaux, S. Graf, J. Sifakis, A. Bouajjani, and S. Bensalem. “Property preserving abstractions for the verification of concurrent systems.” Formal Methods in System Design 6, 1–35, 1995.

    Article  MATH  Google Scholar 

  20. G. Lowe. “Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR.” In Tools and Algorithms for the Construction of Systems, Margaria and Steffen, eds., LNCS 1055, Springer-Verlag, 147–166, 1996.

    Google Scholar 

  21. Sam Owre, John Rushby, Natarajan Shankar, Friedrich von Henke. “Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS.” IEEE Transactions on Software Engineering, vol. 21, no. 2, pp. 107–125, Feb. 1995.

    Article  Google Scholar 

  22. 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.

    Google Scholar 

  23. 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.

    Google Scholar 

  24. D. Peled. “A toolset for message sequence charts.” Proc. 10 th Intern. Conf. on Computer-Aided Verification, CAV ’98, Vancouver, BC, Canada, June–July 1998.

    Google Scholar 

  25. S. T. Probst. “Chemical process safety and operability analysis using symbolic model checking.” PhD thesis, Carnegie-Mellon Univ., Pittsburgh, PA, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Naval Research Laboratory, Code 5546, 20375, Washington, DC, USA

    Constance Heitmeyer

Authors
  1. Constance Heitmeyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Anders P. Ravn Hans Rischel

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heitmeyer, C. (1998). On the need for practical formal methods. In: Ravn, A.P., Rischel, H. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1998. Lecture Notes in Computer Science, vol 1486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055332

Download citation

  • DOI: https://doi.org/10.1007/BFb0055332

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65003-4

  • Online ISBN: 978-3-540-49792-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation