Positioning Verfification in the Context of Software/System Certification

Abstract

Formal verification applied to software has been seen as an important focus in research for determining the acceptability of that software for use. However, in examining the requirements for determining the safety of a software intensive system for use in critical situations, it is quite clear that verification plays a role,
but not necessarily a central role. It is entirely possible that a piece of software satisfies its specification, but is unsafe to use. (The first and foremost reason for this is that the program satisfies an unsafe specification.) In this paper we will address the nature of certification in the context of critical systems, decomposing it,
by means of a new philosophical framework, into four aspects: evidence, confidence, determination and certification. Our point of view is that establishing the safety (in a very general sense) of a system is a confidence building exercise much in the same vein as the scientific method; our framework serves as a setting in which we can properly understand and develop such an exercise. We will then place formal verification and assurance cases in this setting, discussing their roles and limitations.
Keywords: Software certification, System certification, Formal specification, Verification,
Critical systems, Safety, Assurance cases, Safety cases