Skip to main content
SpringerLink
Log in

The Practical Application of Formal Methods: Where Is the Benefit for Industry?

  • Conference paper
Formal Verification of Object-Oriented Software (FoVeOOS 2011)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7421))

  • 602 Accesses

Abstract

Though the use of formal methods for software verification has progress tremendously in the last ten year, its take up in industry has been meager, but with the right emphasis this could change dramatically. Software certification standards have started to take formal methods seriously as an alternative to testing. By focusing on practical issues such as common specification languages, adaption to industrial processes for safety certification, scalability, training, and synergies between tools, common reservations about using formal methods could be lain to rest. This could help formal methods become the center of software engineering in the coming decade.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 49.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  2. Clark, A., Warmer, J. (eds.): Object Modeling with the OCL. The Rationale behind the Object Constraint Language. LNCS, vol. 2263. Springer, Heidelberg (2002)

    MATH  Google Scholar 

  3. Jackson, D.: Alloy: A Logical Modelling Language. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, p. 1. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  4. Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Technical Report TR #98-06t, Department of Computer Science, Iowa State University (2002)

    Google Scholar 

  5. MISRA Consortium. MISRA-C: 2004 — Guidelines for the use of the C language in critical systems (2004)

    Google Scholar 

  6. S. of the SC-205/WG-71 Plenary. DO-330: Software Tool Qualification Considerations (December 2011)

    Google Scholar 

  7. S. of the SC-205/WG-71 Plenary. DO-332: Object-Oriented Technology and Related Techniques Supplement to DO-178C and DO-278A (December 2011)

    Google Scholar 

  8. S. of the SC-205/WG-71 Plenary. DO-333: Formal Methods Supplement to DO-178C and DO-278A (December 2011)

    Google Scholar 

  9. S. of the SC-205/WG-71 Plenary. ED-215: Software Tool Qualification Considerations (January 2012)

    Google Scholar 

  10. S. of the SC-205/WG-71 Plenary. ED-217: Object-Oriented Technology and Related Techniques Supplement to ED-12C and ED-109A (January 2012)

    Google Scholar 

  11. S. of the SC-205/WG-71 Plenary. ED-218: Formal Methods Supplement to ED-12C and ED-109A (January 2012)

    Google Scholar 

  12. S. Plenary. DO-178C: Software Considerations in Airborne Systems and Equipment Certification (December 2011)

    Google Scholar 

  13. S. Plenary. DO-178C: Supporting Information for DO-178C and DO-278A (December 2011)

    Google Scholar 

  14. S. Plenary. DO-278A: Software Integrity Assurance Considerations for Communication, Navigation, Surveillance and Air Traffic Management (CNS/ATM) Systems (December 2011)

    Google Scholar 

  15. S. Plenary. DO-109A: Software Integrity Assurance Considerations for Communication, Navigation, Surveillance and Air Traffic Management (CNS/ATM) Systems (January 2012)

    Google Scholar 

  16. S. Plenary. ED-12C: Software Considerations in Airborne Systems and Equipment Certification (January 2012)

    Google Scholar 

  17. S. Plenary. ED-94C: Supporting Information for ED-12C and ED-109A (January 2012)

    Google Scholar 

  18. Spivey, J.M.: The Z notation: a reference manual. Prentice-Hall, Inc., Upper Saddle River (1989)

    MATH  Google Scholar 

  19. Stepney, S., Cooper, D., Woodcock, J.: An electronic purse: Specification, Refinement and Proof. Technical Monograph PRG–126. Oxford University Computing Laboratory, Programming Research Group (2000)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. aicas GmbH, Haid-und-Neu-Str. 18, D-76131, Karlsruhe, Germany

    James J. Hunt

Authors
  1. James J. Hunt
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Theoretical Informatics, Karlsruhe Institute of Technology, Am Fasanengarten 5, 76131, Karlsruhe, Germany

    Bernhard Beckert

  2. Dipartimento di Informatica, Università di Torino, Italy

    Ferruccio Damiani

  3. Royal Institute of Technology, Stockholm, Sweden

    Dilian Gurov

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hunt, J.J. (2012). The Practical Application of Formal Methods: Where Is the Benefit for Industry?. In: Beckert, B., Damiani, F., Gurov, D. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2011. Lecture Notes in Computer Science, vol 7421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-31762-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-31762-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-31761-3

  • Online ISBN: 978-3-642-31762-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation