How to Construct Formal Arguments that Persuade Certifiers

Developers of a critical system must argue that the system satisfies its critical requirements -- those that, if not satisfied, could result in human injury or death, substantial loss of capital, or the compromise of national security. Documenting an explicit, persuasive assurance argument is especially important when the system produced must be evaluated and approved by an independent certifier, as is often the case for safety- and security-critical systems. Past experience developing independently evaluated systems using formal methods demonstrates that the presentation of the assurance argument is as important as the rigor of the assurance evidence on which that argument is based. Formal specifications and analyses must be presented coherently in the context of the overall system decomposition or much of their power to persuade may be lost. This chapter describes and illustrates a general framework that supports gathering, integrating, presenting and reviewing the evidence that we can trust a system to conform to its critical requirements