|Title:||Verification Extensions for Programming Languages|
|Conference:||Communicating Process Architectures 2014|
Peter H. Welch
School of Computing, University of Kent
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 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 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.
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).