Overview

Software is now at the core of our infrastructure. We depend on software to control devices ranging from pacemakers to spacecraft, to manage our banking, communication, and power distribution systems. Most applications of software are benign --- the failure of the software is annoying but of little consequence. However, there are a significant number of applications where software failure can be catastrophic, leading either to the loss or damage to human life or to large financial costs. A study (pdf) conducted by the National Institute for Standards and Technologies (NIST) estimates the yearly cost of unreliable software to be in the range of 20 to 60 Billion US dollars. The RISKS forum maintains a long and growing list of failures that can be at least partially attributed to flawed software. The sciences are increasingly dependent on software to interpret large volumes of data and to validate theories and explanations. Many engineering disciplines increasingly rely on computer-aided design tools. Modern computers are themselves are designed using such tools. Even traditional sciences such as Mathematics, Physics, Chemistry, and Biology depend on computational models. Since software is crucial to the fidelity with which we can observe, model, predict, and manipulate both the physical and the mental world, it is imperative to have a software base that is manifestly reliable and trustworthy.

Already in 1999, the Presidential Information Technology Advisory Committee (PITAC) in a report entitled Information Technology Research: Investing in our Future notes that Software systems are now among the most complex human-engineered structures. ... The Nation needs robust systems, but the software our systems depend on is often fragile. ... Even after large, expensive testing efforts, commercial software is shipped riddled with errors ( bugs )....The Nation cannot afford to let the current situation continue. We must commit to develop the science, technologies, and methods needed to build robust software systems ones that are reliable, fault-tolerant, secure, evolvable, scalable, maintainable, and cost-effective. The report concludes that Technologies to build reliable and secure software are inadequate, and recommends investment in developing The science and methods for efficiently creating and maintaining high-quality software of all kinds, for ensuring the reliability of the complex software systems that now provide the infrastructure for much of our economy \ldots .

The recent 2005 PITAC report on Cybersecurity: A Crisis of Prioritization focuses on security risks stemming from an IT infrastructure that is vulnerable to hostile attacks. It notes that Software development is not yet a science or a rigorous discipline, and the development process by and large is not controlled to minimize the vulnerabilities that attackers exploit. It goes on recommend research in Secure Software Engineering and Software Assurance as research priority, including

• Programming languages and systems that include fundamental security features
• Portable or reusable code that remains secure when deployed in different environments
• Technologies to capture requirement definitions and design specifications that address security issues * Verification and validation technologies to ensure that documented requirements and specifications have been implemented
• Models for comparison and metrics to assure that required standards have been met and to enable evaluation of alternatives
• Technologies to efficiently and economically verify that computer code does not contain exploitable features that are not documented or desired.

The semiconductor industry publishes the International Technology Roadmap for Semiconductors where the key technology trends and metrics are surveyed. The 2005 edition observes: Without major breakthroughs, verification will be a non-scalable, show-stopping barrier to further progress in the semiconductor industry (italics in the original). As with software, testing generates very poor coverage. At the Conference on Automated Verification (CAV 2005), Intel verification expert Bob Bentley noted that accumulated register-transfer level simulation of the Pentium 4 amounted to less than a minute of actual CPU time of a 2 GHz system. The ITRS road map calls for greater focus on robust and structured verification methods and hybrid techniques that combine formal and semi-formal approaches.

The Verified Software project is an ambitious, international, long-term program of research for achieving a substantial and useful body of code that has been formally verified to the highest standards of rigor and accuracy. We argue that such a rigorous understanding of the software infrastructure will also improve our understanding of the physical and the man-made world, and to employ software with a confidence and certitude that is currently lacking.

The Verified Software Grand Challenge was initiated by Professor Tony Hoare to develop an integrated automated tool suite for establishing the total correctness of a significant body of software. A workshop on this topic was held at Menlo Park in February, 2005. An IFIP Working Conference on Verified Software: Theories, Tools, and Experiments was held at Zurich, Switzerland in October 2005.

This document outlines a road map for a research program into verified software. The goal of the research program is to demonstrate the feasibility of using formal verification technology in large-scale software development. The concrete goal of this 15-year project is to achieve

1. A comprehensive theory of program construction and analysis.
2. A comprehensive and integrated suite of tools that support verification activities ranging from specification, validation, test case generation, program refinement, program analysis, program verification, and run-time checking.
3. A significant and widely used collection of formal specifications and verified codes that have been analyzed to the highest standards of rigor.

Our goal for the Verified Software challenge is to develop verification technology to a point where it demonstrably enhances the productivity and reliability with which software is designed, developed, integrated, and maintained. The impact of this work will be felt in a number of related areas of software development including software engineering, safety-critical systems, mathematical modeling, and artificial intelligence.

This roadmap document is a community effort compiling contributions from many of the leading researchers based on the contributions from various workshops and the VSTTE working conference.

Background

• Highlights of Forty Five Years of Verification
• Technical Background
• [[Motivation]]?

Systems and Reliable Software

Pilot Projects

The Mondex Case Study

The first pilot project is an international effort to verify the specification and refinement of the Mondex smart card, an electronic purse for financial transactions. The project brings together researchers working with Alloy, B, Raise, OCL, PerfectDeveloper, VDM, and Z. The most important objective is to bring together an international team for longer term work. Over the next year, we will test the state of the art in mechanical theorem proving, find out how far each group can get, find out what some approaches can do that others can't, and address the question of combining the best of each approach. Since we started, an independent group working with the KIV theorem prover have completed the verification of the specification and its refinements. For more details on the work and the people involved, see The Mondex Case Study.

A Verified Software Repository

[Woodcock/Shankar/Margaria/Kiniry]

The Verified Software Repository (VSR) is a first step towards the realisation of the goals of the Verified Software Challenge. It will maintain and develop an evolving collection of state-of-the-art tools, together with a representative portfolio of real programs and specifications on which to test, evaluate, and develop the tools. It will contribute initially to the inter-working of tools, and eventually to their integration. It will promote transfer of the relevant technology to industrial tools and into software engineering practice. It will build on the recognised achievements of practical formal development of safety-critical computer applications, and contribute to the international initiative in verified software, covering theory, tools, and experimental validation.

The VSR is described more fully in the paper The verified software repository: a step towards the verifying compiler. In the UK, an EPSRC-funded project (VSR-net) is helping to plan the repository. Further details about VSR-net can be found through its wiki.

Research Directions

Experiments

Conclusions