How exhaustive static analysis can slash software verification costs and schedule for developers of safety and cybersecurity critical systems

Introduction

In the first post of this series , we discussed why software for safety-critical systems is hitting an “affordability wall,” why reliance on wireless connectivity in those systems is exacerbating the problem, and one way the cost of critical software could be dramatically reduced.

In this post, we’ll explore why industries like aerospace and nuclear energy generation are moving away from traditional software testing and toward exhaustive static analysis and formal verification to solve the problems just mentioned.

This post is Part 2 of a 3-part series derived from TrustInSoft’s latest white paper, “Delivering Safety-Critical Software Faster and Cheaper: How Exhaustive Static Analysis Guarantees Correctness and Security while Reducing Cost and Schedule.” To obtain a FREE copy, CLICK HERE.

A holistic approach to software debugging and verification

Industry experience shows software engineering best practices combined with commercial off-the-shelf (COTS) tools can decrease project development times by up to 25% and reduce associated costs by as much as 80%.[i]

Among the most prevalent COTS tools that offer these kinds of savings for software developers are those for exhaustive static analysis.

Exhaustive static analysis is a methodology that uses formal methods to increase the operational efficiency of development and verification processes. Developed to guarantee the behavior, safety, and reliability of safety-critical systems, exhaustive static analysis can guarantee cybersecurity as well.

Exhaustive static analysis is a framework where a full toolkit of formal methods collaborate. The framework contains algorithms that choose the right formal method according to the question being asked. It can switch seamlessly from one formal method to another, depending on the problem it has been asked to solve.

In other words, exhaustive static analysis is a holistic approach, not one of brute force. Rather than trying to solve every problem using a single formal method, the framework has been designed to determine which combination of formal methods is best suited to solving the problem at hand and to apply those methods in the best way possible.

Drastically improving productivity and code quality while lowering costs

Several prominent companies have been using exhaustive static analysis to increase their software development efficiency and lower costs while following their tested, rigorous safety practices.

In its development of the C-130J Hercules II, for example, Lockheed Martin used a “correctness by construction” development approach that emphasized the use of exhaustive static analysis for verification.[ii] The company reported that they completed their safety-critical software for the project—developed to DO-178B Level A (the highest assurance level)—for half the cost of their non-safety-critical code[iii], [iv] and that they accomplished their verification process for less than a fifth of normal industry costs.[v],[vi] They gained other benefits as well, including an improvement of code quality by a factor of ten over industry norms and a four-fold increase in productivity.[vii]

Following the successful development of the C-130J program, Lockheed Martin used the same principles and methods on a smaller project for the C-27J. The latter required DO-178B Level B safety assurance. Re-using the same process and some of the code, Lockheed Martin realized an additional four-fold improvement in productivity compared to the C-130J, for a 16-fold improvement overall compared to their previous process without exhaustive static analysis.[viii]

A proven technology

The use of formal methods in verifying and certifying safety-critical systems is not new or unproven. Several aerospace did pioneering work in formal methods verification while DO-178 was still in version B. As a result, DO-178C now allows formal verification to replace certain forms of testing.

Since 2001, a group at Airbus has been transferring formal verification technology, tools, and associated methods from research projects to operational teams who develop avionic software. On programs that include the A400M military aircraft and the A380 and A350 commercial aircraft, Airbus has used a process they call “unit proof,” which they developed to verify their code meets its low-level functional requirements.

As the name suggests, unit proof replaces unit testing in Airbus’s process. The use of unit proof was treated as an “alternative method of compliance” under the DO-178B standard, so Airbus worked with their certification authorities to authorize this alternative.[ix] The new DO-178C standard—together with the formal methods supplement DO-333—fully supports the use of unit proof.

Dassault Aviation was another early adopter of formal methods to replace manual testing. Like Airbus, they did so at a time when DO-178B did not fully recognize formal verification. In 2004, Dassault began using formal verification techniques experimentally to replace integration robustness testing on the digital flight control systems for their Falcon business jets.

On flight control software, integration testing is functional, based on pilot-in-the-loop and hardware-in-the-loop activation of the flight control laws. Dassault determined that designing test cases to observe what might happen if some internal “assertions” were to break would be costly and inconclusive. (Assertions are assumptions expected to be met under both normal and abnormal input conditions for the model to operate correctly.) So, they used exhaustive static analysis to perform robustness verification, proving mathematically that both normal and abnormal external inputs can’t lead to assertion failures.[x]

Finally, it’s important to note that the use of formal methods in safety-critical systems has not been limited to the aerospace industry. Between 2001 and 2009, for example, researchers in Korea developed a static analysis toolset that lets nuclear engineers apply formal methods without needing to know the underlying formalisms in depth. Designed to support the development and verification of safety-critical software such as a nuclear power plant’s reactor protection system (RPS), the toolset has proven effective and easy to apply.[xi]

Users are thoroughly convinced of formal methods’ value

There is widespread skepticism towards formal methods tools among engineers who have not used them. Many believe such tools are difficult to use and likely require more effort than they save.

In contrast, engineers who have used formal methods tools tend to be thoroughly convinced of their value.

An international survey conducted between November 2007 and December 2008 on the use of formal methods in safety-critical industrial projects found that, on the whole, formal methods had a beneficial effect on productivity, cost, and quality. Three times as many respondents reported a reduction in schedule, rather than an increase, and five times as many reported reduced costs.[xii]

Overall, 92% of the respondents believed that formal methods had a beneficial effect on quality assurance in safety-critical systems.[xiii]

Benefits of exhaustive static analysis

Exhaustive static analysis can help companies in critical software industries:

• Deal with the challenges of verifying and validating increasingly complex software
• Identify and eliminate most bugs in early phases of development, lowering rework costs
• Guarantee their software is 100% bug-free
• Guarantee their software conforms precisely to its specification
• Provide mathematical proof for certification against both safety and cybersecurity standards
• Reduce discussion and friction with customers and regulatory authorities

Exhaustive static analysis tools are designed to ensure the correctness and reliability of software code. They automate a large portion of code review and catch nearly all coding errors and undefined behaviors (bugs) early in the development process, allowing developers to focus more time and attention on higher-level issues, like whether the code meets its requirements.

Plugs into your existing development process… and transforms it

What’s more, exhaustive static analysis does all this in a way that does not disrupt your current software development process. It brings the value of formal methods to software development in a way that—in most applications—is practically invisible to the user.

With an exhaustive static analysis framework, all the selection and application of the various formal methods are transparent to the developer. From the users’ perspective, they are simply testing their code in a manner that is quite similar to what they’re used to.

The framework expands and automates the testing process. For example, by adding just a couple of lines of code to your test script, you can expand a limited set of test cases into a complete set that covers all possible values for every input variable.

Again, you don’t need a Ph.D. in formal methods to use these tools. Any developer can handle them. For the most part, users don’t even need to be aware of the method the tool is using. They just express the problem, and the tool does the analysis automatically. It’s easy for users to find the answers they need. The framework chooses the right tools for the problem and switches tools on the fly.

For example, our own platform, TrustInSoft Analyzer for C/C++, offers several abstract memory models to analyze the software being validated. It has been painstakingly refined so that no matter how a C/C++ developer programs, the tool will extract the meaning of the code and apply the best formal methods for the problem at hand.

TrustInSoft Analyzer has even been cited in a National Institute of Standards and Technology report to the White House[xiv] for having demonstrated that it can formally guarantee that no known undesired behaviors (bugs) are present in a system. It can also prove that a system behaves precisely according to its specification.

To learn more about TrustInSoft Analyzer, please visit our product page: https://trust-in-soft.com/product/trustinsoft-analyzer/.

This post is Part 2 of a 3-part series derived from TrustInSoft’s latest white paper, “Delivering Safety-Critical Software Faster and Cheaper: How Exhaustive Static Analysis Guarantees Correctness and Security while Reducing Cost and Schedule.” To obtain a FREE copy, CLICK HERE.

In our next post…

In the third and final installment of this series, we’ll look at how our own exhaustive static analysis solution, TrustInSoft Analyzer, has helped four leading developers of safety-critical systems eliminate pesky bugs, guarantee cybersecurity, shorten discussions with customers and regulators over verification and compliance, and reduce verification costs and schedule.

References

[i]      Hawthornthwaite, M. and Marcil, L., Paving the road to DO-178B compliance with COTS tools, VME and Critical Systems, November 2007.

[ii]      Wong, W., Demel, A., Debroy, V. and Siok, M., Safe Software: Does it Cost More to Develop?, IEEE, June 2011.

[iii]      Abts, C., Boehm, B. and Clark, E., COCOTS: A COTS Software Integration Lifecycle Cost Model – Model Overview and Preliminary Data Collection Findings, USC Center for Software Engineering, 2000.

[iv]      Amey, P., Correctness by construction: better can also be cheaper, CrossTalk Journal, March 2002.

[v]      Ibid.

[vi]      Amey, P. and Hilton, A., Practical experiences of safety- and security-critical technologies, Ada User Journal, March 2001.

[vii]      Ibid.

[viii]      Wong, W., Demel, A., Debroy, V. and Siok, M., Safe Software: Does it Cost More to Develop?, IEEE, June 2011.

[ix]      Moy, Y., Ledinot, E., Delseny, H., Wiels, V., Monate, B., Testing or Formal Verification: DO-178C Alternatives and Industrial Experience, IEEE, April 2013.

[x]      Ibid.

[xi]      Yoo, J., Jee, E., Cha, S., Formal Modeling and Verification of Safety-Critical Software, IEEE, May 2009.

[xii]      Woodcock, J., Larsen, P., Bicarregui, J. and Fitzgerald, J., Formal Methods: Practice and Experience, ACM Computing Surveys, October 2009.

[xiii]      Ibid.

[xiv]      Black, P.; Badger, L.; Guttman, B.; Fong, E.; Dramatically Reducing Software Vulnerabilities: Report to the White House Office of Science and Technology Policy; National Institute of Science and Technology (NIST), November 2016.