Four universities are collaborating in a five-year, $10 million project to move software development from an art to a science, creating formal methods of developing and verifying software to eliminate bugs, glitches and flaws.
The program is the Science of Deep Specifications, or DeepSpec. Its goal is to apply formal logic and precise specifications for software behavior to create verifiably sound software, avoiding the unintended consequences of today’s development practices. Researchers want to bridge the gap between themselves and the educators teaching the programmers and engineers who create software. The principal investigator for the program is Andrew Appel of Princeton. Also participating are the University of Pennsylvania, Yale and the Massachusetts Institute of Technology.
DeepSpec is one of three Expeditions in Computing projects announced Jan. 7 by the National Science Foundation. The projects will be sharing $30 million in federal funding. Expeditions in Computing began in 2008 and has provided about $190 million for 19 projects. Other programs in the current round involve evolvable living computing and computational sustainability.
The task of ensuring reliable software is particularly challenging because bugs are not just mistakes in coding. Mistakes are relatively easy to identify and eliminate. But many bugs are the result of unforeseen uses and interactions of otherwise sound features in the code, which can have unwanted results in the form of errors or vulnerabilities. Solving this challenge is increasingly critical as more of our economy, security and everyday lives become dependent on IT.
“The researchers’ initial challenge will involve dissecting the complexity of modern hardware and software to uncover factors that determine how various computer components work together,” according to Princeton’s computer science department. Researchers then will develop “deep specifications,” detailed descriptions of the expected behavior of software elements based on formal logic. These are intended to let engineers not only build bug-free programs, but also verify that the programs perform as intended.
“Using formal logic is good, because then we can verify programs using automated provers and proof-checkers, to guarantee that module implementations satisfy their specifications,” the DeepSpec Web site says.
This certainty is not possible in the usual software development process today. The lack of institutional knowledge and of communication among developers working on different tasks within a project result is unintended consequences in complex software-hardware environments.
The project will build on the work of CompCert, a French project on which Appel also worked that developed a software compiler that can be proven to accurately translate programming language into code. This provided a proof of concept for deep specifications in software development. DeepSpec will carry on by creating a full set of verifiable compilers, operating systems, program analysis tools and processor architectures using deep specifications. The resulting specifications will be open source.
“It would be a major breakthrough to build the coherent system of specified/verified components that we have in mind,” the Web site says.
This is a tall order, but five years, $10 million and the brainpower of four major computer science programs might be able to accomplish it. The next big challenge will be to see that this new model is incorporated into real-world software development.