If you learned formal methods for software, how useful have you found it?

Question

If you have been trained in the use of formal methods (FM) for programming:

• How useful have you found it?
• What did your FM training involve (e.g. a course, a book)?
• What FM tools do you use?
• What advantages in speed/quality has it given you compared to not using FM?
• What kind of software do you create with FM?
• And if you don't directly use FM now, was it at least worth learning??

I'm curious to hear as many experiences/opinions on FM as can be found in this community; I'm starting to read up on it and want to know more.

Background

Programming and software development/engineering are some of the newest human skills/professions on Earth, so not surprisingly, the field is immature — that shows in our field's main output, as code that is typically late and error-prone. Industry immaturity is also shown by the wide margin (at least 10:1) in productivity between average and top coders. Such dismal facts are well covered in the literature, and introduced by books like Steve McConnell's Code Complete.

The use of formal methods (FM) has been proposed by major figures in software/CS (e.g. the late E. Dijkstra) to address (one of) the root causes of errors: the lack of mathematical rigour in programming. Dijkstra, for instance, advocated for students developing a program and its proof together.

FM seems to be much more prevalent in CS curricula in Europe compared to the US. But in the past few years, new "lightweight" FM approaches and tools like Alloy have attracted some attention. Still, FM is far from common usage in industry, and I'm hoping for some feedback here on why.

Update

As of now (10/14/2010), of the 6 answers below, no one has clearly argued for the usage of FM in "real world" work. I'm really curious if someone can and will; or perhaps FM really does illustrate the divide between academia (FM is the future!) and industry (FM is mostly useless).

Answer 1

Absolutely useless for anything nontrivial.

I had a course called, aptly, "Formal Methods" that focused on Alloy- I can't possibly see using that anywhere. Had another class that focused on concurrency modeling with LTSA- equally useless.

The problem is that most bugs and problems in software (at least in my experience) arise from complexity that occurs below the level of abstraction of those tools.

Answer 2

I have a background in CSP (Communicating Sequential Processes). Not to toot my own horn but I wrote my Master's thesis on Timed CSP, particularly "compiling" specifications written in formal methods into executable C++. I can say I have some experience with formal methods. Once I completed my degree and got a job in the industry, I have not been using formal methods at all. Formal methods is still too theoretical to be applied in the industry. Formal methods have found some practical application in the area of embedded systems. For example, NASA uses formal methods in their projects. I would speculate that formal methods are very far from being widely adopted in the industry. It simply does not make sense to write software specifications in formal methods and then "human interpret" them to your framework of choice. Plain English and diagrams work better for that, while unit and integration tests have been doing a pretty good job of "verifying" the correctness of code. I think formal methods will remain in the world of academia for some time.

Answer 3

I've read a few books about formal methods, and applied some. My immediate reaction was, "Gee, these books tell me how to be a good programmer, as long as I'm a perfect mathematician." Another weakness is that you can only prove equivalence with another formal description. Writing up a formal specification for a program is tantamount to writing a program in a higher-level language, and there's no way you can avoid introducing bugs in a reasonably large spec.

I've never made formal methods work on a large scale. They can be useful in getting something small and tricky correct, and in convincing me that they're correct. In that way, I can work with slightly larger building blocks and sometimes get a little more done.

One thing I did pick up that is more generally useful is the concept of an invariant, a statement about a program and its state that is always true. Anything you can reason from is good.

As alluded to above, I'm not a perfect mathematician, and so my proofs sometimes contain errors. However, in my experience these tend to be big dumb mistakes that are easy to catch and fix.

Answer 4

I took a graduate course in formal program analysis, where we focused on operational semantics. I did my final paper on the seL4 effort, reviewing the formal methods they used. My primary take-away in terms of practicality was that it's of marginal value. Not only do you have to write the program, you have to write the proof. Wow. Two sources of bugs. Not just one. Further, there was an enormous amount of restrictions placed on the actual code. It's very hard to formally describe a physical computer, including I/O.

Answer 5

Self-taught myself TLA+ last year, have been using it ever since. It's one of the first tools I reach for whenever I start a project. The mistake most people make is they assume that formal methods is an all-or-nothing thing: either you're not using formal methods or you have complete verification. However, there's something between them: formal specification, where you check that an abstract specification of your project doesn't break your invariants. Unlike verification, specification is practical enough to use in industry.

Specification languages are more expressive than programming languages. For example, here's a (very) simple PlusCal spec for a distributed data store:

process node \in 1..5 \* Nodes
variables online = TRUE,
          stored \in SUBSET data; \* Some set
begin 
  Transfer:
    either
      with node \in Nodes, datum \in stored do
        node.stored := node.stored \union {datum};
      end
    or \* crash
      online := FALSE;
    end either;
end process;

This snippet specifies five nodes running simultaneously, running transfers in an arbitrary order, where every transfer is an arbitrary piece of data to an arbitrary node. Additionally, we've specified that any given transfer may fail and cause the node to crash. And we can simulate all of these behaviors in the TLA+ model checker! That way we can test that regardless of order, failure rates, etc, our requirements still hold. Speaking of which, let's add a couple of requirements. First, that we never transfer data to an offline node:

[][\A node \in Nodes: ~online => UNCHANGED node.stored]_vars

In our simplified version, the model checker will find a failure state. We can also specify "any given piece of data is in at least one online node":

\A d \in data: \E n \in Nodes: n.online /\ d \in n.stored

Which will also fail. Good luck checking these with a unit test!

The main limitation of specification is it exists independently of your actual code. It can only tell you that your design is correct, not that you implemented it right. But it's faster to specify than verify and it catches bugs that are too subtle for testing, so I find it worth the effort. Pretty much any code involving concurrency or multiple systems is a good place for a formal spec.

Answer 6

State diagrams and Petri nets are useful for modelling and analyzing protocols and realtime systems. First they help design a solution. Second they help find test cases for exciting software in very specific situations.

Answer 7

I used to work in a department at ICL, before they were bought up by Fujitsu. They had some large government-type contracts that required proof that the software worked as advertised, so they built a machine that would take the formal specification written in Z and validate the code as it ran, with a big green or red light for pass/fail.

It was an amazing thing, but, as the esteemed @FishToaster points out, it was useless for anything non-trivial.