16

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

  • Regarding your update, maybe no one has argued for the usage of FM in "real world" work because there are very few use cases for them in real world work – Richard Nov 3 '11 at 12:42
8

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.

  • Thanks for sharing; Would you say the training in FM was at least helpful to your later work, e.g. helped you think more clearly? Or not? – limist Oct 7 '10 at 23:34
  • @limist: I really don't think so. I mean, I kinda liked Alloy, but I don't think it was useful even just to expanding how I think. – Fishtoaster Oct 8 '10 at 4:08
  • 2
    This is exactly the answer I would have given. The most totally redundant class I took at university and not something I have ever looked back on and been glad I learned it. I think the root of the problem is that the Formal Specification must be more complex than the code in order to model it correctly, so for any remotely complex code it's a massively arduous task creating a formal model of it, to the point that I can't imagine anyone outside hardware design or similarly irrevocable work wanting or being able to do it. – glenatron Oct 14 '10 at 21:39
  • 1
    That's disappointing. I was imagining it might be useful for testing that you had a reasonably complete model; while the actual bugs would most often be below the model (screwing up the mutexes or whatever), I assumed it would be useful to use Alloy to find flaws in the model itself. (Intuitively it seems less likely to be useful to try to use a proof assistant; I'd expect counterexamples to be more useful, and that seems more in the domain of things like Alloy (though ideally I guess it would be good to be able to approach both in the same system).) – Bruce Stephens Dec 20 '12 at 16:04
7

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.

  • Thanks for sharing, I'll ask a follow-up repeated often on this Q: Would you say the training in FM was at least helpful to your later work, e.g. helped you think more clearly? Or not? – limist Oct 7 '10 at 23:35
  • Congrats on your masters! – Chris Oct 8 '10 at 0:13
  • @limist: I would say it was a very good theoretical experience, but I found very little practical application in the industry. – ysolik Oct 8 '10 at 3:24
4

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.

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.

  • I once saw a stab at describing tape-style I/O. The author had no solutions for formally describing random access files, and contented himself with badmouthing them. – David Thornley Oct 8 '10 at 17:43
  • 1
    @David: Those random-access files. Bad news. You don't want to use them. =) – Paul Nathan Oct 8 '10 at 20:19
3

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.

3

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.

1

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.

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.