An important trend we're anticipating for 2015 is a significant move toward using "Formal Methods" for verifying safety- and security-critical software.

Because they are founded on rigorous mathematics-based techniques and often require help from mathematicians, Formal Methods have long been considered too complex for developers of embedded software. Another drawback was that they also required very extensive changes in the standard software verification strategies.

But the ever-increasing size and complexity of the software needed to control things like trains, aircraft or cars have made standard verification techniques (those mainly based on testing) increasingly more expensive and less effective. Moreover, transportation industries – whether civil or military – are facing rising pressures to deal as effectively with security threats as they do with safety concerns. The truth is, security issues can no longer be ignored when ensuring the safety of transportation software.

To this end, industries like automotive, aerospace and railway are organizing working groups with goals around both safety and security concerns in the system and software lifecycles objectives required by their industry certification standards. A first step already has been accomplished in recent years through the large-scale adoption of static analysis tools such as CodePeer from AdaCore and PolySpace from MathWorks. These static analysis tools detect the presence of typical programming errors. More daring users may attempt to use static analysis tools to prove the absence of such errors, but static analysis tools guaranteeing the detection of all possible errors in specified categories usually come with a fair number of "false positives." In cases where they detect more errors than really exist, the developer must conduct additional analysis to verify that those cases detected by the tools are not truly errors.

In contrast, Formal Methods based on deductive verification (proofs) are not yet used widely in industry, with some notable exceptions. For instance, aviation company Airbus has used Formal Methods for significant parts of the software controlling the A380 and the A350, and the French railway industry has used them for many years.

Deductive-based Formal Methods allow developers to go one step further than static analysis techniques. They guarantee the absence of runtime errors while also allowing verification that a program completely implements its specification. They also provide a better verification than traditional unit testing since the latter verify only a limited number of test cases while the former verify all possible cases. In fact, it is possible to replace some significant parts of the testing by using such Formal Methods while increasing the quality of the overall verification. One issue was still making it impractical: For proofs to be consistent required the formal verification to be achieved on a complete system, which is challenging when some parts of the system are not amenable to such techniques.

AdaCore's Spark 2014 is a good example of a modern language that brings formal proof capabilities and a way to solve this last barrier of entry. Spark 2014 supports contracts that can be either executed or mathematically proved because they can be interpreted as regular SPARK expressions or as first-order logic formulas. With SPARK, users can combine verification techniques based on testing with those based on proofs without having to worry about the frontier between the code that is tested and the code that is formally proved. In other words, if the proof engine is intelligent enough to automatically and completely offer formal verification, some testing is made unnecessary. For areas of code that would require manual proofs and the intervention of mathematicians, standard testing techniques can continue to be used instead, making it possible to introduce such techniques gradually and benefit from them very quickly without having to completely change verification strategies. Spark 2014 and solutions like it are viable for a variety of different usages and scenarios, such as the formal proof of safety properties, complying with standards in regulated industries, performing flow analysis for security, enhancing existing Ada programming language code, combining evidence from proof and test, determining dependency relations, and more.

2015 will be the year of expanding the boundaries of safe and secure programming, and deductive-based Formal Methods will be at the heart of that expansion.

AdaCore

www.adacore.com