BT

Facilitating the Spread of Knowledge and Innovation in Professional Software Development

Write for InfoQ

Topics

Choose your language

InfoQ Homepage News Developing Provably-Correct Software Using Formal Methods

Developing Provably-Correct Software Using Formal Methods

This item in japanese

Bookmarks

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.

Rate this Article

Adoption
Style

Hello stranger!

You need to Register an InfoQ account or or login to post comments. But there's so much more behind being registered.

Get the most out of the InfoQ experience.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Community comments

  • Typo

    by Jonathan Barbero,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    There is a typo on the title

  • Typo

    by Jonathan Barbero,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    There is a typo on the title

  • Re: Typo

    by Charles Humble,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    Hi Jonathan,
    I can't see a typo in the title. Was it provably (capable of being proven as true or real) that caused confusion or something else?
    Charles
    Head of Editorial, InfoQ

  • Re: Typo

    by Jonathan Barbero,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    Yep, you are right.
    Sorry.

  • Lobb on Proofs and Provable Correctness of Software

    by William Frank,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    Wayne Lobb writes:

    "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."

    I believe that the use of such models, as well as other aspects of provability, has immense unused commercial benefit, as he says, and as Tony Hoare taught us in 1978.

    But, if I am not mistaken,Wayne's characterization of the situation might be misleading. I believe that the functional behavior of distributed systems requires for its description something equivalent for example to a queuing network or a petri net, or at least first order logic. (As Wayne says:'mathematically equivalent to the most powerful computational logic known to humanity.' - in fact, knowable by humans is a stronger and true statement). All these formal models are undecidable, as a matter of mathematical necessity, which means that while we can sometimes, with the abilities that mathematicians have, prove that a given statement about a model is true, we cannot, given an arbitrary statement, assuredly determine in a finite number of steps whether it is true or false. And, as a result, machines will never be able to automatically check, in all cases, whether a program is is correct or not.

    Some of the specific features of the program are decidable -- Wayne mentions type usage, ignored messages, deadlocks, which a machine can check. So, he is right, that there is immense unused capacity to save money and improve quality using machine checkable code. But, unless I am mistaken, to conclude from his message that we will be able to replace people's smarts with machine smarts is wrong.

    As well as seldom known or understood, the importance of undecidability is underestimated. I conclude from Hoare's work not that we should trying to write proofs of software, but that we should let machines do what part of the work they can, and that we write software in a way that is *amenable** to proof, even as we do not write the proofs, because in writing our software this way, we ensure that it is clear and simple. As Hoare most famously says: "Every system is either so simple there are obviously no errors or so complex there are no obvious errors." (how to keep 'systems' simple is the other part of the story.)

  • Lobb on Proofs and Provable Correctness of Software

    by William Frank,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    Wayne Lobb writes:

    "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."

    I believe that the use of such models, as well as other aspects of provability, has immense unused commercial benefit, as he says, and as Tony Hoare taught us in 1978.

    But, if I am not mistaken, Wayne's characterization of the situtation might be misleading. I believe that the functional behavior of distributed systems requires for its description something equivalent for example to a queuing network or a petri net, or at least first order logic. (As Wayne says:'mathematically equivalent to the most powerful computational logic known to humanity.' - in fact, knowable by humans is a stronger and true statement). All these formal models are undecidable, as a matter of mathematical necessity, which means that while we can sometimes, with the abilities that mathematicians have, prove that a given statement about a model is true, we cannot, given an arbitrary statement, assuredly determine in a finite number of steps whether it is true or false. And, as a result, machines will never be able to automatically check, in all cases, whether a program is is correct or not.

    Some of the specific features of the program are decidable -- Wayne mentions type usage, ignored messages, deadlocks, which a machine can check. So, he is right, that there is immense unused capacity to save money and improve quality using machine checkable code. But, unless I am mistaken, to conclude from his message that we will be able to replace people's smarts with machine smarts is wrong.

    As well as seldom known or understood, the importance of undecidability is underestimated. I conclude from Hoare's work not that we should trying to write proofs of software, but that we should let machines do what part of the work they can, and that we write software in a way that is *amenable** to proof, even as we do not write the proofs, because in writing our software this way, we ensure that it is clear and simple. As Hoare most famously says: "Every system is either so simple there are obviously no errors or so complex there are no obvious errors."

  • Re: Lobb on Proofs and Provable Correctness of Software

    by Wayne Lobb,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    My thanks to William Frank, all his points are well taken.

    Model-checkers don’t prove that a *program* is correct, only that the logic in the program’s abstracted and simplified communications *model* has no inherent race conditions, deadlocks and so forth, i.e. no typical concurrency flaws. Model-checkers don’t “prove” correctness in the mathematical sense (and maybe I should have written “verifiably-correct” instead of “provably-correct”). Rather, model-checkers search for counterexamples to the hypothesis “there are no concurrency flaws in this model”, by exhaustively tracing through all possible distinct execution paths through the model (Amazon calls their models “exhaustively testable pseudo-code”). If no counterexample is found, then we can be sure the model has none of the standard concurrency flaws, and we can be sure that the communications “housekeeping” code auto-generated from the model will have none either. This is a limited yet extremely powerful and valuable aspect of correctness, the hardest kind of correctness for humans to achieve in concurrent software.

    William is right, I believe, in saying that machines will not replace humans. Software engineers will still design and develop concurrent systems. But I believe software engineers can and should start routinely using model-checking on concurrent logic, taking advantage of the machine’s ability to race relentlessly through enormous numbers of execution paths to uncover subtle flaws in logic. Even the smallest change to concurrent logic can have far-reaching consequences that are very hard for humans to envision. I believe that competitiveness and sound engineering practice demand use of model-checkers on concurrent logic.

  • Re: Lobb on Proofs and Provable Correctness of Software

    by William Frank,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    Thanks for this clarification, Wayne.

    I think that the problem is not in your use of the word 'proof', but in the expression provably correct software', rather than 'provably correct concurrency and communications", i.e., that the software uses a provably correct distribution model. Which, as you say, is the easiest for people to get wrong, as checking it takes a tedious examination of many many cases -- all possible paths through the distributable elements of the system.

    And, when you say algorithms are mathematical and therefore provable, you are saying something else, because if I am not mistaken, the correctness of an algorithm expressed in any language as rich as first order arithmetic, is, in principle, undecidable, meaning we will succeed in proving some are correct, and that others are incorrect, but there is, as has been mathematically proven, no way to take an arbitrary algorithm and be sure that we will eventually have proven it correct or incorrect.

    It is this undeciability I refer to when I say that we need to write programs that a computer will, in principle, not always be able to prove correct.

    And, when you say: "I believe software engineers can and should start routinely using model-checking on concurrent logic, taking advantage of the machine’s ability to race relentlessly through enormous numbers of execution paths to uncover subtle flaws in logic. " I think that the second way you say it :"ompetitiveness and sound engineering practice ***demand*** use of model-checkers on concurrent logic." is more to the point; In other words, it has become irresponsible, in most situations, NOT to use dynamic model checking when building distributable systems.

  • Re: Lobb on Proofs and Provable Correctness of Software

    by Wayne Lobb,

    Your message is awaiting moderation. Thank you for participating in the discussion.

    William, I intended this business-oriented piece for technical managers and technology executives, so I used the word “software” in the title rather than the more accurate “concurrency and communications” that you suggest.

    In like spirit I wrote that algorithms are provable. You’re right: it’s been proved that we can’t always prove that an arbitrary formally-expressed algorithm is correct or incorrect. In software development practice, though, as I’m sure you know, we rarely even think of proving algorithms beyond the sense of running them through a proving ground. Most are simple enough, or have constrained enough inputs in our particular applications, that we only test their implementations. More complex and critical ones often end up in reference packages or commercial products that others stand behind, for example Fourier transforms, linear programming, statistics, and so forth.

    I view communications and state management as the hard skeleton or timber framing of concurrent software, upon which relatively manageable algorithms and data hang.

    Thanks for saying the main point more forcefully than I did: it’s irresponsible any more *not* to model-check concurrent logic in important software.

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

Allowed html: a,b,br,blockquote,i,li,pre,u,ul,p

BT