Most of this is conventional wisdom – although not always put into practice – so what makes CbyC different? Well, the system specification is written in Z, a formal specification notation based on set theory and first order predicate logic and developed on the seventies by the Programming Research Group at the Oxford University Computing Laboratory (OUCL).
There is a FAQ here and it has a respectable commercial pedigree: in 1992, the OUCL and IBM were jointly awarded the Queens Award for Industry for the use of the Z notation in the production of IBM's mainframe CICS (Customer Information Control System) products.
Praxis has developed tools that help you automate the verification of the specification and the comparison of the unambiguous spec with the equally unambiguous SPARK code.
If the two don't differ, the only opportunity for defects in your system is that the spec solves the wrong problem (you can verify it for completeness and consistency) – the resources that you no longer need for debugging your code can be devoted to analysing the business domain and ensuring that you're solving the right problem.
This really does work, according to Peter Amey, who has metrics (and that in itself is a sign of a mature process) showing a steady decline in delivered defects over the last decade using CbyC and a steady increase in productivity.
"Of course," he says, "we benefit from Moore's Law, all that unused CPU power can power our verification and proving tools."
He seems to be especially proud of the work Praxis did for the NSA: "The NSA concluded two rather interesting things: (1) the formally-based CbyC development was cheaper than traditional approaches and (2) the software we delivered had zero defects," he claims (see Conclusions in the previously-quoted paper here).
So, why aren't we all using SPARK? There are cultural issues, which mean that CbyC is easier to introduce in a greenfield site. People are frightened of math and proof – and Ada. People whose status comes from their prowess in writing and debugging C++ are unlikely to recommend CbyC to their managers.
And adopting CbyC is a bit of a leap of faith for people unused to proof and formal methods – suppose it is only suitable for simple safety-critical embedded systems and can't cope with the complexity of your business processes?
That last one can only be answered by you yourself reviewing the published case studies here – but how safety-critical, for your career, are the financial control systems your CEO signs off (on pain of a possible jail sentence) to the regulators?
But what about all the modern innovations such as eXtreme Programming and UML (or, rather, the world of Model Driven Architecture, MDA, as UML is just a modelling language)? Does CbyC mean throwing these out? Not exactly, says Peter Amey.
In Static Verification and Extreme Programming (published in Proceedings of the ACM SIGAda Annual International Conference, available here), he and co-author Rod Chapman say: "We were both surprised and pleased to find out how much XP we already do on high-integrity projects."
And, they consider that coding with a human designer and a static-analysis tool such as SPARK Examiner is logically equivalent to pair programming as described by Kent Beck. They posit that the reason Beck doesn't talk about static analysis in an XP context is that the depth it can offer in conjunction with imprecise languages like Java is very limited; and the inefficiency (lack of speed) of static analysis tools not written in and working on something like SPARK can make it infeasible.
As for UML, Amey considers that SPARK confers precision onto the UML model and makes verification of the generated code easier (see High-Integrity Ada in a UML and C World, Lecture Notes in Computer Science 3063 here).
In fact, he believes that using the UML modelling process in conjunction with SPARK formal verification and auto-generation of C from validated SPARK can deliver more robust C. Writing in 2004, however, he considers that "the semantics [in UML alone] are not rich enough for the rigorous reasoning we require in the production of quality software".
However, I believe that this may no longer be so true for UML 2.0, potentially at least, partly because of its well-thought-through metamodel, which is designed to facilitate UML extension; and partly because of the level of semantic detail that can be supported with the Object Constraint Language.
MDA already supports many of the principles behind CbyC (such as generating new deliverables by automatic transformation of previous deliverables, rather than by duplicating and rewriting them), and perhaps the future of "formal methods" (as used in CbyC) for general software development could lie in their incorporation into MDA processes.
For more detail on SPARK, read John Barnes' book High Integrity Software: The SPARK Approach to Safety and Security.
As for formal methods generally, there is a wealth of information at Professor John Knight's University of Virginia website here.
Next page: Summary
Next page: Summary
Well, I've written about Formal Methods before. And yes, we only scratched the surface - but a) I thought that treating one company in reasonable (for some value of reasonable) depth was better than the usual whirlwind tour of companies most people haven't heard of, with a bare para on each one; and b) this article was already about as long as could work online.
But I'm happy to cover more formal approaches and in more detail, if those involved can put their case forward as well as, say, Praxis can (I didn't find Praxis through press channels, I was originally impressed by hearing Rod Chapman speaking at a BCS meeting). And, of course, if enough Reg Dev readers express an interest...
BTW, I do realise that Microsoft has now discovered formal methods (I did mention it) but I'm waiting for the weekly bugfix stream to dry up before I get too enthusiastic.
And I'll check out that URL - thanks.
Ahead of the game?
Well, probably CbyC and Bayesian analysis are still ahead of the game. There are certainly development shops where even test automation would be a radical innovation. And possibly, quality in consumer software isn't that important (except that the games industry has to take bugs seriously - and silly bugs in wordprocessors and spreadsheets can really spoil your day).
But I think it's the "attitude" I'd complain about - not that of "QA Helper", who obviously understands the issues and has made a reasoned choice (not necessarily one that I'd agree with, but I could be wrong) as to what is appropriate in particular environments; but the attitude that says "software has bugs, always has, always will; so let's not worry about it".
Software doesn't have to have bugs in it; so if it does, hopefully someone has done a proper risk assessment for defect removal vs. delivery; but perhaps someone just decided that the customer wouldn't mind; or that the customer prefers low cost to quality. Or perhaps the developers are oncompetant - or. more likely, untrained and/or or badly led.
Unrealistic? Well, possibly, but I mostly remember people regretting not getting it right - and stuff delivered too quickly taking even longer to deliver in the end. I also remember Toyota's success with "Lean" and how competitive British Leyland was in comparison.
Remember, (and I do mention cultural issues) that there is some evidence that removing defects with formal methods is CHEAPER than doing it by testing (although you can't replace testing entirely). But perhaps this is only in fields where quality matters - not testing anything is cheapest of all, if someone thinks that production failures don't cost anything.
Nice article, shame it barely scratched the surface
It's nice to see mathematical approaches being mentioned in the mainstream e-press at last. What a shame that the piece on formal methods concentrated on just one company's system and failed to touch on the many other techniques being used.
SPARK may be great for embedded aerospace systems, but if you are developing a large commercial application, you probably want at least basic OO features, like inheritance and polymorphism. Enter Verified Design-by-Contract, ESC/Java, Perfect Developer and Microsoft's Spec# (yes, even Microsoft is looking at FM these days).
Or maybe you want to prove that your software can't get locked up in states from which there is no way out. Try a model checking tool - choose from FDR, Spin, SMV, SLAM... (that last one is from Microsoft again - maybe they're on to something!).
QA Helper argues that writing a formal specification is expensive and time-consuming. Sure it is - but the formal spec is shorter than the code, and quicker to write. The trick is to use the spec to greatly shorten the coding time. We generate most of our code directly from the specification.
Lot more info can be found at the directory of formal methods maintained by Jonathan Bowen of London South Bank University - http://www.afm.sbu.ac.uk/.