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 testcases, 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.
Yet software is deeply rooted in uncertainty making pragmatic assurance more inductive than deductive: most of complex open-world functionality is either not completely specifiable (due to uncertainty) or it is not cost-effective to do so, and deductive verification cannot happen without specification. Inductive assurance, achieved by sampling or testing, is easier but generalization from finite set of examples cannot be formally justified. And of course the recent popularity of constructing software via machine learning only worsens the problem. Then how can we successfully argue about safety and security of software under all this uncertainty, and without fully sound and complete methods?
This talk will aim to tease apart the ultimately intertwined notions of argument and uncertainty in order to identify research opportunities to make progress with software assurance.
|Marsha Chechik's Keynote Slides (Marsha_Chechik-etaps2019-final.pdf)||4.21MiB|
Marsha Chechik is Professor and Bell University Labs Chair in Software Engineering in the Department of Computer Science at the University of Toronto. Prof. Chechik’s research interests are in modeling and reasoning about software. She has authored over 100 papers in formal methods, software specification and verification, computer security and requirements engineering. Marsha Chechik has been Program Committee Co-Chair of a number of conferences in verification (TACAS’16, VSTTE’16, CONCUR’08) and software engineering (ASE’14, FASE’09, CASCON’08), and is gearing up to co-chair the technical program committee of the 2018 International Conference in Software Engineering (ICSE’18). She has been fortunate to work with many extremely talented graduate students and postdocs, some of whom are now on faculty in top universities in Canada, the US, Chile, Luxembourg, and China.