The affordable application of formal methods to software engineering

ABSTRACT

The purpose of this research paper is to examine (1) why formal methods are required for software systems today; (2) the Praxis High Integrity Systems' Correctness-by-Construction methodology; and (3) an affordable application of a formal methods methodology to software engineering. The cultivated research for this paper included literature reviews of documents found across the Internet and in publications as well as reviews of conference proceedings including the 2004 High Confidence Software and Systems Conference and the 2004 Special Interest Group on Ada Conference. This research realized that (1) our reliance on software systems for national, business and personal critical processes outweighs the trust we have in our systems; (2) there is a growing demand for the ability to trust our software systems; (3) methodologies such as Praxis' Correctness-by-Construction are readily available and can provide this needed level of trust; (4) tools such as Praxis' SparkAda when appropriately applied can be an affordable approach to applying formal methods to a software system development process; (5) software users have a responsibility to demand correctness; and finally, (6) software engineers have the responsibility to provide this correctness. Further research is necessary to determine what other methodologies and tools are available to provide affordable approaches to applying formal methods to software engineering. In conclusion, formal methods provide an unprecedented ability to build trust in the correctness of a system or component. Through the development of methodologies such as Praxis' Correctness by Construction and tools such as SparkAda, it is becoming ever more cost advantageous to implement formal methods within the software engineering lifecycle. As the criticality of our IT systems continues to steadily increase, so must our trust that these systems will perform as expected. Software system clients, such as government, businesses and all other IT users, must demand that their IT systems be delivered with a proven level of correctness or trust commensurate to the criticality of the function they perform.

REFERENCES

• 1: Amey, P. (2002, March). Correctness by Construction: Better can also be cheaper. Crosstalk Magazine. Retrieved 20 April 2005, from http://www.praxis-his.com/pdfs/c_by_c_better_cheaper.pdf.
• 2: Chapman, R. (2004). Correctness by Construction: A TSP-Friendly Approach to Ultra-Low Defect Software. Retrieved 20 April 2005, from http://www.sei.cmu.edu/tsp/tug-2004-presentations/chapman.pdf.
• 3: Chapman, R. (2004, November). SPARK, an Intensive Overview. Proceedings of the SIGADA Conference, 14-18 November.
• 4: Chapman, R. & Hall, A. (2002, Jan). Correctness by Construction: Developing a Commercial Secure System. IEEE Software. Retrieved 20 April 2005, from http://www.praxis-his.com/pdfs/c_by_c_secure_system.pdf.
• 5: Chen, J. (2004, May). The Enterprise: Unwired. 2nd National Software Summit, Reston, VA. Retrieved 20 April 2005, from http://www.cnsoftware.org/nss2report/Chen-NSS2v.3.pdf.
• 6: "Formal Methods." (n.d.). Retrieved 20 April 2005, from http://en.wikipedia.org/wiki/Formal_methods.
• 7: Hoare, T. (2004, August). The Verifying Compiler: a Grand Challenge for Computing Research. High Confidence Software & Systems Conference, March. Retrieved 20 April 2005, from http://research.microsoft.com/~thoare/The_Verifying_Compiler.ppt.
• 8: Knight, J.C. (2004). Correctness by Construction: An Introduction to SPARK Ada. Retrieved 20 April 2005, from http://www.cs.virginia.edu/~jck/cs651/slides/14.correctness.by.construction.pdf.
• 9: Michael, J.B., Voas, J.M., & Linger, R.C. (2004, May). Proceedings of the Center for National Software Studies Workshop on Trustworthy Software, 8-9 April. Retrieved 20 April 2005, from http://www.cnsoftware.org/nss2report/NSS2FinalReport04-29-05PDF.pdf.
• 10: Moore, D., Paxson, V., Savage, S., et. al. (2003). The Spread of the Sapphire/Slammer Worm. Retrieved 20 April 2005, from http://www.cs.berkeley.edu/~nweaver/sapphire/.
• 11: Morgan, T. & Roberts, J. (2002). An Analysis of the Patriot Missile System. Retrieved 20 April 2005, from http://seeri.etsu.edu/SECodeCases/ethicsC/PatriotMissile.htm.
• 12: Praxis High Integrity Systems. (n.d.). Case Study: MULTOS Certification Authority. Retrieved 20 April 2005, from http://www.praxis his.com/services/software/casestudy.asp.
• 13: Praxis High Integrity Systems. (n.d.). Correctness by Construction Approach. Retrieved 20 April 2005, from http://www.praxis-his.com/services/software/approach.asp.
• 14: Praxis High Integrity Systems. (n.d.). Correctness by Construction Principles. Retrieved 20 April 2005, from http://www.praxis-his.com/services/software/principles.asp.
• 15: Wulf, W.A. (2004, May). Do we have a creeping crisis and are we losing our edge? 2nd National Software Summit, Reston, VA. Retrieved 20 April 2005, from http://www.cnsoftware.org/nss2report/Wulf%20Luncheon%20Presentation.pdf.
• 16: Verton, D. (2003, November). Software failure cited in August blackout investigation. ComputerWorld. Retrieved 20 April 2004, from http://www.computerworld.com/securitytopics/security/recovery/story/0,10801,87400,00.html.
• 17: Vienneau, R. (1993, May). A Review of Formal Methods. Retrieved 20 April 2005, from http://www.dacs.dtic.mil/techs/fmreview/definition.html

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Formal methods

General Terms:
Design, Reliability, Security, Verification

Keywords:
correctness, engineering, formal, proven, trust