<p>The question is rather broad.  To answer it in a reasonable space I will make many oversimplifications.</p>

<p>Let us agree on terminology.  A program is <em>correct</em> when it implies its specification.  This vague statement is made precise in many ways, by pinning down what exactly is a program and what exactly is a specification.  For example, in model checking the program is a <a href="http://en.wikipedia.org/wiki/Kripke_structure_%28model_checking%29" rel="nofollow noreferrer">Kripke structure</a> and the specification is often an <a href="http://en.wikipedia.org/wiki/Linear_temporal_logic" rel="nofollow noreferrer">LTL</a> formula.  Or, the program could be a list of PowerPC instructions and the specification could be a set of <a href="http://en.wikipedia.org/wiki/Hoare_logic" rel="nofollow noreferrer">Hoare-Floyd assertions</a> written in, say, <a href="http://en.wikipedia.org/wiki/First-order_logic" rel="nofollow noreferrer">first-order logic</a>.  There are very many possible variations.  It is tempting to conclude that in one case (Kripke structure) we do not verify an actual program, while in the second case (list of PowerPC instructions) we do.  However, it is important to realize we really are looking at mathematical models in both cases, and this is perfectly fine.  (The situation is quite similar to physics where, for example, classical mechanics is a mathematical model of reality.)</p>

<p>Most formalizations distinguish between the syntax and the semantics of a program; that is, how it is represented and what does it mean.  The semantics of a program is what counts from the point of view of program verification.  But, it is of course important to have a clear way of assigning meanings to (syntactical representations of) programs.  Two popular ways are the following:</p>

<ul>
<li>(small step) <em>operational semantics</em>: This is very much like defining a programming language by writing an interpreter for it. For this you need to say what is the <em>state</em>, and it is affected by each statement in the language.  (You may wonder in which language you write the interpreter, but I'll pretend you aren't.)</li>
<li><em>axiomatic semantics</em>: Here each statement type comes with an axiom schema. So, roughly, whenever a particular statement of that type is used, it translates in being able to use certain axioms.  For example, the assignment ${\bf x}:={\bf e}$ comes with the schema $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$; the particular assignment $x:=x+1$ comes with the axiom $\{x+1=1\}\,x:=x+1\,\{x=1\}$ if we instantiate the schema with $P=(x=1)$.</li>
</ul>

<p>(There are others.  I feel particularly bad for omitting denotational semantics, but this answer is already long.)  Machine code plus operational semantics is pretty close to what most people would call a ‘real program’.  Here is a seminal paper, which happens to use operational semantics for a subset of the DEC Alpha machine code:</p>

<ul>
<li>Necula, Lee, <a href="http://scholar.google.co.uk/scholar?q=proof-carrying%20code" rel="nofollow noreferrer">Proof-Carrying Code</a>, 1996</li>
</ul>

<p>Why would you ever use some higher-level semantics, like the axiomatic ones?  When you do not want your proof of correctness to depend on the hardware on which you run.  The approach then is to prove correctness of an algorithm with respect to some convenient high-level semantics, and then prove that semantics sound with respect to lower-level semantics that are closer to actual machines.</p>

<p>In summary, I could think of three reasons that led to your question:</p>

<ol>
<li>You saw only high-level semantics that don't look like what you are used to call a program, and you wonder if there are low-level ones.  The answer is yes.</li>
<li>You wonder how you prove that a model corresponds to reality.  Like in physics, you don't.  You simply come up with better models and check them against reality.</li>
<li>You have not seen the distinction between syntax and semantics, and various ways to assign meanings to programs.  Two <a href="https://cstheory.stackexchange.com/questions/3670/formal-semantics-of-programming-languages">previous</a> <a href="https://cstheory.stackexchange.com/questions/3533/books-on-programming-language-semantics">questions</a> list some books.</li>
</ol>

<p>This answer is merely trying to identify three different ways in which I understood the question.  Going deep in <em>any</em> of these points would require a lot of space.</p>

CC BY-SA 3.0
2012-09-16T21:09:30.217Z
2012-09-16T21:09:30.217Z
2017-04-13T12:32:28.117Z
Radu GRIGore
<p>One approach to reducing the gap between a program and its specification is to use a language with a formal semantics.  An interesting example here would be <a href="http://www-sop.inria.fr/meije/esterel/doc/main-papers.html">Esterel</a>.  Have a look at Gérard Berry's web page for some interesting talks about his work bringing formal methods into the real world.
<a href="http://www-sop.inria.fr/members/Gerard.Berry/">http://www-sop.inria.fr/members/Gerard.Berry/</a></p>

<p>p.s. Been on an Airbus?  You have flown with formal methods!</p>

CC BY-SA 3.0
2012-09-14T15:55:54.563Z
any ref on how airbus uses formal methods would be helpful. (understand that its possibily proprietary info.)
vzn
CC BY-SA 3.0
2012-09-16T06:38:49.040Z
@RossDuncan I found this [web page](http://www.esterel-technologies.com/products/scade-suite/add-on-modules/design-verifier) after going to Berry's web page and a few searches. Is this the formal methods Airbus was using that you were referring to?
Nobody
CC BY-SA 3.0
2012-09-16T16:09:14.780Z
I don't have any inside information regarding Airbus use of Esterel;  my comment simply repeats a remark that Berry made during a lecture.  However this [page](http://www.esterel-technologies.com/technology/success-stories/airbus) trumpets the successful use of the SCADE product with Airbus.  If you look at the history of Esterel, it was adopted by Dassault fairly early on.  Google is your friend.
Ross Duncan
CC BY-SA 3.0
2012-09-16T19:35:40.017Z
Airbus also uses http://www.astree.ens.fr/
Radu GRIGore
CC BY-SA 3.0
2012-09-14T09:18:52.187Z
2012-09-14T09:18:52.187Z
Ross Duncan
<p>The science of building reliable software in the "real world" is still being developed and is to some degree verging on an inherently cultural or anthropological study, because computers and software dont "cause" bugs— humans do! this answer will focus on general Q/A approaches of which formal software verification can be seen as one element.</p>

<p>a remarkable observation is that often software that is "good enough" yet "buggy" can frequently outsell better tested but lower functionality software in the marketplace. in other words, the marketplace does not always put a premium on software quality and the modern techniques of software engineering, which do not always emphasize quality, somewhat reflect that. moreover quality can often add a significant expense to the final product. with those caveats, here are some of the basics:</p>

<ul>
<li><p><strong>redundant/fault tolerant systems.</strong> this is a wide area of study. fault tolerance &amp; redundancy can be designed into the many layers of a system. eg a router, a server, a disk drive, etcetera.</p></li>
<li><p><strong>testing</strong>. all the types— unit testing, integration testing, user acceptance testing, regression testing, etc.</p></li>
<li><p>nowadays <strong>automated testing</strong> via test suites that can be run unattended is more developed/important. test suites running are often coupled with the build tool.</p></li>
<li><p>an important concept in testing is <strong>code coverage</strong>. ie what code is <strong>exercised</strong> by the test. a test cannot find a bug in code that is not "touched" by the test.</p></li>
<li><p>another key concept in testing is <strong>test harnessess</strong> that exercise code that is not easily accessed directly.</p></li>
<li><p>tests should exercise all levels of the software. if the software is well modularized, this is not difficult. higher level tests should penetrate deeply into the code. tests that exercise large amounts of code with small test setup increase <strong>"test leverage"</strong>.</p></li>
<li><p>making the code <strong>as least complicated as possible</strong> is important for testing. testing should be a consideration in the architecture design. often there are multiple ways to implement the same feature yet some have much different implications for test coverage/leverage. for every branch in the code, its often another test case. branches within branches escalate to exponential increase in code paths. therefore avoiding highly nested/conditional logic improves ability to test.</p></li>
<li><p>studying <strong>famous (massive) software failures</strong> of which there are many examples &amp; case studies is helpful for understanding the history and developing a mindset oriented towards quality considerations.</p></li>
<li><p>one can get carried away with testing! there is both a problem with <strong>too little or too much</strong> testing. there is a "sweet spot". the software cannot be successfully built in either extreme.</p></li>
<li><p>use all the basic tools in the most effective way. debuggers, code profilers, test code coverage tools, defect tracking system, etc! do not necessarily commit to fixing, but <strong>track</strong> even the smallest defects in the tracking software. </p></li>
<li><p>careful use of SCM, source code management, and <strong>branching</strong> techniques is important in avoiding regressions, isolating and progressing fixes, etc</p></li>
<li><p><strong><a href="http://gse.ufsc.br/~bezerra/disciplinas/Confiabilidade/docs/n-versionprogramming.pdf" rel="nofollow">N-version Programming</a></strong>: a practice used often for developing Mission Critical Software. The premise of this practice is that N independently developed programs are unlikely to have the same common bug / fault. This has been criticized in a few <a href="http://sunnyday.mit.edu/critics.pdf" rel="nofollow">papers</a> . <a href="http://en.wikipedia.org/wiki/N-version_programming" rel="nofollow">NVP</a> is, however, a practice not a theoretical concept.</p></li>
</ul>

<p>I believe physicist Feynman has some account of the method that NASA used to guarantee reliability of the space shuttle systems in his book "What do you care what other people think?" — he said they had two teams, say Team A and Team B. team A built the software. team B took an adversarial approach to Team A and tried to break the software. </p>

<p>it helps if Team B has good software engineering background, ie themselves can write code harness/programmatic tests etcetera. in that case Team B had almost equal level of resources as Team A. on the other hand, this approach is expensive because it can nearly double the cost of building the software. more typically, there is a smaller QA team compared to the development team.</p>

CC BY-SA 3.0
2012-09-17T11:32:13.807Z
Someone should check your OS for correctness with respect to the specification that pressing the Shift key and a letter produces a capital letter.
Andrej Bauer
CC BY-SA 3.0
2012-09-18T20:40:24.767Z
addendum: schedule constraints can impact quality. see also [project mgt triangle](http://en.wikipedia.org/wiki/Project_management_triangle) composed of scope, cost, schedule with quality the "area" affected by all 3. see also ["Why can't the IT industry deliver large, faultless projects quickly as in other industries?"](http://programmers.stackexchange.com/questions/158640/why-cant-the-it-industry-deliver-large-faultless-projects-quickly-as-in-other). did not add the N-Version item myself [its covered other answer] but note Feynman mentioned that NASA used it also in the space shuttle design.
vzn
CC BY-SA 3.0
2012-09-18T21:27:37.223Z
also, ["why isnt software as reliable as a car"?](http://programmers.stackexchange.com/questions/41050/why-isnt-software-as-reliable-as-a-car)
vzn
CC BY-SA 3.0
2012-09-19T02:26:20.350Z
another interesting case study is the [mars rover](http://programmers.stackexchange.com/questions/159637/what-is-the-mars-curiosity-rovers-software-built-in) which has large amts of code, much of it autogenerated. in that case prior rovers field tested most of the software & it was reused.
vzn
CC BY-SA 3.0
2012-09-12T15:27:02.780Z
2012-09-17T11:05:06.887Z
2012-09-17T11:05:06.887Z
vzn
<p>An old approach (but it is still used in some applications) is the <a href="http://en.wikipedia.org/wiki/N-version_programming">N-version programming</a></p>

<p>From Wikipedia:</p>

<p><strong>N-version programming</strong> (<strong>NVP</strong>), also known as <em>multiversion programming</em>, is a method or process in software engineering where multiple functionally equivalent programs are independently generated from the same initial specifications. The concept of N-version programming was introduced in 1977 by Liming Chen and Algirdas Avizienis with the central conjecture that the "independence of programming efforts will greatly reduce the probability of identical software faults occurring in two or more versions of the program".The aim of NVP is to improve the reliability of software operation by building in fault tolerance or redundancy.<br>....</p>

<p>See for example: "<a href="http://www.iaeng.org/IJCS/issues_v35/issue_4/IJCS_35_4_07.pdf">Challenges in Building Fault - Tolerant Flight Control System for a Civil Aircraft</a>"</p>

CC BY-SA 3.0
2014-04-28T09:25:56.553Z
It's worth noting that n-version programming *does not work*. The fundamental assumption -- namely, that errors in repeated trials of the software development process are independent -- is *completely false*. This idea makes no sense theoretically (a difficult-to-implement algorithm won't get magically easier for a second independent team), and it's been debunked experimentally, too: John Knight and Nancy Leveson's experiment showing that the independence assumption is not statistically valid is one of the most famous papers in software engineering.
Neel Krishnaswami
CC BY-SA 3.0
2014-04-28T10:11:14.863Z
@NeelKrishnaswami: I agree! However I think (but I'm not an expert) that *does not work* should be replaced with *it doesn't improve reliability as much as it should if compared with other approaches*. Citing K&L: "*... We never suggested that our result should be used by utself as a basis for a decision about the effectiveness of N-version programming. We merely suggested that caution would be appropriate ...*". I think that the debate on how much the NVP approach can be useful for critical system design is still open (see the recent work of Khoury et al.)
Marzio De Biasi
CC BY-SA 3.0
2012-09-12T14:36:07.147Z
2012-09-12T14:36:07.147Z
Marzio De Biasi
<p>Two or three years ago I started taking a look to formal methods applied to software. This was a quest driven by curiosity, and by the feeling that I had to learn programming tools and methods with longer time-spans. Although I dreamed wishfully about a <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.315" rel="nofollow">Silver Bullet</a>, I really thought that there was not an answer to the question: "How can I write a correct program?".</p>

<p>At this point of the quest after trying some tools (Z, B, VHDL, and Estelle), I'm using <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html" rel="nofollow">TLA+</a>. This is a variant of temporal logic with software tools for model checking and mechanic proofs. I think that I choose this approach because L. Lamport was behind it, the syntax was simple, there were lots of examples, there was a community taking care of it, and the language and tools were fairly well documented.</p>

<p>Regarding my initial question, I think that there is not a complete answer. However, it is worth learning that it pays off to specify formally some portions of a system. It is also pretty useful to reverse engineer some complex ones. That is, It is effective to create a blueprint for the difficult and critical parts. However, I don't think there is an effective method to translate automatically the specification to a programming language or framework (unless you restrict the project to a very specific environment). I also do not think that having a formal specification should prevent you from testing the software.</p>

<p>In a nutshell, I think that the following metaphor (from Lamport) is really powerful: "Do you expect a house to be automatically build from a blueprint? Will you buy a house that is not yet build and it does not have blueprint?".</p>

<p>During this quest, I have found the following resources useful:</p>

<ul>
<li><a href="http://rads.stackoverflow.com/amzn/click/1905209347" rel="nofollow">Software Specification Methods</a>. This book provides a broad overview of the existing methods and tools. There you can find basic explanations and examples of Z, SDL, TLA+, Petri Nets, Coq, etc.  </li>
<li>If you think that TLA+ fits your needs, I really recommend the book <a href="http://research.microsoft.com/en-us/um/people/lamport/tla/book.html" rel="nofollow">Specifying Systems</a>. You can get the book for free, and it comes with examples to play with :). </li>
<li>Recently, I read a couple of related articles that give two different perspectives to the state of the art of the formal methods: <a href="http://permalink.gmane.org/gmane.comp.encryption.general/14818m" rel="nofollow">The Case for Formal Methods</a>, and <a href="http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext" rel="nofollow">Formally Verified Mathematics</a>.</li>
</ul>

<p>Good luck!</p>

CC BY-SA 3.0
2014-04-27T22:27:57.710Z
2014-04-27T22:27:57.710Z
marcmagransdeabril
<p>The answers so far covered already most of what should be said about the foundations of how relate specification and code to each other. I just want to add a more practical point that approaches the question in the header of this thread: </p>

<p>How create mission critical software? </p>

<p>There exists tools that automatically analyze your code for errors (violations of the specification, or "typical bugs"). To my knowledge, these methods mostly build on static analysis and are not immediately related to the theories you mentioned (LTL/CTL/...), but they do find errors in real code and it is already feasible, from a practical point of view, to use such tools in industrial projects. I personally have not used many of them, but it seems that these tools start being accepted by practitioners. For further reading, I can recommend the following blog article:</p>

<p><a href="http://www.altdevblogaday.com/2011/12/24/static-code-analysis/" rel="nofollow">http://www.altdevblogaday.com/2011/12/24/static-code-analysis/</a></p>

CC BY-SA 3.0
2012-09-19T17:47:49.110Z
example implementation with java, open source apache— [findbugs](http://findbugs.sourceforge.net/)
vzn
CC BY-SA 3.0
2012-09-19T16:58:57.553Z
2012-09-19T16:58:57.553Z
Markus
<blockquote>
  <p>But then how to verify that the software (not only the specification) is indeed correct?</p>
</blockquote>

<p>Unit testing? Write a test for every single requirement in the spec, and then test every single method in your implementation to see that its output/input conforms to said spec. This can be automated so that these tests are run continuously to ensure no change ever breaks previously working features.</p>

<p>Theoretically speaking, if your unit tests have 100% code coverage (i.e. every single method in your code is tested) your software should be correct, provided the tests themselves are accurate and realistic.</p>

CC BY-SA 3.0
2012-09-12T13:23:29.540Z
For any reasonably complex program, code coverage (by testing) cannot ensure correctness.  You would have to cover all possible executions; all lines of code is _not_ enough.
Radu GRIGore
CC BY-SA 3.0
2012-09-12T13:53:33.893Z
Code coverage is too vague a concept. We distinguish between, e.g. method coverage, statement coverage, branch coverage, path coverage and so on. As Radu points out, for non-trivial programs, testing often runs into combinatoral explosions. That said, aeronautics software has a pretty great track record, and its correctness is often based on extensive testing.
Martin Berger
CC BY-SA 3.0
2012-09-12T14:00:39.607Z
If you mean testing by tools like JUnit, this kind of standard automatic testing can not cover every cases (unless the program is extremely small). For typical application, this kind of testing is typically enough. But for mission critical application, I don't know whether this is enough (or not).
fajrian
CC BY-SA 3.0
2012-09-12T16:10:42.033Z
think this answer is being unfairly penalized. suspect formal verification methods that work with infinite and not finite cases are excellent areas of academic study but possibly not used frequently or widely in industry. ie there may be a divergence/gap between what academics & industry practitioners see as "enforcing correctness"
vzn
CC BY-SA 3.0
2012-09-12T16:42:56.860Z
@vzn: In my experience, there is remarkable agreement between what is considered to be a bug by academics and, respectively, practitioners.  Also, I bet that most of my (former) colleagues from industry would agree that "every single method in your code is tested" does not sound very reassuring. (And, no, I did not downvote. I almost never do.)
Radu GRIGore
CC BY-SA 3.0
2012-09-12T16:46:52.860Z
@radu, a straw man. did not assert otherwise. merely asserted that the focus, emphasis, or approaches may be different between theoretical study & practice/application in the "real world"[TM]. eagerly awaiting your own constructive answer.
vzn
CC BY-SA 3.0
2012-09-12T16:58:16.040Z
@vzn: Did I say you said otherwise? I was simply trying to explain why I believe that others are not upvoting this answer. At this time I cannot answer this question, because I don't understand it.
Radu GRIGore
CC BY-SA 3.0
2012-09-12T13:18:41.610Z
2012-09-12T13:18:41.610Z
gillesv
<p><em>Certifying algorithms</em> can be useful when building mission critical software. </p>

<blockquote>
  <p>A certifying algorithm is an algorithm that produces, with each
  output, a certiﬁcate or witness (easy-to-verify proof) that the
  particular output has not been compromised by a bug.</p>
</blockquote>

<p>Read more in this survey paper <a href="http://www.cs.colostate.edu/~rmm/cert11.pdf" rel="nofollow">Certifying algorithms
by McConnell, R.M. and Mehlhorn, K. and Naher, S. and Schweitzer, P.</a></p>

CC BY-SA 3.0
2012-09-18T18:17:20.497Z
In 1998, Pnueli, Siegel and Singerman described this idea applied to compilers, under the name _translation validation._ Compilers are inherently higher-order (the input is a program, the output is a program), so they tend to be hard to verify.  But there are crazy people like X. Leroy who develop verified compilers anyway. (Crazy in the best possible sense!)
Radu GRIGore
CC BY-SA 3.0
2012-09-18T03:24:47.940Z
2012-09-18T03:24:47.940Z
Pratik Deoghare
<p>I am self learning formal methods. I heard that formal methods is used (and usually only used) to create mission critical software (such as nuclear reactor controller, aircraft flight controller, space probe controller). That's why I am interested to learn it :p</p>

<p>However, after learning formal methods (especially LTL, CTL and their siblings), I feel that they can only be used to verify the correctness of the specification (safety, liveness, fairness, etc).</p>

<p>But then how to verify that the software (not only the specification) is indeed correct?</p>

<p>Disclaimer: I am a 90% idiot when it comes to theoretical computer science. So please be merciful while answering.</p>

CC BY-SA 3.0
2012-09-12T09:57:23.983Z
What do you exactly mean with _"...that the software is indeed correct..."_? Which of the following 2 do you mean: **1)** The software is adherent with the specification **2)** Specific blocks of code respect some given property or some input - output relationship.
Giorgio Camerani
CC BY-SA 3.0
2012-09-12T10:44:04.643Z
@GiorgioCamerani : The first one
fajrian
CC BY-SA 3.0
2012-09-12T13:19:04.213Z
Correctness of a program usually means that (1) it is consistent with a specification and (2) it never crashes.  Point (1) is really a statement about the pair (program, specification) rather than about the program in itself.  A further complication is that ‘program’ is usually a shorthand for ‘model of a program’, because programs themselves are rather too complicated or do not have precise semantics. Given this, I _think_ you are asking about the gap between a program and its model, but I'm not quite sure.
Radu GRIGore
CC BY-SA 3.0
2012-09-12T13:52:35.357Z
@RaduGRIGore: Actually I don't understand what "model" is. But I think you address my question quite closely. Basically, what I am wondering is the gap between specification and the program source code. Many stupid things can happen when programmers (like me) are implementing the specification.
fajrian
CC BY-SA 3.0
2012-09-12T16:21:16.537Z
@fajrian: I suspect that you say ‘specification’ for what I would call ‘model’.  There are tools that work on programs written in languages like C or Java, or even machine code.  (It is still a model, though, as they have to assume some semantics, which _should_, but may not, correspond to what the compiler/processor does.)
Radu GRIGore
<program-verification><formal-methods><se.software-engineering>
How to Create Mission Critical Software?
fajrian
# How to Create Mission Critical Software?

(Asked by: username_0 on 2012-09-12)

I am self learning formal methods. I heard that formal methods is used (and usually only used) to create mission critical software (such as nuclear reactor controller, aircraft flight controller, space probe controller). That's why I am interested to learn it :p

However, after learning formal methods (especially LTL, CTL and their siblings), I feel that they can only be used to verify the correctness of the specification (safety, liveness, fairness, etc).

But then how to verify that the software (not only the specification) is indeed correct?

Disclaimer: I am a 90% idiot when it comes to theoretical computer science. So please be merciful while answering.

**Tags:** program-verification, formal-methods, se.software-engineering
> **Comments:**
> **username_1**: What do you exactly mean with _"...that the software is indeed correct..."_? Which of the following 2 do you mean: **1)** The software is adherent with the specification **2)** Specific blocks of code respect some given property or some input - output relationship.  
> **username_0**: @GiorgioCamerani : The first one  
> **username_2**: Correctness of a program usually means that (1) it is consistent with a specification and (2) it never crashes.  Point (1) is really a statement about the pair (program, specification) rather than about the program in itself.  A further complication is that ‘program’ is usually a shorthand for ‘model of a program’, because programs themselves are rather too complicated or do not have precise semantics. Given this, I _think_ you are asking about the gap between a program and its model, but I'm not quite sure.  
> **username_0**: @RaduGRIGore: Actually I don't understand what "model" is. But I think you address my question quite closely. Basically, what I am wondering is the gap between specification and the program source code. Many stupid things can happen when programmers (like me) are implementing the specification.  
> **username_2**: @fajrian: I suspect that you say ‘specification’ for what I would call ‘model’.  There are tools that work on programs written in languages like C or Java, or even machine code.  (It is still a model, though, as they have to assume some semantics, which _should_, but may not, correspond to what the compiler/processor does.)  

---

## 8 answers

### Answer by username_2 on 2012-09-16. Score: 11

The question is rather broad. To answer it in a reasonable space I will make many oversimplifications.

Let us agree on terminology. A program is *correct* when it implies its specification. This vague statement is made precise in many ways, by pinning down what exactly is a program and what exactly is a specification. For example, in model checking the program is a [Kripke structure](http://en.wikipedia.org/wiki/Kripke_structure_%28model_checking%29) and the specification is often an [LTL](http://en.wikipedia.org/wiki/Linear_temporal_logic) formula. Or, the program could be a list of PowerPC instructions and the specification could be a set of [Hoare-Floyd assertions](http://en.wikipedia.org/wiki/Hoare_logic) written in, say, [first-order logic](http://en.wikipedia.org/wiki/First-order_logic). There are very many possible variations. It is tempting to conclude that in one case (Kripke structure) we do not verify an actual program, while in the second case (list of PowerPC instructions) we do. However, it is important to realize we really are looking at mathematical models in both cases, and this is perfectly fine. (The situation is quite similar to physics where, for example, classical mechanics is a mathematical model of reality.)

Most formalizations distinguish between the syntax and the semantics of a program; that is, how it is represented and what does it mean. The semantics of a program is what counts from the point of view of program verification. But, it is of course important to have a clear way of assigning meanings to (syntactical representations of) programs. Two popular ways are the following:

* (small step) *operational semantics*: This is very much like defining a programming language by writing an interpreter for it. For this you need to say what is the *state*, and it is affected by each statement in the language. (You may wonder in which language you write the interpreter, but I'll pretend you aren't.)
* *axiomatic semantics*: Here each statement type comes with an axiom schema. So, roughly, whenever a particular statement of that type is used, it translates in being able to use certain axioms. For example, the assignment ${\bf x}:={\bf e}$ comes with the schema $\{P[{\bf x}/{\bf e}]\}\,{\bf x}:={\bf e}\,\{P\}$; the particular assignment $x:=x+1$ comes with the axiom $\{x+1=1\}\,x:=x+1\,\{x=1\}$ if we instantiate the schema with $P=(x=1)$.

(There are others. I feel particularly bad for omitting denotational semantics, but this answer is already long.) Machine code plus operational semantics is pretty close to what most people would call a ‘real program’. Here is a seminal paper, which happens to use operational semantics for a subset of the DEC Alpha machine code:

* Necula, Lee, [Proof-Carrying Code](http://scholar.google.co.uk/scholar?q=proof-carrying%20code), 1996

Why would you ever use some higher-level semantics, like the axiomatic ones? When you do not want your proof of correctness to depend on the hardware on which you run. The approach then is to prove correctness of an algorithm with respect to some convenient high-level semantics, and then prove that semantics sound with respect to lower-level semantics that are closer to actual machines.

In summary, I could think of three reasons that led to your question:

1. You saw only high-level semantics that don't look like what you are used to call a program, and you wonder if there are low-level ones. The answer is yes.
2. You wonder how you prove that a model corresponds to reality. Like in physics, you don't. You simply come up with better models and check them against reality.
3. You have not seen the distinction between syntax and semantics, and various ways to assign meanings to programs. Two [previous](https://cstheory.stackexchange.com/questions/3670/formal-semantics-of-programming-languages) [questions](https://cstheory.stackexchange.com/questions/3533/books-on-programming-language-semantics) list some books.

This answer is merely trying to identify three different ways in which I understood the question. Going deep in *any* of these points would require a lot of space.


---

### Answer by username_3 on 2012-09-14. Score: 8

One approach to reducing the gap between a program and its specification is to use a language with a formal semantics. An interesting example here would be [Esterel](http://www-sop.inria.fr/meije/esterel/doc/main-papers.html). Have a look at Gérard Berry's web page for some interesting talks about his work bringing formal methods into the real world.
<http://www-sop.inria.fr/members/Gerard.Berry/>

p.s. Been on an Airbus? You have flown with formal methods!

> **Comments:**
> **username_4**: any ref on how airbus uses formal methods would be helpful. (understand that its possibily proprietary info.)  
> **username_5**: @RossDuncan I found this [web page](http://www.esterel-technologies.com/products/scade-suite/add-on-modules/design-verifier) after going to Berry's web page and a few searches. Is this the formal methods Airbus was using that you were referring to?  
> **username_3**: I don't have any inside information regarding Airbus use of Esterel;  my comment simply repeats a remark that Berry made during a lecture.  However this [page](http://www.esterel-technologies.com/technology/success-stories/airbus) trumpets the successful use of the SCADE product with Airbus.  If you look at the history of Esterel, it was adopted by Dassault fairly early on.  Google is your friend.  
> **username_2**: Airbus also uses http://www.astree.ens.fr/  

---

### Answer by username_4 on 2012-09-12. Score: 7

The science of building reliable software in the "real world" is still being developed and is to some degree verging on an inherently cultural or anthropological study, because computers and software dont "cause" bugs— humans do! this answer will focus on general Q/A approaches of which formal software verification can be seen as one element.

a remarkable observation is that often software that is "good enough" yet "buggy" can frequently outsell better tested but lower functionality software in the marketplace. in other words, the marketplace does not always put a premium on software quality and the modern techniques of software engineering, which do not always emphasize quality, somewhat reflect that. moreover quality can often add a significant expense to the final product. with those caveats, here are some of the basics:

* **redundant/fault tolerant systems.** this is a wide area of study. fault tolerance & redundancy can be designed into the many layers of a system. eg a router, a server, a disk drive, etcetera.
* **testing**. all the types— unit testing, integration testing, user acceptance testing, regression testing, etc.
* nowadays **automated testing** via test suites that can be run unattended is more developed/important. test suites running are often coupled with the build tool.
* an important concept in testing is **code coverage**. ie what code is **exercised** by the test. a test cannot find a bug in code that is not "touched" by the test.
* another key concept in testing is **test harnessess** that exercise code that is not easily accessed directly.
* tests should exercise all levels of the software. if the software is well modularized, this is not difficult. higher level tests should penetrate deeply into the code. tests that exercise large amounts of code with small test setup increase **"test leverage"**.
* making the code **as least complicated as possible** is important for testing. testing should be a consideration in the architecture design. often there are multiple ways to implement the same feature yet some have much different implications for test coverage/leverage. for every branch in the code, its often another test case. branches within branches escalate to exponential increase in code paths. therefore avoiding highly nested/conditional logic improves ability to test.
* studying **famous (massive) software failures** of which there are many examples & case studies is helpful for understanding the history and developing a mindset oriented towards quality considerations.
* one can get carried away with testing! there is both a problem with **too little or too much** testing. there is a "sweet spot". the software cannot be successfully built in either extreme.
* use all the basic tools in the most effective way. debuggers, code profilers, test code coverage tools, defect tracking system, etc! do not necessarily commit to fixing, but **track** even the smallest defects in the tracking software.
* careful use of SCM, source code management, and **branching** techniques is important in avoiding regressions, isolating and progressing fixes, etc
* **[N-version Programming](http://gse.ufsc.br/~bezerra/disciplinas/Confiabilidade/docs/n-versionprogramming.pdf)**: a practice used often for developing Mission Critical Software. The premise of this practice is that N independently developed programs are unlikely to have the same common bug / fault. This has been criticized in a few [papers](http://sunnyday.mit.edu/critics.pdf) . [NVP](http://en.wikipedia.org/wiki/N-version_programming) is, however, a practice not a theoretical concept.

I believe physicist Feynman has some account of the method that NASA used to guarantee reliability of the space shuttle systems in his book "What do you care what other people think?" — he said they had two teams, say Team A and Team B. team A built the software. team B took an adversarial approach to Team A and tried to break the software.

it helps if Team B has good software engineering background, ie themselves can write code harness/programmatic tests etcetera. in that case Team B had almost equal level of resources as Team A. on the other hand, this approach is expensive because it can nearly double the cost of building the software. more typically, there is a smaller QA team compared to the development team.

> **Comments:**
> **username_6**: Someone should check your OS for correctness with respect to the specification that pressing the Shift key and a letter produces a capital letter.  
> **username_4**: addendum: schedule constraints can impact quality. see also [project mgt triangle](http://en.wikipedia.org/wiki/Project_management_triangle) composed of scope, cost, schedule with quality the "area" affected by all 3. see also ["Why can't the IT industry deliver large, faultless projects quickly as in other industries?"](http://programmers.stackexchange.com/questions/158640/why-cant-the-it-industry-deliver-large-faultless-projects-quickly-as-in-other). did not add the N-Version item myself [its covered other answer] but note Feynman mentioned that NASA used it also in the space shuttle design.  
> **username_4**: also, ["why isnt software as reliable as a car"?](http://programmers.stackexchange.com/questions/41050/why-isnt-software-as-reliable-as-a-car)  
> **username_4**: another interesting case study is the [mars rover](http://programmers.stackexchange.com/questions/159637/what-is-the-mars-curiosity-rovers-software-built-in) which has large amts of code, much of it autogenerated. in that case prior rovers field tested most of the software & it was reused.  

---

### Answer by username_7 on 2012-09-12. Score: 6

An old approach (but it is still used in some applications) is the [N-version programming](http://en.wikipedia.org/wiki/N-version_programming)

From Wikipedia:

**N-version programming** (**NVP**), also known as *multiversion programming*, is a method or process in software engineering where multiple functionally equivalent programs are independently generated from the same initial specifications. The concept of N-version programming was introduced in 1977 by Liming Chen and Algirdas Avizienis with the central conjecture that the "independence of programming efforts will greatly reduce the probability of identical software faults occurring in two or more versions of the program".The aim of NVP is to improve the reliability of software operation by building in fault tolerance or redundancy.  
....

See for example: "[Challenges in Building Fault - Tolerant Flight Control System for a Civil Aircraft](http://www.iaeng.org/IJCS/issues_v35/issue_4/IJCS_35_4_07.pdf)"

> **Comments:**
> **username_8**: It's worth noting that n-version programming *does not work*. The fundamental assumption -- namely, that errors in repeated trials of the software development process are independent -- is *completely false*. This idea makes no sense theoretically (a difficult-to-implement algorithm won't get magically easier for a second independent team), and it's been debunked experimentally, too: John Knight and Nancy Leveson's experiment showing that the independence assumption is not statistically valid is one of the most famous papers in software engineering.  
> **username_7**: @NeelKrishnaswami: I agree! However I think (but I'm not an expert) that *does not work* should be replaced with *it doesn't improve reliability as much as it should if compared with other approaches*. Citing K&L: "*... We never suggested that our result should be used by utself as a basis for a decision about the effectiveness of N-version programming. We merely suggested that caution would be appropriate ...*". I think that the debate on how much the NVP approach can be useful for critical system design is still open (see the recent work of Khoury et al.)  

---

### Answer by username_9 on 2014-04-27. Score: 3

Two or three years ago I started taking a look to formal methods applied to software. This was a quest driven by curiosity, and by the feeling that I had to learn programming tools and methods with longer time-spans. Although I dreamed wishfully about a [Silver Bullet](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.117.315), I really thought that there was not an answer to the question: "How can I write a correct program?".

At this point of the quest after trying some tools (Z, B, VHDL, and Estelle), I'm using [TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html). This is a variant of temporal logic with software tools for model checking and mechanic proofs. I think that I choose this approach because L. Lamport was behind it, the syntax was simple, there were lots of examples, there was a community taking care of it, and the language and tools were fairly well documented.

Regarding my initial question, I think that there is not a complete answer. However, it is worth learning that it pays off to specify formally some portions of a system. It is also pretty useful to reverse engineer some complex ones. That is, It is effective to create a blueprint for the difficult and critical parts. However, I don't think there is an effective method to translate automatically the specification to a programming language or framework (unless you restrict the project to a very specific environment). I also do not think that having a formal specification should prevent you from testing the software.

In a nutshell, I think that the following metaphor (from Lamport) is really powerful: "Do you expect a house to be automatically build from a blueprint? Will you buy a house that is not yet build and it does not have blueprint?".

During this quest, I have found the following resources useful:

* [Software Specification Methods](http://rads.stackoverflow.com/amzn/click/1905209347). This book provides a broad overview of the existing methods and tools. There you can find basic explanations and examples of Z, SDL, TLA+, Petri Nets, Coq, etc.
* If you think that TLA+ fits your needs, I really recommend the book [Specifying Systems](http://research.microsoft.com/en-us/um/people/lamport/tla/book.html). You can get the book for free, and it comes with examples to play with :).
* Recently, I read a couple of related articles that give two different perspectives to the state of the art of the formal methods: [The Case for Formal Methods](http://permalink.gmane.org/gmane.comp.encryption.general/14818m), and [Formally Verified Mathematics](http://cacm.acm.org/magazines/2014/4/173219-formally-verified-mathematics/fulltext).

Good luck!


---

### Answer by username_10 on 2012-09-19. Score: 1

The answers so far covered already most of what should be said about the foundations of how relate specification and code to each other. I just want to add a more practical point that approaches the question in the header of this thread:

How create mission critical software?

There exists tools that automatically analyze your code for errors (violations of the specification, or "typical bugs"). To my knowledge, these methods mostly build on static analysis and are not immediately related to the theories you mentioned (LTL/CTL/...), but they do find errors in real code and it is already feasible, from a practical point of view, to use such tools in industrial projects. I personally have not used many of them, but it seems that these tools start being accepted by practitioners. For further reading, I can recommend the following blog article:

<http://www.altdevblogaday.com/2011/12/24/static-code-analysis/>

> **Comments:**
> **username_4**: example implementation with java, open source apache— [findbugs](http://findbugs.sourceforge.net/)  

---

### Answer by username_13 on 2012-09-18. Score: 0

*Certifying algorithms* can be useful when building mission critical software.

> A certifying algorithm is an algorithm that produces, with each
> output, a certiﬁcate or witness (easy-to-verify proof) that the
> particular output has not been compromised by a bug.

Read more in this survey paper [Certifying algorithms
by McConnell, R.M. and Mehlhorn, K. and Naher, S. and Schweitzer, P.](http://www.cs.colostate.edu/~rmm/cert11.pdf)

> **Comments:**
> **username_2**: In 1998, Pnueli, Siegel and Singerman described this idea applied to compilers, under the name _translation validation._ Compilers are inherently higher-order (the input is a program, the output is a program), so they tend to be hard to verify.  But there are crazy people like X. Leroy who develop verified compilers anyway. (Crazy in the best possible sense!)  

---

### Answer by username_11 on 2012-09-12. Score: -2

> But then how to verify that the software (not only the specification) is indeed correct?

Unit testing? Write a test for every single requirement in the spec, and then test every single method in your implementation to see that its output/input conforms to said spec. This can be automated so that these tests are run continuously to ensure no change ever breaks previously working features.

Theoretically speaking, if your unit tests have 100% code coverage (i.e. every single method in your code is tested) your software should be correct, provided the tests themselves are accurate and realistic.

> **Comments:**
> **username_2**: For any reasonably complex program, code coverage (by testing) cannot ensure correctness.  You would have to cover all possible executions; all lines of code is _not_ enough.  
> **username_12**: Code coverage is too vague a concept. We distinguish between, e.g. method coverage, statement coverage, branch coverage, path coverage and so on. As Radu points out, for non-trivial programs, testing often runs into combinatoral explosions. That said, aeronautics software has a pretty great track record, and its correctness is often based on extensive testing.  
> **username_0**: If you mean testing by tools like JUnit, this kind of standard automatic testing can not cover every cases (unless the program is extremely small). For typical application, this kind of testing is typically enough. But for mission critical application, I don't know whether this is enough (or not).  
> **username_4**: think this answer is being unfairly penalized. suspect formal verification methods that work with infinite and not finite cases are excellent areas of academic study but possibly not used frequently or widely in industry. ie there may be a divergence/gap between what academics & industry practitioners see as "enforcing correctness"  
> **username_2**: @vzn: In my experience, there is remarkable agreement between what is considered to be a bug by academics and, respectively, practitioners.  Also, I bet that most of my (former) colleagues from industry would agree that "every single method in your code is tested" does not sound very reassuring. (And, no, I did not downvote. I almost never do.)  
> **username_4**: @radu, a straw man. did not assert otherwise. merely asserted that the focus, emphasis, or approaches may be different between theoretical study & practice/application in the "real world"[TM]. eagerly awaiting your own constructive answer.  
> **username_2**: @vzn: Did I say you said otherwise? I was simply trying to explain why I believe that others are not upvoting this answer. At this time I cannot answer this question, because I don't understand it.  

---

