Computer-checked models can be used to prove that core communications and state management in a software program are 100% logically correct. Such models can also be used to generate 100% correct source code. The usage of formal methods can reduce costs and time to market and help to deliver highly reliable software products.
Wayne Lobb will talk about business perspectives on provably-correct software at the Bits&Chips Software Engineering conference.
InfoQ did an interview with Wayne about what makes software complex, how formal methods and models can help us to develop provably-correct software, business advantages of using formal methods and using agile development practices for safety-critical and/or business-critical software.
InfoQ: In your opinion what is it that makes software so complex and hence difficult to make it bug free?
Lobb: Software is difficult partly because it seems easy. Primary school children can write simple programs. But those children cannot design circuits. Hardware in the form of digital circuitry is logic made physical – and difficult to manufacture. Software is logic still fluid, but easy to "manufacture" and change – just type it in and edit it. But logic itself is inherently complex and difficult, whether expressed in software or in hardware. Hardware engineers understood the difficulty decades ago. Circuit designers and testers today rely heavily on automated mathematical tools and algorithms to build, verify and ship bug-free ICs. Software designers and testers can now do the same thing for the same reason, applying the mathematics of formal methods to help build, verify and ship bug-free software.
InfoQ: Can you elaborate on what you mean with provably-correct software?
Lobb: Software source code can be partitioned into three categories: configuration/data, communications/state logic, and algorithms. Algorithms are clearly mathematical and therefore provable. Communications/state logic is provable as well, but this is less obvious. Multi-computer networks, multi-core computers, and multi-threaded software all embody "communicating sequential processes", CSPs, which are mathematically equivalent to the most powerful computational logic known to humanity. We can now use computer-checked models to prove, through formal methods, that core communications and state management in a software program are 100% logically correct, i.e. have no inherent logical flaws such as ignored messages, deadlocks in which two processes wait for each other forever, race conditions, and so forth. Beyond logic errors are implementation (construction) errors such as array overflows; these are different from communications/state logic errors and can be found and fixed using static-analysis tools such as CodeSonar, Coverity, Klocwork and Parasoft.
InfoQ: Can you give some examples of how formal methods and models can help us to develop provably-correct software?
Lobb: There are many. One recent example is the Chord distributed-hash-table protocol for detecting peer nodes in a network. Though the MIT Chord protocol had been studied and used intensively for 10 years, a lightweight run through the MIT Alloy model checker in 2009 discovered several logical errors in it – google "zave chord" (with or without quotes) for more information. NASA uses the Spin model checker to develop and verify Mars rover control software – google "mars code". Toyota, after its debacle with Camry unintended acceleration, adopted the Altran SPARK formal-methods tools to develop reliable software (toyota ada spark). Amazon uses Microsoft TLA+ model checking to ensure cloud data security and integrity via "exhaustively testable pseudocode" (amazon tla+). Aerospace companies use MathWorks StateFlow and other tools to design and verify aircraft software (do-333 case studies).
InfoQ: Can you mention some of the business advantages that formal methods can give?
Lobb: It’s well known that the earlier you find and fix a bug or error during software development, the less expensive and schedule-disruptive the repair usually is. The cost to find and fix a bug before implementation is typically 10 to 100 times lower than finding and fixing it during testing or after deployment. Doing model checking on communications/state designs can find bugs even before a single line of source code gets written. Further, some tools such as Verum Dezyne and Quantum Leaps can generate 100% correct source code in C, C++, Java etc for core communications/state software, saving even more cost and time. Companies like ASML and Philips Healthcare report 40% or greater reduction in costs and time-to-market using formal methods to deliver highly reliable software control products. Of course, such returns do not come for free: your team will have to ramp up, but once that’s done it will pay back over and over again.
InfoQ: How do you feel about using agile development practices for safety-critical and/or business-critical software?
Lobb: To me, "agile" at heart means iterative discovery of actual requirements through user responses to prototypes. In this limited sense agile is absolutely necessary to design (for example) excellent user interfaces including those for safety- and business-critical software products. But once actual requirements are known, I believe that the most cost-effective approach for all but the smallest teams is, first, to specify requirements and designs, in detail and in writing, as soon and as fully as possible and reasonable. Then all involved staff can work confidently and relatively independently – software engineers, test/verification engineers, documentation staff, marketing, regulatory conformance staff, deployment engineering, application engineering, others. Second, I believe that implementation in all cases proceeds best when it’s "agile" in the sense of short iterations, each taking no more than a few weeks, each delivering a well-defined set of functions, but having varying durations depending on the difficulty of the deliverables.
InfoQ: Are there any further resources that you would recommend for people who want to know more about using formal methods in software development?
Lobb: I’d recommend starting with the examples cited above: Amazon for data security and integrity, NASA for control software in extreme environments, Chord for protocol verification, MathWorks StateFlow for aircraft control. Also see supplier/vendor sites including www.event-b.org, www.spinroot.com,www.verum.com, plus dozens of others listed in Wikipedia’s List_of_model_checking_tools. There are hundreds of technical papers and articles about formal methods including model checking. These technologies have been studied for decades. They are mature and solid. It’s only recently, though, that computing power and sophistication have enabled everyday software engineering use of formal methods outside of academic settings. Software engineering is now poised to mature into true engineering in the same way circuit engineering did long ago.
