Dr. Natarajan Shankar, a Distinguished Senior Scientist and SRI Fellow at the SRI Computer Science Laboratory, Menlo Park, USA gave a Distinguished lecture on Composing High-Assurance Software on 8 February.
Summary of the talk in Dr. Natarajan Shankar’s words: The versatility and flexibility of software makes it an indispensable tool for building critical systems, but its inherent complexity opens up vulnerabilities that can compromise safety and security. High-assurance software systems must be designed with rigorous claims supported by reliable and reproducible evidence and efficient arguments
that magnify the salience of potential flaws and weaknesses. We motivate the need for constructing software hand-in-hand with an assurance argument supporting the critical safety and security claims. We describe some technologies that we have been developing to assist with design for assurance. Specifically, we outline the “efficient argument” approach to system design, the use of formal architectures as a foundation for efficient compositional arguments, ontic type analysis linking the requirements ontology to code-level representations, automatic code generation from high-level specifications, and the Evidential Tool Bus (ETB) architecture for integrating evidence-generating tools within a design workflow for building and maintaining assurance arguments.
Dr. Natarajan Shankar is the author of the book, Metamathematics, Machines, and Godel’s Proof, co-developer of a number of technologies including the PVS interactive proof assistant, the SAL model checker, and the Yices SMT solver. He is a co-recipient of the 2012 CAV Award and the recipient of the 2022 Herbrand Award.
