Verification Extensions for Programming Languages

Leader: Peter Welch <p.h.welch@kent.ac.uk>
Estimated time: 1 hour plus

Background

As the world becomes dependant on computer systems to sustain and advance its way of life, the correctness and, therefore, safety of those systems becomes essential. Yet the reliability of the software controlling our computers has barely improved over the past few decades, even as the speed with which they can go wrong has risen exponentially.

Software verification is not part of the normal practice of software engineering, probably because it is perceived to be too difficult and is, currently, so time consuming compared to the practice of generating code ("with no obvious deficiencies", C.A.R.Hoare). Instead, verification is reserved for software whose failure would certainly kill or injure people (e.g. certain elements of flight avionics) or lose lots of money (e.g. banking services).

The difficulties of verification must therefore be removed. It is the responsibility of mathematicians and engineers with the rare specialist skills needed (today) for verification to find ways to do themselves out of this particular line of work. They can do this by building those skills into the tools used daily to construct code: most notably, programming languages.

At present, there is a disabling disconnect between the languages used for programming and those for formal analysis and model checking. Bridging that gap with specialists is too expensive and brings in too many delays for standard practice. Even for those critical applications where that effort is applied, there is danger: relying on humans to associate program code with model checking scripts and get it right every time is not credible. And that association has to be remade each time the system is changed.

History

At CPA 2011, a proposal was made to start addressing the above (Adding Formal Verification to occam-pi). The proceedings (and the link just given) only hold an abstract for that presentation, but details are in the accompanying slides. More information, however, is in two sets of slides updated from those at CPA 2011 for talks given later that year: Self-Verifying Concurrent Programming (PPT version) and Self-Verifying Dining Philosophers (PPT version).

The second of these sets demonstrates use of the proposed occam-pi extensions for an implementation of the Dining Philosophers' college. Freedom from deadlock and livelock is verified for any number of philosophers (this side of infinity) through model checking the base and induction steps of an induction argument. For fun, and totally unnecessary given the induction proof, a direct verification deadlock freedom for a college with (10^2000 + 1) philosophers is given, demonstrating the somewhat black art of compression available in FDR – but from the level of occam-pi.

The above slides give details for the translation from occam-pi into CSP-M, allowing the programmer to make FDR-like assertions and set the level of abstraction in the translated model (e.g. which variable values are tracked) sufficient for the assertions to hold (or fail), but not so light that the state space is too vast even for FDR to explore. The examples from the slides were verified using FDR2, with hand translation from occam-pi to CSP-M using the rules given.

Action

Following CPA 2011, I was hopeful that we would be able to produce a working demonstrator within a year. This would require extending the occam-pi compiler to generate CSP-M scripts, feeding the scripts through FDR and re-presenting the results to the programmer in terms of the occam-pi sources. Earlier work on a prototype translator from raw occam to CSP was reported by Fred Barnes in a fringe presentation at CPA 2008 (Towards Guaranteeing Process Oriented Program Behaviour). Unfortunately, modern academic life is such that compiler effort at Kent has stalled.

The aims of this workshop are therefore:

• re-consider the CPA 2011 proposal;
• change it in the light of relevant happenings since then;
• change it because someone has better ideas;
• identify the tasks for building (at least) a demonstrator implementation;
• size those tasks (time and effort);
• find people, including end-users, willing to take this further.

Finally, we note (and understand some of the reasons for) the low level of interest remaining for occam. The ideas of this workshop are not confined to occam, though they were inspired by it and it would be easiest (technically) to start from there. The workshop should also consider re-shaping all these ideas for other languages, though they would need to offer a concurrency model fairly closely compatible with CSP. Candidates might include Go, Java (with JCSP) and Scala (with Bernard Sufrin's CSO, first presented at CPA 2008).