Abstract: This paper reflects on the need for formality, discipline and humility in programming. Starting with the work of Turing, Dijkstra and Humphrey, this paper goes on to cover our experience with the Personal Software Process, formal programming with SPARK, and the impact of putting the two together.
The full reference is:
R. Chapman, “The Fumble Programmer” Invited Keynote Paper. Proc of the 26th Safety Critical Systems Symposium, York, UK, Feb 2018. pp. 143-154. Safety Critical Systems Club, UK. ISBN 978-1-9797-3361-8.
For some time, I’ve been working with Altran UK on how we can use, improve and deploy Agile approaches in the development of high-integrity software. We’ve presented our ideas at SCSC events and at the SSS conference with encouraging feedback, so we wrote it up as a Viewpoint article for CACM, which appeared here today.
I’d like personally thank Moshe Vardi for the encouragement to give this a go in the first place, and diligent reviewing of the manuscript from Bertrand Meyer.
Last April, there was a discussion meeting at the Royal Society on “Verified trustworthy software systems.” The attendance and speakers were something of a who’s-who of the software verification community. The resulting issue of Royal Society Transactions A is now in print and on-line.
Our paper, co-authored with Neil White and Stuart Matthews from Altran UK, covers our experiences with building and applying formal verification to real-world industrial systems, and considers the incentives and barriers that seem to be holding back wider adoption of such technology. The full text is available on request from me by email.
It deals with the tricky issue of how to erase or “sanitize” data in running software, so that it can’t be observed. Many coding standards and guidance documents for secure software say that we should do this for “sensitive” data such as the plaintext of passwords, cryptographic keys, and so on, but offer very little technical advice on how to do it properly. I had to implement this kind of thing for a recent development project and it turns out to be much harder to get right than you might think. The paper describes why it’s hard, what you can do about it.
Post conference note: the “further work” section proposes a special compiler switch that automatically erases local data before it goes out of scope. Recently, I have discovered that this has actually been implemented in LLVM by the team at Embecosm. See their blog entry here for details. It doesn’t look like their work has been contributed upstream to the main LLVM sources yet.
Stop press: I was awarded “Best presentation” for my talk on this work.
There’s a great article in the latest issue of ACM Queue about the effects of uninitialized variables in C by Robert Seacord. See here https://queue.acm.org/app/
Robert is a noted expert and was the principal author of the CERT C Coding Standard, so he really does know what he’s on about. The good news: the article is the most complete and up-to-date treatment of this topic that I know of – I certainly learned lots from it, especially with regard to what C’11 has to say. The bad news: it’s worse, much worse, than you think…
Question: would it be possible to define a subset of C which is both useful and guarantees sound data-flow analysis in P-Time? I fear the answer is “no”… ho hum… I’ll stick to SPARK thanks… 🙂
Well…not sure how this happened, but out of some 170 proposals, I’ve been asked to speak at BrisTech 2016 in November. This looks like a really interesting event, and way out of my normal comfort zone, so looking forward to it. Check out the other speakers and the full programme at 2016.bris.tech
For a while now, I’ve been working with my colleagues at Altran on “High Integrity Agile” – basically trying to work out how we can combine the best bits of the Agile Manifesto with what we already know from Lean, Formal Methods, Correctness-by-Construction, TSP and so on. The other week I gave a short talk on the subject at the invitation of Chris Hills from Phaedrus Systems. This covers a few of the issues we’ve encountered so far. Chris has posted a lightly-edited video of the talk, and I’m pleased to say that I didn’t appear to say anything overtly stupid or embarrassing, so here it is…
Many thanks to Altran UK for supporting this work, and approval to post the video.
I’m pleased to see that the “all new” SPARK book was published this week. The book is by long-time SPARK users John McCormick and Peter Chapin. John has taught SPARK for many years as part of his real-time systems lab courses at UNI, while Peter is mainly known for his involvement in the remarkable Vermont CubeSat project, where the team used SPARK for the in-flight software.
The new book covers SPARK 2014, of course, in all its glory and the latest GPL release of the toolset. It’s aimed at an audience coming to SPARK (and Ada) for the first time, but it should also
be useful for those familiar with SPARK 2005.
The opening chapters covers the basics – SPARK’s type system, subprograms, packages and so on, before moving on to the more meaty stuff such as contracts, proof, and design issues.
The latter topic is particularly welcome – we always found that “design for verification” was a key driving force in the success (or otherwise…) of SPARK projects, but this topic was hardly touched on by other languages and design approaches.
I hope the book reaches a new audience of professors, students and engineers, raising awareness of SPARK and what it can do. A big thanks to John and Peter for their hard work in putting it together.
I was lucky enough to attend and speak at this event in London on 25th June. I was talking about recent work I’ve been doing for a client on “High Integrity Agile” – basically trying to find the right combination of Lean, Agile, and Formal approaches for a high integrity project.
The speakers also included Felix Redmill, speaking about his experience with “Evolutionary Development” in the 1980s that led to his excellent (and recently re-published) book on the subject.
The key-note speaker was Professor Bertrand Meyer, whose recent book “Agile: The Good, the Hype and the Ugly” has caused something of a stir. The book is a plain-speaking critique of the Agile approach and doesn’t pull its punches. There’s also an on-demand version of a recent ACM webinar that Bertrand gave on the same subject which is worth a look.
Slides from the SCSC event are now available here.
Update: a short video shot at the event is now available here.
For a long time at Praxis/Altran, we tried to publish results from projects,
particularly those using SPARK. Sometimes we succeeded, but more often than
not the projects or clients weren’t happy with the idea, so the projects
and their results remain pretty much invisible.
I wanted to write a review paper going over all the projects for a while,
and the opportunity finally arose with this year’s Interactive Theorem Proving
Conference (ITP 2014) in Vienna, where I was asked to deliver some sort of keynote.
So…we sat down and tried to write a “life and times of theorem proving
with SPARK”, starting with the SHOLIS project in 1995, and (finally!)
closing with some data from the NATS iFACTS project and some other more
recent efforts. We also decided to alternate the project stories with
the technical developments in the language and toolset, so the story
closes with a preview of SPARK 2014, which is basically a complete
reboot of the language and toolset.
In the Summer, I was in the middle of setting up Protean Code and doing
a few other things, so I couldn’t attend the conference in the end, but
Florian Schanda from SPARK team was able to go in my place, and did a great
job presenting the story.
Having actually read Springer’s copyright assignment form for the N’th
time, I realised that I could put it up here for those that don’t have
access to LNCS online.