The Affordable Application of Formal Methods to Software Engineering

摘要

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.