Escher Technologies - grand challenge 6

The UKCRC has set up a number of Grand Challenges in computer science. Grand Challenge 6, in which Escher Technologies is particularly involved, is that of Dependable Systems Evolution.

One activity within GC6 is that various formal methods tools, including our own Perfect Developer, are being used to revisit the Mondex electronic purse specification and refinement. These were originally carried out in Z and proved manually. The current aim [2006] is to evaluate the state of the art in mechanizing the specification, refinement and proof.

Group meeting January 2006 (photograph courtesy of Jonathan Bowen)

Back row: Jonathan Bowen, Steve King, Jim Woodcock, Cliff Jones, David Crocker, Michael Butler
Front row: Neil Evans, Alvaro Arenas, Tahina Ramananandro, Juan Bicarregui, Martin Gogolla

Taking the picture: Paul Boca

Escher Technologies Ltd has already been involved with Mondex, notably in September 2004, at a meeting of the Refinement Network at York University, where PD successfully verified the abstract model of the Mondex electronic purse. The original Z specification was translated by hand to Perfect in less than one hour, whereupon Perfect Developer generated 28 verification conditions and proved them in a little under two minutes. This included the two vital security properties, namely that the total value in all the purses did not increase and that all value lost from the purses could be accounted for.

We believe that this was the first time that the Mondex purse abstract specification was proved correct entirely automatically. We're now hoping to build on this by using PD to produce automatic proofs of the refinement to the concrete model of intercommunicating purses.

The study of verifying compilers as described by Hoare is another topic within GC6. At the GC6 workshop of Formal Methods 2005, David Crocker of Escher Technologies gave a talk entitled Verifying Compilers for Financial Applications (PPT, 2900K). In this presentation, he discussed the different sorts of verifying compiler that might be appropriate when developing investment banking software, outlined the challenges of applying formal methods to complex financial models, and demonstrated formal verification of call-put parity for European options valued using the Black-Scholes model.