On 31/08/2015 9:46 pm, Gernot Heiser wrote:
On 31 Aug 2015, at 19:33 , Jeroen Slim van Gelderen <askslim@gmail.com> wrote:
Thanks for the pointer to this article, I hadn’t seen it.
It has a lot of informed content, but also some some confusion, so take it with a grain of salt.
Among the things I noticed:
[snip]
- I have no idea where this factor 25 comes from: "The numbers produced by NICTA indicate that it costs around 25 times as much to develop a system this way as to develop one with no verification, testing, or QA.”
I can understand why somebody might draw that conclusion.
The raw numbers for the total effort to develop and verify seL4 that were often quoted back in 2012 (when the article was written) were around the 25 person-year mark. The TOCS paper from 2014 should however be used these days as the authoritative figure on
that question: ssrg.nicta.com.au/publications/nictaabstracts/7371.pdf
I remember Tanenbaum writing somewhere ages ago that one can expect about a person-year to design and write a kernel ala MINIX (although presumably that figure would include some testing...). Indeed, for rubbish, one might expect to do it in a lot less than
1py. (This highlights the meaninglessness of comparing effort for verified software to that for rubbish, of course. Not to mention that seL4 and MINIX are very different.)
That said, the state of the art in systems software verification has moved on a little since 2009. Our own work at NICTA in the context of file systems is already showing how to dramatically reduce the work required for proving functional correctness (albeit
for software with less internal coupling than a microkernel) by co-designing the programming language and verification infrastructure, taking advantage of cool language type systems coupled with corresponding automated reasoning in the theorem prover. But
that's a story for another day.
Toby
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.