How to Create Mission Critical Software?

Question

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.

Answer 1

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:

• Necula, Lee, Proof-Carrying Code, 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 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.

Answer 2

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!

Answer 3

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.

Answer 4

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"

Answer 5

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.

Answer 6

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!

Answer 7

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/

Answer 8

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.

Answer 9

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.