|
GC6: Dependable Systems Evolution
|
IntroductionContextIndustrial software usually has extensive documentation, but software behaviour often comes as a complete surprise. Depending on the circumstances, these surprises can range from the disastrous to the merely annoying. Why should software not behave as expected? Programming is inherently hard because we have to reduce a problem to a set of rules that can be blindly followed by a computer. This process is error prone, and this is compounded by components interacting and interfering, and undesirable properties emerging. The result is that systems often fail to satisfy their users’ needs. Software is also inherently hard to develop. It’s hard to define requirements, to anticipate interactions, and to accommodate new functionality. Documentation involves large amounts of text, pictures, and diagrams, but these are often imprecise and ambiguous. Important information is often hidden by irrelevant detail. Design mistakes are often discovered too late, making them expensive or even impossible to correct. It’s a tribute to the skill of software engineers that systems work at all. DependabilityA new technological product or system is dependable if, from its initial delivery, it justifies the confidence of its users in its soundness, security, and serviceability. When the design of a system evolves to meet new or widening or changing market needs, it should remain as dependable as on initial delivery. Dependability in the face of evolution is currently a significant challenge for software systems, on which society increasingly depends for its entertainment, comfort, health, wealth, and survival. Another way?Some practitioners in industry and researchers from universities believe it’s now practical to use formal methods to produce software, even non-critical software. And that this will turn out to be the cheapest way to do it. Given the right computer-based tools, the use of formal methods could become widespread and transform the industrial practice of software engineering. The computer science community recently committed itself to making this a reality within the next fifteen to twenty years. Recent advances in theory and tool support have inspired industrial and academic researchers to join together in an international Grand Challenge (GC) in Verified Software, with a sense of urgency in making its objectives a reality. Tony Hoare has summarised the purpose of the challenge: "A mature scientific discipline should set its own agenda and pursue ideals of purity, generality, and accuracy far beyond current needs." To meet this challenge we propose to elucidate and develop the basic scientific principles that justify confidence in the correct behaviour of software systems, even in the face of extreme threats. We propose to exploit these principles in co-operative development of a strong software engineering toolset to assist in design, development, analysis, testing, and formal verification of computer software systems of any size throughout their evolutionary life. We propose to evaluate and improve the tools by competitive testing against a representative range of challenge problems taken from real computer applications. And we propose to assist the producers of commercial programming toolsets to adopt the improved verification technology in their widely marketed products. DeliverablesOur Grand Challenge has two central principles: theory should be embodied in tools; and tools should be tested against real systems. These principles are embodied in our two main current activities: the creation of a strong software engineering tool-set; and the collection of an appropriate range of examples. The challenge is to achieve a significant body of verified programs that have precise external specifications, complete internal specifications, and machine-checked proofs of correctness with respect to a sound theory of programming. At the end of the project, we will have the following deliverables:
Verified Software Repository
A Scientific Repository is a selected collection of scientific data constantly accumulating from experimental or observational sources, together with an evolving library of programs that process the data. The Verified Software Repository (VSR) is a scientific repository serving the advancement of Computer Science, particularly in the area of strong software engineering and the mechanical certification of computer programs. The long-term goal of the repository is to develop a toolset of software engineering aids that could be commercialised for use in the construction, deployment, and continuous evolution of dependable computer systems.
Work has started on creating the VSR, prompted by meetings funded by EPSRC in the UK and NSF in the USA, with two initial activities:
Work is also underway in China, Brazil, and other European countries. |
|
Contact: jim@cs.york.ac.uk Last updated: 6th December 2007 |