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.