The embedded long-term support initiative [LWN.net]

The embedded long-term support initiative

Posted Nov 1, 2011 11:57 UTC (Tue) by dps (guest, #5725)
In reply to: The embedded long-term support initiative by zlynx
Parent article: The embedded long-term support initiative

Formal methods are much more reliable than most programming languages. Just writing an unambiguous specifications helps. Formal methods also allow non-negotiable proof that a proposed solution meets the specification.

You can also prove things like *any* network of the stated components with an infinitely readable external input is deadlock free. I am not aware of any programming language that can do that.

In generally the experience is that using formal methods makes the initial phases longer and the final phases shorter, partly because a lot of problems and discovered sooner. Moves like only proving critical safety properties or analysing a high level design are popular.

As with any tool formal methods can be misused. I not only know formal methods but believe I have the taste to know when *not* to apply them.

to post comments

Secure Software and Formal Methods

Posted Nov 2, 2011 11:18 UTC (Wed) by abacus (guest, #49001) [Link] (1 responses)

As far as I know formal methods are fine for functional specifications. I'm still waiting for a formal specification of a secure operating system though. See e.g. Gerwin Klein e.a., seL4: formal verification of an operating-system kernel, Communications of the ACM, Volume 53 Issue 6, June 2010.

Secure Software and Formal Methods

Posted Nov 2, 2011 17:33 UTC (Wed) by zlynx (guest, #2285) [Link]

My complaint about formal methods is that they aren't any kind of cure-all. They rely on the specifications being complete and that the specifications are correctly translated into the formal verification method.

In almost all programming, the specifications are incomplete or incorrect. Programmers, even without realizing what they are doing, fill in the gaps in incomplete specifications and may not even realize the specification was missing information.

Many bugs are caused by programmers on each side of an interface assuming different things about the specification. An example of this is the POSIX select() timeout parameter.

To fully specify the behavior of a system under all conditions is in my opinion, as prone to oversights and misunderstanding (aka bugs) as writing the program itself in assembly or C. (Well, you can make a lot more typo type mistakes writing in C, but I think it holds for logic errors.)

Reading through some of that seL4 paper you linked, I see they had to make about 300 changes in the spec during the process. In other words, they had to debug it. I wonder how they know if they found all the problems in their spec?