Search-Based Testing for Formal Software Verification — and Vice Versa
Shiva Nejati, University of Ottawa
Dijkstra has been frequently quoted as saying “Testing can be quite effective for showing the presence of bugs, but is hopelessly inadequate for showing their absence”. This remark has often been used by the software engineering community to indicate a dichotomy between testing and verification. From practitioners’ point of view, however, there is not much difference in the ways testing and verification techniques may be used in practice. While engineers would try to demonstrate that their systems are correct (verification), they might find themselves in a situation where they have to prioritize bug finding (testing). As a result, the choice to go for formal verification versus testing is largely driven by the practical needs and the context specificities. In this keynote, I will focus on search-based testing and review some recent research that combines ideas from the search-based testing and the formal verification communities to improve the analysis of models of cyber physical systems (CPS). I will present an empirical study comparing CPS model testing and verification, a search-based testing approach for compute-intensive CPS models that adopt a well-known formal verification framework, and automated generation of formal environment assumptions for CPS models using search-based testing and genetic programming.
Shiva Nejati is currently an associate professor at the School of Electrical Engineering and Computer Science at the University of Ottawa. She is also a (part-time) senior researcher at the SnT Centre at the University of Luxembourg. Prior to coming to Ottawa, she was a full-time senior scientist (2012 – 2019) at the SnT Center — University of Luxembourg and a scientist (2009 – 2012) at the Simula Research Laboratory. She received her PhD from the University of Toronto, Canada in 2008. Her research interests are in software engineering, focussing on software testing, analysis of cyber-physical systems, search-based software engineering, applied machine learning and formal and empirical software engineering methods. She has for the past twelve years been conducting her research in close collaboration with industry partners in telecommunication, maritime, energy, automotive and aerospace sectors. She is the (co)-recipient of a number of awards, including four ACM Distinguished paper awards at ICSE, ESEC/FSE and ASE.