As society becomes ever more dependent on computer systems, effective (and cost-effective) methods for assurance and certification are becoming critical. The field of formal verification has recently benefited from a surge of innovations in technology and in methods for combining technologies. These innovations, and especially their use in combination, are disruptive to traditional formal verification tools, which are mostly each built around a single technology.
This project seeks to harness and advance disruptive innovation in formal verification by constructing an Evidential Tool Bus (ETB) that will allow many different techniques to be applied cooperatively and in novel combinations to formal verification problems. The ETB supports the need for improved certification methods by managing the integration not only of its client tools, but also of the evidence that they supply. The goal of the ETB is to develop coherent chain of evidence from multiple sources, together with the provenance of each link in the chain. Formal logic and state machines are central concepts in verification. The ETB employs a simple ontology based on these concepts and an equally simple invocation model based on semantic interaction to create a lightweight, loosely coupled service-oriented architecture for formal analysis and verification.
The project is developing a prototype ETB, which integrates tools from SRI and cooperating universities and research organizations. The ETB prototype is being used to perform formal verifications and develop certification evidence that will be made available as exemplars through the international Verified Software Grand Challenge Repository. The ETB is expected to prove a transformative resource for formal verification research and ultimately for certification.
