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-byConstruction are readily available and can provide this needed level of trust; (4) tools such as Praxis’ SparkAda when appropri...
James F. Davis