GC6: Dependable Systems Evolution

 

Home
Up

Status 2006

The GC6 Steering Committee comprises Jim Woodcock (York, convenor), Cliff Jones (Newcastle), and Peter O’Hearn (Queen Mary). Much of our work is in collaboration with the International Grand Challenge in Verified Software.

International Grand Challenge in Verified Software

The International Grand Challenge in Verified Software is a  long-term, coordinated programme of research addressing the theoretical, practical, technological, pedagogical, and sociological challenges facing large-scale software verification. Members of the UK Grand Challenge GC6 have been helping to define the International Challenge by developing a Research Roadmap.

The key points of the Research Roadmap are summarised below.

  • Verification technology is critical to the design, implementation, and maintenance of reliable software. It can reduce the cost of developing, using, and maintaining highly reliable software. Current approaches to software development inspire little confidence—even widely used software contains large numbers of bugs.

  • Formal verification technology is advancing rapidly on a number of fronts and is ready for large-scale experiments to measure progress and stimulate further improvements in the performance, robustness, and functionality of this technology.

  • The Verified Software Challenge is aimed at achieving concrete progress through cooperation and competition based on small, medium, and large-scale published benchmarks. The benchmarks, tools, and experimental results will be published on a verified software repository to coordinate the activities of the Verified Software project. The enhancement and combination of existing tools and also the invention and exploration of radical new approaches are proposed. The training of software engineers in the advanced use of verification technology is critical to achieving greater software reliability.

  • The research thrusts will include theory (e.g., mathematics and logic supporting verification and verification tools), methodology (e.g., specification, verification and correct-by-construction techniques), and tools (e.g., property checkers, theorem provers and integrated verification environments).

  • The research agenda will be driven by realistic experiments, both in the form of small-scale pilot projects that are used to benchmark the technology and identify research challenges, as well as large-scale experiments.

  • To be deemed successful, the verification challenge must yield a comprehensive and convincing verification of one or more substantial software artifacts such as a web server or an operating system kernel.

GC6 Pilot Projects

Mondex

Our major activity this year has been the year-long Mondex pilot project, which was launched in January 2006. Its main objectives were: (1) to demonstrate effective collaboration and competition amongst the verification community; (2) to generate artefacts to populate the Verified Software Repository; and (3) to assess the current state of proof mechanisation. The problem was to verify a key property of the Mondex smart card, an electronic purse hosted on a smart card. This product was developed to the high-assurance standard ITSEC Level E6 by a consortium led by NatWest, the UK high-street bank. Mondex purses interact using a communications device, and strong guarantees are needed that transactions are secure in spite of power failures and mischievous attacks. It must not be possible to counterfeit electronic cash. The problem is compounded by transactions being completely distributed: there is no centralised control, with all security measures being locally implemented with no real-time external audit logging or monitoring.

The original verification was seriously security critical, so Logica and the University of Oxford used the Z notation for the development process. They constructed formal models of the overall system and an abstract security policy. They carried out proofs by hand that the system design possesses the security properties. The abstract security policy specification is about 20 pages of Z; the concrete specification (an n-step protocol) is about 60 pages; and the verification (suitable for external evaluation) is about 200 pages of refinement proof and 100 pages of derivation of refinement rules.

The original proof was carefully structured for understanding, a fact much appreciated by the Mondex case study groups. The original hand proof was vital in getting the required certification; it was also useful in finding and evaluating different models. The original team made a key modelling discovery by finding an abstraction that gave a precise description of the security property and explained why the protocol is secure. The original proof revealed a bug in the implementation of a secondary protocol. The failed proof explained what had gone wrong, and provided a convincing counterexample that the protocol was flawed and gave the insight to correct the design. Third-party evaluators also found a bug: an undischarged assumption

The sanitised version of the Mondex documentation is publicly available as Z specifications of security properties, abstract specification, intermediate-level design, concrete design, and rigorous correctness proofs of security and conformance. Originally, there was no question of mechanising proofs, as it was thought that mechanising such a large proof cost-effectively was beyond the state of the art. The challenge was to investigate the degree of automation that can now be achieved in the correctness proofs.

 Eight groups took up the challenge and started regular meetings to discuss their work. Teams represented Alloy (MIT), Event-B (Southampton), OCL (Bremen), PerfectDeveloper (Escher), ambient calculi (Newcastle), Raise (Macao/DTU), and Z (York). They agreed to work for one year, without funding. Meanwhile, separately and silently, a group in Augsburg began work using KIV and ASMs.

Two distinct approaches emerged. The Archaeologists made as few changes as possible to the original documentation. They reasoned that they should not change the models just to make verification easier: how would they know that their results had anything to do with the original specification? The Technologists wanted to use the best proof technology now available, but these new tools do not work for Z. They had two choices: translate the existing models into new languages, or create new models better suited to new tools.

The project demonstrated the following results. 

  1. Mondex was verified by almost all the teams, generating about the same number of verification conditions, with about the same amount of automation, within the same amount of time (about six weeks of effort).

  2. That such a project helps to develop expertise and produces reusable mechanised theories.

  3. That the verification community is willing to undertake competitive and collaborative projects, and that there is some value in doing this.

Other GC6 Pilot Projects

Work has started on a second pilot project: a space-flight file-store in collaboration with Rajeev Joshi and Gerard Holzmann at JPL. Other proposed pilot projects include domain modelling and verification of electronic voting systems and verification of key properties of an open-source web server.

GC6 Workshops

We held the following workshops.

  • 2nd Mondex Workshop 27th–26th May, Cosener’s House, Rutherford Laboratory.

  • 3rd Mondex Workshop 5th–6th October, University of York.

  • Early Starters’ Workshop 18th–19th December, University College Dublin.

Papers Published

  • Tony Hoare. The Ideal of Verified Software. Proceedings CAV2006 Computer Aided Verification, 18th International Conference, Seattle, August 17–20, 2006. Thomas Ball and Robert B. Jones (editors). Lecture Notes in Computer Science 4144:5–16 Springer (2006).

  • Jim Woodcock. Verified Software Grand Challenge. Jayadev Misra, Tobias Nipkow, and Emil Sekerinski (editors). Proceedings FM 2006, 14th International Symposium on Formal Methods, Hamilton, Canada, August 21–27, 2006. Lecture Notes in Computer Science 4085:617–617 Springer (2006).

  • Jim Woodcock, Leo Freitas. Z/Eves and the Mondex Electronic Purse. Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone (editors). Theoretical Aspects of Computing—ICTAC 2006, Third International Colloquium, Tunis, November 20–24, 2006. Lecture Notes in Computer Science 4281:15–34 Springer (2006).

  • Juan Bicarregui, C. A. R. Hoare, J. C. P. Woodcock. The verified software repository: a step towards the verifying compiler. Formal Aspects Computing 18(2):143–151 (2006).

  • Cliff Jones, Peter W. O’Hearn, Jim Woodcock. Verified Software: A Grand Challenge. IEEE Computer 39(4):93–95 (2006).

  • Jim Woodcock. First Steps in the Verified Software Grand Challenge. IEEE Computer 39(10):57–64 (2006).

Meetings Organised

  • Dagstuhl Seminar 06281: The Challenge of Software Verification. Manfred Broy (TU München), Patrick Cousot (ENS, Paris), Jayadev Misra (Univ. of Texas at Austin), and Peter O’Hearn (Queen Mary) (organisers). 9–14 July 2006. Sponsored by Microsoft Research, Cambridge.

  • Grand Challenges of Informatics: An Academia Europaea/Charles Simonyi/John von Neumann Computer Society International Symposium. Budapest, Hungary, 19–20 September 2006. Dines Bjorner (organiser).

Conference Keynote Talks

  • SEW-30: 30th Annual IEEE/NASA Software Engineering Workshop. Loyola College Graduate Center, Columbia. 25–27 April 2006. Keynote talk: Jim Woodcock, Verified Software Grand Challenge.

  • 1st Asian Working Conference on Verified Software. UNU/IIST Macao. 29–31 October 2006. Keynote talk: Jim Woodcock, The Repository: 1,000,000 lines of verified code.

GC6 Grant Proposals

EPSRC UK/China Network on Verified Software. Submitted, but rejected. The only feedback was as follows:

This proposal presents a network at the leading edge of software engineering, with a long research horizon of up to 15 years. The proposal represents a good team with well written aims and objectives. The activities of the network are clearly explained. The network continuity is strong and there is an extensive list of supporting letters. Industrial support is, however, a little thin. It is recognised that software engineering projects do need group work, but the proposal would be strengthened by placing more emphasis on the benefits and advances to software development that this network could bring. As a ’fact-finding’ study, it is fine, but further reach beyond these activities would be beneficial. The applicant may wish to consider a smaller pilot study through standard EPSRC mechanisms to establish the groundwork for a larger proposal covering more detail. Overall this is a solid proposal with some good ideas and methodology, but is slightly scored down for absence of detail on the potential return on this investment.

Tools and Guidelines for Preserving and Accessing Software Research Outputs. Application to JISC Repositories and Preservation Programme.

Outline Project Description  Many research outputs come in the form of software and its associated artefacts such as documentation, install scripts, test cases, tutorials, etc. This project will investigate issues around the deposition and preservation of software artefacts in repositories. It will develop guidelines for preservations of software research outputs, in particular, considering the appropriate use of existing software repositories such as sourceForge. It will develop these guidelines from the partners’ experience in running a number of software repositories and in particular by monitoring and analysing in detail the activities around a particular case study which is a thematic software repository in the software engineering domain. The project will focus particularly on:

  1. The classification of software artefacts to enable their retrieval and use in new contexts.

  2. The preservation of software artefacts as their associated environment evolve.

  3. The role of standards in preservation of software.

  4. The process of depositing software as part of the research project workflow to enable validation of analyses undertaken in the course of the research lifecycle.

More generic issues related to preservation of digital objects in general will not be considered here as they are well covered by other projects in this and other programmes.

Meetings Planned

  • GC6 Conference. Autumn 2007. Cambridge. Sponsored by Microsoft Research.

  • Workshop on Industrial Verification Problems. Microsoft Cambridge. 2007.

  • VSTTE 08: Verified Software: Theories, Tools, and Experiments. 2nd International Conference. 6th–9th October 2008, Toronto. Eric Hehner (local organiser).

  • Workshops are planned for the following conferences: IFM 2007, ICECCS 2007, ICTAC 2007.

  • Royal Society Meeting for Discussion. Planned for 2008.

Other GC6 Activities

Mailing list established. Wiki/Repository established.

Contact: jim@cs.york.ac.uk

Last updated: 6th December 2007