Our weekly SRI Seminar Series welcomes Marsha Chechik, professor and chair of the Department of Computer Science at the University of Toronto. Chechik’s main interests are in software engineering, safety and security assurance, automated verification, software product lines, and model management. Her research focuses on the use of formal methods to improve quality of software, such as scalable automated verification techniques, formal specification languages, verification of protocols, non-classical logics, and reasoning under inconsistency.
In this talk, Chechik contends that safety assurance must be considered as an integral aspect of building reliable software systems. Drawing upon recent innovations for machine learning components (MLCs) in safety-critical domains, she will outline approaches for the development of new methodologies to create and manage safety assurance.
Talk title:
“On safety, assurance and reliability: A software engineering perspective”
Abstract:
From financial services platforms, to social networks, to vehicle control, software has come to mediate many activities of daily life. Governing bodies and standards organizations have responded to this trend by creating regulations and standards to address issues such as safety, security and privacy. In this environment, the compliance of software development to standards and regulations has emerged as a key requirement. Compliance claims and arguments are often captured in assurance cases, with linked evidence of compliance. Evidence can come from test cases, verification proofs, human judgement, or a combination of these. That is, we try to build (safety-critical) systems carefully according to well-justified methods, and articulate these justifications in an assurance case that is ultimately judged by a human.
Building safety arguments for traditional software systems is difficult—they are lengthy and expensive to maintain, especially as software undergoes change. Safety is also notoriously non-compositional—each subsystem might be safe, but together they may create unsafe behaviors. It is also easy to miss cases, which in the simplest case would mean developing an argument for when a condition is true but missing arguing for a false condition. Furthermore, many ML-based systems are becoming safety-critical. For example, recent Tesla self-driving cars misclassified emergency vehicles and caused multiple crashes. ML-based systems typically do not have precisely specified and machine-verifiable requirements. While some safety requirements can be stated clearly (e.g. “the system should detect all pedestrians at a crossing”) these requirements are for the entire system, making them too high-level for safety analysis of individual components. Thus, systems with ML components (MLCs) add a significant layer of complexity for safety assurance.
I argue that safety assurance should be an integral part of building safe and reliable software systems, but this process needs support from advanced software engineering and software analysis. In this talk, I outline a few approaches for development of principled, tool-supported methodologies for creating and managing assurance arguments. I then describe recent work on specifying and verifying reliability requirements for machine-learned components in safety-critical domains.
About Marsha Chechik
Marsha Chechik is a professor and chair of the Department of Computer Science at the University of Toronto. She received her Ph.D. from the University of Maryland in 1996. Chechik’s research interests are in the application of formal methods to improve the quality of software. She has authored over 200 papers in formal methods, software specification and verification, computer safety and security and requirements engineering.
Chechik has been Program Committee Co-Chair of the 2021 International Conference on Foundations of Software Engineering, 2018 International Conference in Software Engineering, 2016 International Conference on Tools and Algorithms for the Construction and Analysis of Systems, the 2016 Working Conference on Verified Software: Theories, Tools, and Experiments, the 2014 International Conference on Automated Software Engineering, the 2008 International Conference on Concurrency Theory, the 2008 International Conference on Computer Science and Software Engineering, and the 2009 International Conference on Formal Aspects of Software Engineering. She is a Distinguished Member of ACM, and Vice-Chair of ACM SIGSOFT.
About the SRI Seminar Series
The SRI Seminar Series brings together the Schwartz Reisman community and beyond for a robust exchange of ideas that advance scholarship at the intersection of technology and society. Seminars are led by a leading or emerging scholar and feature extensive discussion.
Each week, a featured speaker will present for 45 minutes, followed by 45 minutes of discussion. Registered attendees will be emailed a Zoom link approximately one hour before the event begins. The event will be recorded and posted online.
Marsha Chechik