Abstract: Current formal methods focus on mathematical proof as a means for establishing that a system is correct with respect to a formal specification. This perspective can limit the applicability of formal methods, since the development of such proofs remains a very difficult task requiring specialized expertise, even with computer assistance. This presentation argues that formal-specification approaches that support both proof and testing as V&V technologies can enhance the practical usefulness of formal methods. It then shows how this observation can be put into practice in the context of model-based testing of automotive control software, in which the so-called back-to-back testing strategy for software is supported using the Reactis® test-generation tool for Simulink® / Stateflow® models of control systems.

Biography: Rance Cleaveland is a Professor of Computer Science at the University of Maryland at College Park; he is currently, since 2018, also serving as Division Director for Computing and Communication Foundations at the National Science Foundation. Prior to joining the UMD faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University (NCSU). He is a co-founder of Reactive Systems, Inc., a company that makes model-based testing tools for embedded software, and a past recipient of National Young Investigator Awards from the National Science Foundation and the Office of Naval Research and the Alcoa Engineering Research Achievement prize from NCSU. He has also won undergraduate teaching awards from UMD and NCSU. He has published over 150 papers in the areas of software verification and validation, formal methods, cyber-physical systems, model checking, software and system specification formalisms, verification tools, and embedded-software testing. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and M.S. and Ph.D. degrees from Cornell University in 1985 and 1987, respectively.