<p>Regarding 4: There's plenty of work combining formal methods and testing. Googling "formal methods testing" reveals quite a large amount of work. Although there are many different goals of such work, one of the key goals is to generate more effective test suites. This <a href="http://www.csl.sri.com/users/rushby/slides/efftestgen.pdf">talk</a> gives a nice introduction, based on model checking.</p>

<p>Also regarding the issue <em>software security</em>, which has been edited out of the question: formal methods need to work harder to deliver in that realm. Typically one writes a specification for a piece of software and verifies that the specification is satisfied, namely, that when the input satisfies the precondition that the output satisfies the postcondition. To ensure secure software one also needs to check also that the software behaves sensibly for input that does not satisfy the precondition. (This is of course equivalent to setting the precondition to true for all input.) The space of all inputs is typically much larger than just well-formed input, but typically this is one place where even functionally correct software can be violated, simply by violating its assumptions.</p>

<p>Regarding point 3: Some work has been done for verifying systems in settings where faults are explicitly modelled, including <a href="http://www.cs.princeton.edu/~dpw/papers/faultylogic_esop2010.pdf">Faulty Logic:  Reasoning About Fault-tolerant Programs.</a> Matthew Meola and David Walker. European Symposium on Programming, 2010. Work on probabilistic model checking and probabilistic verification certainly both also address the issue of faults to some degree.</p>

CC BY-SA 2.5
2011-01-05T21:37:03.213Z
2011-01-06T10:39:25.800Z
2011-01-06T10:39:25.800Z
Dave Clarke
<p>Your points in order: </p>

<ul>
<li>The correctness of all specifications are ultimately subjective: they are perceived to solve a problem correctly according to their users or they don't.  There is no getting away from this is software development, and no method has the silver bullet for this one.</li>
<li>A lot of work goes into proving that the process is correct with respect to its assumptions.  Usually there is information available for experts to validate these rules.  Any human activity is subject to error but very formalized systems using well-studied approaches are <em>much less</em> subject to error than almost all other human processes.</li>
<li>At some point, any system has a failure mode outside the scope of that system.  You are still better off eliminating all the <em>predictable</em> sources of error, even if you leave some unpredictable ones unaccounted for.</li>
<li>Testing and proving can easily coexist.  Testing is a less specific, more <em>ad hoc</em> process, so you may find less formal work done on it.  But you may be interested in a tool such as <a href="http://en.wikipedia.org/wiki/QuickCheck">QuickCheck</a> that supplements with tests the proofs offered by the Haskell type system.</li>
</ul>

CC BY-SA 2.5
2011-01-05T22:44:02.623Z
2011-01-05T22:44:02.623Z
Marc Hamann
<p>Formal methods have already been shown to work big-time. Without them, we would not have managed to cope with the complexity of designing modern digital systems (microprocessors).  </p>

<p>No micro ships without having its logic subject to functional equivalence verification; without its FPU having been subject to FV; without its cache coherence protocols having been subject to FV (this has been the case since 1995).  </p>

<p>Barring obvious differences between software and engineered physical systems (e.g. bridges, where one can add safety factors), they play the role of engineering math in CS. 
However, FM's use always depends on benefit/cost. Fuzz testing pays off big-time at companies such as Microsoft (Google SAGE in one slide).  </p>

<p>Even within a micro, there are subsystems (e.g. microprocessor pipelines), where FV hasn't had the same impact as elsewhere (e.g. FPU, where conventional testing was not done at all in many cases when formal symbolic trajectory evaluation proved the absence of bugs: Kaivola <em>et al</em> CAV'09).  </p>

<p>Formal methods are also being used in the synthesis of artifacts (code, high-quality tests, schedules for optimally draining battery banks, ...). Of course, all of the issues raised in the question are quite valid, and like in any other use of technology, false ads must be recognized and avoided.</p>

CC BY-SA 3.0
2011-11-05T21:38:17.140Z
2011-12-05T09:59:49.923Z
2011-12-05T09:59:49.923Z
Ganesh
<p>Regarding 2: if the system is formalized in a proof assistant (e.g, Twelf or Agda or Coq) and the properties of soundness and completeness are verified, and the proofs are done in this encoding, this is a non-issue. You may have formalized a system that isn't describing <em>what</em> you intended, but at the least you won't have incorrect proofs or a broken system in which you are reasoning.</p>

CC BY-SA 2.5
2011-01-05T22:55:21.453Z
Also, there is something known as "adequacy" of your encoding: that what you've formalized in a proof assistant is in fact the system you've written down on paper (see http://twelf.plparty.org/wiki/Adequacy). This is not, however, addressing your first point, it is constructing a bijection.
Jamie Morgenstern
CC BY-SA 2.5
2011-01-05T21:05:39.310Z
2011-01-05T21:05:39.310Z
Jamie Morgenstern
<blockquote>
  <p>However, it seems that even if you can give a correctness proof, you may NOT be able to guarantee that the system will not fail.</p>
</blockquote>

<p><a href="http://lesswrong.com/lw/mp/0_and_1_are_not_probabilities/">Yes, perhaps there are no guarantees</a>. Formal methods are meant to find and eliminate errors and to convince humans.</p>

<blockquote>
  <p>What techniques are known to test whether a specification makes any sense at all?</p>
</blockquote>

<p>You might be interested in <a href="http://portal.acm.org/citation.cfm?id=1273931">model checking tools for specifications of formal systems</a>.</p>

<blockquote>
  <p>The proof process may be flawed too! Who knows that those inference rules are correct and legitimate?</p>
</blockquote>

<p>I think (because of Goedel's incompleteness theorem) showing a system of inference rules is consistent necessarily appeals to an even more powerful set of inference rules.</p>

<blockquote>
  <p>Furthermore, proofs can be very large, and how do we know that they do not contain errors?</p>
</blockquote>

<p>Hopefully, huge proofs are checked by a small proof checker that can be read and understood by humans in a reasonable amount of time. This is sometimes called the "de Bruijn criterion". If you believe that the proof checker will not certify an incorrect proof, you need only check the checker.</p>

<blockquote>
  <p>Are there any techniques known to account for the fallibility of real hardware?</p>
</blockquote>

<p>How about <a href="http://portal.acm.org/citation.cfm?id=1250741">Fault tolerant typed assembly language</a>?</p>

<blockquote>
  <p>However, I mostly see research which is either focused on formal methods or testing. What is known about combining the two?</p>
</blockquote>

<p><a href="http://www.tap2011.informatik.uni-bremen.de/">"The TAP conference is devoted to the convergence of proofs and tests"</a>.</p>

<p>Just googling for "proofs and tests" has several good hits above the fold.</p>

CC BY-SA 2.5
2011-01-06T09:28:21.260Z
2011-01-06T09:28:21.260Z
jbapple
<blockquote>
  <p>What techniques are known to test
  whether a specification makes any
  sense at all?</p>
</blockquote>

<p>It is definitely a judgement call. In software engineering, people have designed very strict methodology to find/write/confirm the specifications. This is done by real humans and using a non formal (in the sense non mathematical process), so it is still subject to inconsistency, but at the end of the day, it corresponds to what people want to verify, no more no less. </p>

<blockquote>
  <p>Are there any techniques known to
  account for the fallibility of real
  hardware?</p>
</blockquote>

<p>Sure, there is a field of verification known as <a href="http://en.wikipedia.org/wiki/Runtime_verification">runtime verification</a>, you can also use execution based model checking on the real system running on a totally virtual environment subject to specific scenario (I contributed myself to this with <a href="http://portal.acm.org/citation.cfm?id=1531774">V-DS</a> + <a href="http://www.computer.org/portal/web/csdl/doi/10.1109/QEST.2006.5">APMC</a>). However, this is clearly a major problem to add the interaction between the system and the environment into the verification process.</p>

<blockquote>
  <p>However, I mostly see research which
  is either focused on formal methods or
  testing. What is known about combining
  the two?</p>
</blockquote>

<p>Wow, today I will be totally shameless and cite myself again. With coauthors we work on combining model checking and testing, you can look at <a href="http://www.lri.fr/~oudinet/en/research.html#publications">the publication list of a former PhD student of our group</a> or search for "approximate probabilistic model checking" or "statistical model checking" in any good search engine (work done by Younes et al., Sen et al. or myself et al. and many others). </p>

CC BY-SA 2.5
2011-01-06T15:55:31.980Z
ad 1: Note that the need for a formal formulation of specifications is supposed to aid the subjective part as opposed to formulations in natural language. By having to be very precise, inconsistencies and uncertainties are visible and have to be resolved.
Raphael
CC BY-SA 2.5
2011-01-06T16:47:06.987Z
The process is non formal, but the result is, for model checking, typically a temporal formula (LTL or CTL for example). In my experience (with people from industry), using a formal language does not necessarily improve the consistency of the result :(
Sylvain Peyronnet
CC BY-SA 2.5
2011-01-07T00:51:31.560Z
But you can check for inconsistencies at least, can't you? What have your experiences been regarding "getting what you want"?
Raphael
CC BY-SA 2.5
2011-01-07T11:39:47.590Z
Yes, I can check for the inconsistencies, but unfortunately that does not always help to solve them. The problem is that it is very difficult for most engineers/industrial designers to write specifications in classical verification languages. My opinion is that, if you don't have a deep knowledge of a specification language, using it will guide you too much: you end up writing only what you are able to write with a little familiarity of the language. In summary, it kills your creativity.
Sylvain Peyronnet
CC BY-SA 2.5
2011-01-06T08:16:00.237Z
2011-01-06T08:16:00.237Z
Sylvain Peyronnet
<p>You might be very interested in the works of <a href="http://www.csl.sri.com/users/rushby/">John Rushby</a>, one of the designers of the PVS theorem prover, who is generically interested in exactly the points you mention. You might enjoy reading this classic <a href="http://www.csl.sri.com/users/rushby/abstracts/csl-93-7">report to the FAA about the use of Formal Methods and the Certification of Critical Systems (1993)</a>, and his <a href="http://www.csl.sri.com/users/rushby/biblio.html">newer writings</a> about assembling a probabilistic, formal safety case out of various means of evidence provided (testing, proofs, analyses, etc).</p>

CC BY-SA 3.0
2011-12-05T10:50:53.290Z
2011-12-05T10:50:53.290Z
Martin Schwarz
<p>An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be able to guarantee that the system will not fail. For example:</p>

<ul>
<li>The specification may not model the system correctly, or a production system may be too complicated to model, or the system may be flawed inherently due to contradictory requirements. What techniques are known to test whether a specification makes any sense at all?</li>
<li>The proof process may be flawed too! Who knows that those inference rules are correct and legitimate? Furthermore, proofs can be very large, and how do we know that they do not contain errors? This is the heart of the critique in de Millo, Lipton, and Perlis's "Social Processes and Proofs of Theorems and Programs".  How do modern formal methods researchers respond to this critique?</li>
<li>At runtime, there are many nondeterministic events and factors that can seriously affect the system. For example, cosmic rays can alter RAM in unpredictable ways, and more generally we have no guarantees that hardware will not suffer Byzantine faults, which Lamport has proved are very difficult to be robust against. So the correctness of the static system does not guarantee the  system won't fail! Are there any techniques known to account for the fallibility of real hardware?</li>
<li>At present, testing is the most important tool we have for establishing that software works. It seems like it should be a complementary tool with formal methods. However, I mostly see research which is either focused on formal methods or testing. What is known about combining the two?</li>
</ul>

CC BY-SA 2.5
2011-01-05T20:10:18.970Z
Issues 1 and 3 seem to be inherent to system analysis, whatever the method. Formal methods at least make them obvious, unlike other methods. Issue 2 is non-existent as far as I know; the formal systems I have seen used have been proven to be correct; you _can_ mess up every deduction system by modifying it yourself and making mistakes, of course.
Raphael
CC BY-SA 2.5
2011-01-05T20:42:13.903Z
This question is phrased rather subjectively, and in a way as to provoke. I'd recommend rephrasing or closing.
Suresh Venkat
CC BY-SA 2.5
2011-01-05T21:29:29.333Z
I made some major revisions to make the question more useful in my judgment. If you think this was too aggressive an alteration, please post in meta.
Neel Krishnaswami
CC BY-SA 2.5
2011-01-05T21:35:17.490Z
Thanks to Suresh for pointing it out. I didn't realize that, was eager to know what arguments there are to make me think it right.
Jenny
CC BY-SA 2.5
2011-01-05T21:41:05.880Z
Thanks, Neel Krishnaswami! I should learn from how to write properly, and your revision is urging me to think more...looking forward to more thought-provoking comments on those questions.
Jenny
CC BY-SA 2.5
2011-01-05T21:41:06.363Z
@Neel: Nice edit. One thing your change omits is a reference to system security, which was part of the essence of the original question. Perhaps Jenny can put that back in, to again make it her question.
Dave Clarke
CC BY-SA 2.5
2011-01-05T22:21:59.713Z
Nice edit: I reverted my downvote.
Suresh Venkat
CC BY-SA 2.5
2011-01-05T22:55:03.857Z
As for new bullet 4: Big misconception: (realistic) testing can never show the absence of errors.
Raphael
CC BY-SA 2.5
2011-01-05T23:02:32.480Z
I think the areas don't mingle as much as one would like because of the very different schools of thinking. Engineery minds will test or claim quality by construction process, learning while they go in practice. Sciency minds will want formal proofs -- and realize the restrictions, retreat to the ivory tower and extend their toolset first. Both ways are not very compatible.
Raphael
CC BY-SA 2.5
2011-01-05T23:14:14.247Z
@Raphael: I waffled about that, but decided to go with the stronger claim, since people do use testing to build belief htat a program works. Sometimes this is even ok! As a simple example, if your programming language is the language of polynomials, you can test whether an expression correctly implements a function of degree $n$ by testing $n$ points. So a question is whether actual programs have any qualities that justify similar (albeit maybe probabilistic/Bayesian) conclusions, and what such properties might be....
Neel Krishnaswami
CC BY-SA 2.5
2011-01-06T01:12:42.583Z
@Raphael: I think that is an oversimplification about [formal verification](http://en.wikipedia.org/wiki/Formal_verification), model checking people (e.g. [Edmund M. Clarke](http://www.cs.cmu.edu/~emc/) and [Moshe Y. Vardi](http://www.cs.rice.edu/~vardi/)) are also very rigorous, while people from proof theoretic side (e.g. [Thierry Coquand](http://www.cse.chalmers.se/~coquand/) and [Gerard Huet](http://sanskrit.inria.fr/huet/)) are also seriously interested in practical issues.
Kaveh
CC BY-SA 2.5
2011-01-06T15:53:17.223Z
@Neel: You are right, some programs can be proven to be correct by testing a few inputs. In general, however, this is not true but that fact is often ignored, therefore my statement. @Kaveh: It is a simplification, for sure, since people mix methodologies. I have the feeling, though, that most people are either engineers or scientists at heart, rarely both. You can see this when engineers do proofs or scientists build something. That impression might be wrong, of course.
Raphael
<lo.logic><pl.programming-languages><formal-systems><formal-methods>
How can we know that formal methods work?
Jenny
# How can we know that formal methods work?

(Asked by: username_0 on 2011-01-05)

An important goal of formal methods is to prove the correctness of systems, either by automated or human-directed means. However, it seems that even if you can give a correctness proof, you may NOT be able to guarantee that the system will not fail. For example:

* The specification may not model the system correctly, or a production system may be too complicated to model, or the system may be flawed inherently due to contradictory requirements. What techniques are known to test whether a specification makes any sense at all?
* The proof process may be flawed too! Who knows that those inference rules are correct and legitimate? Furthermore, proofs can be very large, and how do we know that they do not contain errors? This is the heart of the critique in de Millo, Lipton, and Perlis's "Social Processes and Proofs of Theorems and Programs". How do modern formal methods researchers respond to this critique?
* At runtime, there are many nondeterministic events and factors that can seriously affect the system. For example, cosmic rays can alter RAM in unpredictable ways, and more generally we have no guarantees that hardware will not suffer Byzantine faults, which Lamport has proved are very difficult to be robust against. So the correctness of the static system does not guarantee the system won't fail! Are there any techniques known to account for the fallibility of real hardware?
* At present, testing is the most important tool we have for establishing that software works. It seems like it should be a complementary tool with formal methods. However, I mostly see research which is either focused on formal methods or testing. What is known about combining the two?

**Tags:** lo.logic, pl.programming-languages, formal-systems, formal-methods

> **Comments:**
> **username_1**: Issues 1 and 3 seem to be inherent to system analysis, whatever the method. Formal methods at least make them obvious, unlike other methods. Issue 2 is non-existent as far as I know; the formal systems I have seen used have been proven to be correct; you _can_ mess up every deduction system by modifying it yourself and making mistakes, of course.  
> **username_2**: This question is phrased rather subjectively, and in a way as to provoke. I'd recommend rephrasing or closing.  
> **username_3**: I made some major revisions to make the question more useful in my judgment. If you think this was too aggressive an alteration, please post in meta.  
> **username_0**: Thanks to Suresh for pointing it out. I didn't realize that, was eager to know what arguments there are to make me think it right.  
> **username_0**: Thanks, username_3! I should learn from how to write properly, and your revision is urging me to think more...looking forward to more thought-provoking comments on those questions.  
> **username_4**: @Neel: Nice edit. One thing your change omits is a reference to system security, which was part of the essence of the original question. Perhaps username_0 can put that back in, to again make it her question.  
> **username_2**: Nice edit: I reverted my downvote.  
> **username_1**: As for new bullet 4: Big misconception: (realistic) testing can never show the absence of errors.  
> **username_1**: I think the areas don't mingle as much as one would like because of the very different schools of thinking. Engineery minds will test or claim quality by construction process, learning while they go in practice. Sciency minds will want formal proofs -- and realize the restrictions, retreat to the ivory tower and extend their toolset first. Both ways are not very compatible.  
> **username_3**: @username_1: I waffled about that, but decided to go with the stronger claim, since people do use testing to build belief htat a program works. Sometimes this is even ok! As a simple example, if your programming language is the language of polynomials, you can test whether an expression correctly implements a function of degree $n$ by testing $n$ points. So a question is whether actual programs have any qualities that justify similar (albeit maybe probabilistic/Bayesian) conclusions, and what such properties might be....  
> **username_5**: @username_1: I think that is an oversimplification about [formal verification](http://en.wikipedia.org/wiki/Formal_verification), model checking people (e.g. [Edmund M. Clarke](http://www.cs.cmu.edu/~emc/) and [Moshe Y. Vardi](http://www.cs.rice.edu/~vardi/)) are also very rigorous, while people from proof theoretic side (e.g. [Thierry Coquand](http://www.cse.chalmers.se/~coquand/) and [Gerard Huet](http://sanskrit.inria.fr/huet/)) are also seriously interested in practical issues.  
> **username_1**: @Neel: You are right, some programs can be proven to be correct by testing a few inputs. In general, however, this is not true but that fact is often ignored, therefore my statement. @username_5: It is a simplification, for sure, since people mix methodologies. I have the feeling, though, that most people are either engineers or scientists at heart, rarely both. You can see this when engineers do proofs or scientists build something. That impression might be wrong, of course.  

---

## 7 answers

### Answer by username_4 on 2011-01-05. Score: 11

Regarding 4: There's plenty of work combining formal methods and testing. Googling "formal methods testing" reveals quite a large amount of work. Although there are many different goals of such work, one of the key goals is to generate more effective test suites. This [talk](http://www.csl.sri.com/users/rushby/slides/efftestgen.pdf) gives a nice introduction, based on model checking.

Also regarding the issue *software security*, which has been edited out of the question: formal methods need to work harder to deliver in that realm. Typically one writes a specification for a piece of software and verifies that the specification is satisfied, namely, that when the input satisfies the precondition that the output satisfies the postcondition. To ensure secure software one also needs to check also that the software behaves sensibly for input that does not satisfy the precondition. (This is of course equivalent to setting the precondition to true for all input.) The space of all inputs is typically much larger than just well-formed input, but typically this is one place where even functionally correct software can be violated, simply by violating its assumptions.

Regarding point 3: Some work has been done for verifying systems in settings where faults are explicitly modelled, including [Faulty Logic: Reasoning About Fault-tolerant Programs.](http://www.cs.princeton.edu/~dpw/papers/faultylogic_esop2010.pdf) Matthew Meola and David Walker. European Symposium on Programming, 2010. Work on probabilistic model checking and probabilistic verification certainly both also address the issue of faults to some degree.


---

### Answer by username_6 on 2011-01-05. Score: 9

Your points in order:

* The correctness of all specifications are ultimately subjective: they are perceived to solve a problem correctly according to their users or they don't. There is no getting away from this is software development, and no method has the silver bullet for this one.
* A lot of work goes into proving that the process is correct with respect to its assumptions. Usually there is information available for experts to validate these rules. Any human activity is subject to error but very formalized systems using well-studied approaches are *much less* subject to error than almost all other human processes.
* At some point, any system has a failure mode outside the scope of that system. You are still better off eliminating all the *predictable* sources of error, even if you leave some unpredictable ones unaccounted for.
* Testing and proving can easily coexist. Testing is a less specific, more *ad hoc* process, so you may find less formal work done on it. But you may be interested in a tool such as [QuickCheck](http://en.wikipedia.org/wiki/QuickCheck) that supplements with tests the proofs offered by the Haskell type system.


---

### Answer by username_7 on 2011-11-05. Score: 9

Formal methods have already been shown to work big-time. Without them, we would not have managed to cope with the complexity of designing modern digital systems (microprocessors).

No micro ships without having its logic subject to functional equivalence verification; without its FPU having been subject to FV; without its cache coherence protocols having been subject to FV (this has been the case since 1995).

Barring obvious differences between software and engineered physical systems (e.g. bridges, where one can add safety factors), they play the role of engineering math in CS.
However, FM's use always depends on benefit/cost. Fuzz testing pays off big-time at companies such as Microsoft (Google SAGE in one slide).

Even within a micro, there are subsystems (e.g. microprocessor pipelines), where FV hasn't had the same impact as elsewhere (e.g. FPU, where conventional testing was not done at all in many cases when formal symbolic trajectory evaluation proved the absence of bugs: Kaivola *et al* CAV'09).

Formal methods are also being used in the synthesis of artifacts (code, high-quality tests, schedules for optimally draining battery banks, ...). Of course, all of the issues raised in the question are quite valid, and like in any other use of technology, false ads must be recognized and avoided.


---

### Answer by username_8 on 2011-01-05. Score: 8

Regarding 2: if the system is formalized in a proof assistant (e.g, Twelf or Agda or Coq) and the properties of soundness and completeness are verified, and the proofs are done in this encoding, this is a non-issue. You may have formalized a system that isn't describing *what* you intended, but at the least you won't have incorrect proofs or a broken system in which you are reasoning.

> **Comments:**
> **username_8**: Also, there is something known as "adequacy" of your encoding: that what you've formalized in a proof assistant is in fact the system you've written down on paper (see http://twelf.plparty.org/wiki/Adequacy). This is not, however, addressing your first point, it is constructing a bijection.  

---

### Answer by username_9 on 2011-01-06. Score: 6

> However, it seems that even if you can give a correctness proof, you may NOT be able to guarantee that the system will not fail.

[Yes, perhaps there are no guarantees](http://lesswrong.com/lw/mp/0_and_1_are_not_probabilities/). Formal methods are meant to find and eliminate errors and to convince humans.

> What techniques are known to test whether a specification makes any sense at all?

You might be interested in [model checking tools for specifications of formal systems](http://portal.acm.org/citation.cfm?id=1273931).

> The proof process may be flawed too! Who knows that those inference rules are correct and legitimate?

I think (because of Goedel's incompleteness theorem) showing a system of inference rules is consistent necessarily appeals to an even more powerful set of inference rules.

> Furthermore, proofs can be very large, and how do we know that they do not contain errors?

Hopefully, huge proofs are checked by a small proof checker that can be read and understood by humans in a reasonable amount of time. This is sometimes called the "de Bruijn criterion". If you believe that the proof checker will not certify an incorrect proof, you need only check the checker.

> Are there any techniques known to account for the fallibility of real hardware?

How about [Fault tolerant typed assembly language](http://portal.acm.org/citation.cfm?id=1250741)?

> However, I mostly see research which is either focused on formal methods or testing. What is known about combining the two?

["The TAP conference is devoted to the convergence of proofs and tests"](http://www.tap2011.informatik.uni-bremen.de/).

Just googling for "proofs and tests" has several good hits above the fold.


---

### Answer by username_10 on 2011-01-06. Score: 5

> What techniques are known to test
> whether a specification makes any
> sense at all?

It is definitely a judgement call. In software engineering, people have designed very strict methodology to find/write/confirm the specifications. This is done by real humans and using a non formal (in the sense non mathematical process), so it is still subject to inconsistency, but at the end of the day, it corresponds to what people want to verify, no more no less.

> Are there any techniques known to
> account for the fallibility of real
> hardware?

Sure, there is a field of verification known as [runtime verification](http://en.wikipedia.org/wiki/Runtime_verification), you can also use execution based model checking on the real system running on a totally virtual environment subject to specific scenario (I contributed myself to this with [V-DS](http://portal.acm.org/citation.cfm?id=1531774) + [APMC](http://www.computer.org/portal/web/csdl/doi/10.1109/QEST.2006.5)). However, this is clearly a major problem to add the interaction between the system and the environment into the verification process.

> However, I mostly see research which
> is either focused on formal methods or
> testing. What is known about combining
> the two?

Wow, today I will be totally shameless and cite myself again. With coauthors we work on combining model checking and testing, you can look at [the publication list of a former PhD student of our group](http://www.lri.fr/~oudinet/en/research.html#publications) or search for "approximate probabilistic model checking" or "statistical model checking" in any good search engine (work done by Younes et al., Sen et al. or myself et al. and many others).

> **Comments:**
> **username_1**: ad 1: Note that the need for a formal formulation of specifications is supposed to aid the subjective part as opposed to formulations in natural language. By having to be very precise, inconsistencies and uncertainties are visible and have to be resolved.  
> **username_10**: The process is non formal, but the result is, for model checking, typically a temporal formula (LTL or CTL for example). In my experience (with people from industry), using a formal language does not necessarily improve the consistency of the result :(  
> **username_1**: But you can check for inconsistencies at least, can't you? What have your experiences been regarding "getting what you want"?  
> **username_10**: Yes, I can check for the inconsistencies, but unfortunately that does not always help to solve them. The problem is that it is very difficult for most engineers/industrial designers to write specifications in classical verification languages. My opinion is that, if you don't have a deep knowledge of a specification language, using it will guide you too much: you end up writing only what you are able to write with a little familiarity of the language. In summary, it kills your creativity.  

---

### Answer by username_11 on 2011-12-05. Score: 5

You might be very interested in the works of [John Rushby](http://www.csl.sri.com/users/rushby/), one of the designers of the PVS theorem prover, who is generically interested in exactly the points you mention. You might enjoy reading this classic [report to the FAA about the use of Formal Methods and the Certification of Critical Systems (1993)](http://www.csl.sri.com/users/rushby/abstracts/csl-93-7), and his [newer writings](http://www.csl.sri.com/users/rushby/biblio.html) about assembling a probabilistic, formal safety case out of various means of evidence provided (testing, proofs, analyses, etc).


---

