The focus of the roadmap is on verified software, but software does not operate in isolation. It is usually part of a larger system for transportation, energy, telecommunication, banking, commerce, process control, healthcare, or entertainment. The software itself has to be evaluated in the context of the system. In the case of the aborted Ariane-5 launch in 1995, the main error was not that the software failed, but that the system assumed that the software could not fail. Even when some properties of the software have been verified, it is possible that some key properties have been overlooked. For example, can the software recover gracefully from hardware or sensor failure, data corruption, security breaches, unintended feature interaction, communication loss, and other eventualities. Anthony Hall points out that there is principle of unbounded irrelevance where it is not always possible to anticipate and circumscribe the phenomena that are relevant to the operation of a system. As an example, even with verified encryption software running on secure hardware, it is possible to extract information about the key by analyzing the power consumption graph during encryption or decryption. At the system level, when multiple components, including verified software components, are integrated, undesirable behavior can emerge in surprising ways. Software itself is extended and adapted as requirements change, and can be reused in contexts far removed from the one for which it was verified. Verification should therefore be seen as a tool for sharpening skepticism, rather than a means to certitude. Verified software need not be correct software.

Certification

Critical systems containing software need to be certified or assured before they can be deployed. John Rushby has written an extensive report examining the relationship between formal methods and certification.

For the case of software, the certification process consists of

• Standards that specify guidelines for constructing certifiable critical systems and components. Examples of these include the avionics standard DO-178B, the Common Criteria for security-related software, and
• A protection profile which outlines the specific requirements that have to be met in order for system to be certified. This document can include the certification basis as well as the means of compliance. A list of protection profiles is available at
• An evaluation level which states that required depth of evidence (the assurance case) that is required to support the claims for the software.

The National Institute of Standards and Technologies maintains a list of protection profiles for various security-related software components such as operating systems, smart cards, encryption, web servers, switches, and databases.