Are Formal Methods Ready for Prime Time? The Use of Formal Methods in Development Large Software Systems

摘要

Formal Methods is a term used to describe the use of a formal language for the specification of a software product at some level. The use of a formal language allows requirements to be specified more crisply and less ambiguously than a textual document. It can also allow the developers to formally prove that an implementation meets the specified requirements. Some formal languages can even be transformed into executable code. The use of formal methods is explored for large software projects in commercial enterprises, government, and the military. A comparison is made of the attributes and results of these projects. A table at the end supports the conclusion that formal methods can be successful on a large scale.