There is an increasing demand in high-assurance certification of critical software-based systems.
Achieving highest levels of assurance, formal modeling and verification provide a competitive advantage.
At EAL6 and above, the Common Criteria require a formal model of the system to be constructed and key requirements to be formally verified against that model. Formal methods can demonstrate crucial properties of a software-based system such as the security of access control policies or communication protocols.
The supplement D0-333 of RTCA DO-178C provides guidance for using formal methods to support the certification of avionics software systems.
Applied early in the system design process, the deep and precise analysis of critical system properties provides insight that reduces the risk of project failure. Analyzing a formal design model before coding the implementation exhibits flaws early and avoids expensive fixes later in the development process.
Design alternatives can easily be analyzed for their impact on critical system requirements and for the interaction between system features.
Once a formal model covers critical features of a system, it can be used to analyze the impact of changes to these features as the system evolves. Finding regressions on requirements is an automated process, and thus highly cost-effective.
Formal code verification provides the highest possible assurance of the functional correctness of an algorithm and its implementation. It demonstrates the functional correctness and fitness-for-use of complex, highly-optimized or concurrent algorithms, where classical testing may not provide sufficient coverage.
A contract, expressed in a formal logic, precisely describes the functional effect of an algorithm, and the preconditions under which the algorithm can safely be used. Tool supported code verification formally proves that the implementation, in a classical programming language, meets the contract. Client code can be verified to establish the preconditions of the contract whenever the algorithm is used, thus providing assurance that the algorithm is fit-for-use in a specific application context.
Dr.-Ing. Thomas Santen, Diplom-Informatiker
Independent IT consultant
contact@formalassurance.com