Overview
Typically, certification that a software intensive critical system is safe and secure is provided by an assurance case. This presents an argument built on evidence from the developed system. Creating this argument is a complex, time consuming task. The talk will describe how the assurance argument should be constructed hand-in-hand with the development of the system, and how the system development can include analyses that facilitate building the assurance argument.
Abstract
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. Software failures due to design flaws and bugs in software can be costly. These flaws are extremely expensive to fix once the software has been deployed. Safety-critical software systems need assurance that the software operates safely and securely prior to deployment. Such systems must therefore be designed with rigorous claims supported by reliable, reproducible, and maintainable evidence. We motivate the need for constructing software hand-in-hand with an assurance argument backing the critical safety and security claims. We describe some technologies that we have been developing to assist with design for certification. 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. The talk presents joint work with members of the DesCert (Design for Certification) team.
Speaker
Dr. Natarajan Shankar is a Distinguished Senior Scientist and SRI Fellow at the SRI Computer Science Laboratory. He received a BTech degree in Electrical Engineering from the Indian Institute of Technology, Madras, and PhD in Computer Science from the University of Texas at Austin. He is the author of the book, “Metamathematics, Machines, and Godel’s Proof” (Cambridge University Press) and the 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.
Event details
Join us on March 7 at 2:30 p.m – 3:30 p.m. in the Michael DeGroote Centre for Learning and Discovery, Room 1102.