Formal Methods as Specification and Verification Tools Towards Stable Software Solutions

Abstract

Formal Methods could provide mathematical models for specifying and verifying designs- hardware or software. Early on, formal methods had more acceptance in hardware than software. Employing mathematical models in software to proof correctness or validate requirements reduces or eliminates errors at the early stages of development and also makes testing easier. Formal methods are powerful tools in introducing rigor that would enforce correctness in design specification and help build confidence in design. Indeed, formal method should be seriously considered in safety-critical systems where there is zero tolerance for failure. Formal methods have possibility of gaining magnitude because of the capability to formulate accurate solutions. This work proposes to look into the effects of mathematical models on software system designs from the perspective of formal methods. Trends, benefits, state of the art and future prospects of formal method are considered. Formal methods might require much in terms of implementation, skills and use but there is much benefit in terms of removing design ambiguity and inconsistency and at the same time improving correctness and accuracy.