15
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ 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. $\endgroup$ – Giorgio Camerani Sep 12 '12 at 9:57
  • $\begingroup$ @GiorgioCamerani : The first one $\endgroup$ – fajrian Sep 12 '12 at 10:44
  • 2
    $\begingroup$ 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. $\endgroup$ – Radu GRIGore Sep 12 '12 at 13:19
  • $\begingroup$ @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. $\endgroup$ – fajrian Sep 12 '12 at 13:52
  • 1
    $\begingroup$ @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.) $\endgroup$ – Radu GRIGore Sep 12 '12 at 16:21
11
$\begingroup$

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 and the specification is often an LTL formula. Or, the program could be a list of PowerPC instructions and the specification could be a set of Hoare-Floyd assertions written in, say, 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:

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

$\endgroup$
8
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ any ref on how airbus uses formal methods would be helpful. (understand that its possibily proprietary info.) $\endgroup$ – vzn Sep 14 '12 at 15:55
  • $\begingroup$ @RossDuncan I found this web page after going to Berry's web page and a few searches. Is this the formal methods Airbus was using that you were referring to? $\endgroup$ – scaaahu Sep 16 '12 at 6:38
  • $\begingroup$ 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 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. $\endgroup$ – Ross Duncan Sep 16 '12 at 16:09
  • 2
    $\begingroup$ Airbus also uses astree.ens.fr $\endgroup$ – Radu GRIGore Sep 16 '12 at 19:35
7
$\begingroup$

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: 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 . NVP 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.

$\endgroup$
  • 8
    $\begingroup$ Someone should check your OS for correctness with respect to the specification that pressing the Shift key and a letter produces a capital letter. $\endgroup$ – Andrej Bauer Sep 17 '12 at 11:32
  • 1
    $\begingroup$ addendum: schedule constraints can impact quality. see also project mgt 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?". 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. $\endgroup$ – vzn Sep 18 '12 at 20:40
  • 1
    $\begingroup$ also, "why isnt software as reliable as a car"? $\endgroup$ – vzn Sep 18 '12 at 21:27
  • 1
    $\begingroup$ another interesting case study is the mars rover which has large amts of code, much of it autogenerated. in that case prior rovers field tested most of the software & it was reused. $\endgroup$ – vzn Sep 19 '12 at 2:26
6
$\begingroup$

An old approach (but it is still used in some applications) is the 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"

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Neel Krishnaswami Apr 28 '14 at 9:25
  • $\begingroup$ @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.) $\endgroup$ – Marzio De Biasi Apr 28 '14 at 10:11
4
$\begingroup$

fajrian, this question you've done cover two of the biggest problems in the research of software engineer: the conformity between the specification and the model and between the model and the code. Model here a representation of what the system will do, or how it will be done, there are lots of levels to model a system.

So, there are some people trying to find the best answer to your question. Because it is very difficult to check the correctness of a software based on a model, for example, using formal methods. I know JML is a way to do it, but i don't know the limits of its usage.

To wrap up, how checking the correctness of code is hard to do, people try to mix formal methods and test, creating testing automatically from specifications for example. One example for real-time systems is the TIOSTS that is a based on input/output timed events.

Testing only is not a formal method approach, doing it improves reliability but not checks correctness.

$\endgroup$
3
$\begingroup$

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, 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+. 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. 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. 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, and Formally Verified Mathematics.

Good luck!

$\endgroup$
1
$\begingroup$

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/

$\endgroup$
  • $\begingroup$ example implementation with java, open source apache— findbugs $\endgroup$ – vzn Sep 19 '12 at 17:47
0
$\begingroup$

Certifying algorithms can be useful when building mission critical software.

A certifying algorithm is an algorithm that produces, with each output, a certificate 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.

$\endgroup$
  • $\begingroup$ 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!) $\endgroup$ – Radu GRIGore Sep 18 '12 at 18:17
-2
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ 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. $\endgroup$ – Radu GRIGore Sep 12 '12 at 13:23
  • 1
    $\begingroup$ 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. $\endgroup$ – Martin Berger Sep 12 '12 at 13:53
  • $\begingroup$ 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). $\endgroup$ – fajrian Sep 12 '12 at 14:00
  • 2
    $\begingroup$ @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.) $\endgroup$ – Radu GRIGore Sep 12 '12 at 16:42
  • 1
    $\begingroup$ @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. $\endgroup$ – Radu GRIGore Sep 12 '12 at 16:58

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.