Seminars & Meetings | Abstracts

December 7, 2009

Rance Cleaveland
Department of Computer Science
University of Maryland
Validating Automotive Control Software using Instrumentation-Based Verification


This talk discusses the results of an application of a formally based verification technique, called Instrumentation-Based Verification (IBV), to a production automotive lighting controller. The goal of the study is to assess, from both a tools as well as a methodological perspective, the utility of IBV in an industrial setting. In IBV, requirements are formalized in terms of so-called "instrumentation" that inspects the behavior of software to search for violations of the associated requirements. The insights obtained as a result of the project include a refinement of a previously developed architecture for requirements specifications; observations about changes to model-based design workflows; insights into the role of requirements during development; and the capability of automated verification to detect inconsistencies among requirements as well as between requirements and design models.


Rance Cleaveland is Professor of Computer Science at the University of Maryland at College Park, where he is also Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. Prior to joining the Maryland faculty in 2005, he held professorships at the State University of New York at Stony Brook and at North Carolina State University. He also co-founded Reactive Systems, Inc., in 1999 to commercialize tools for model-based testing of embedded software; Reactive Systems currently has numerous customers worldwide in the automotive and aerospace industries. In 1992 he received Young Investigator Awards from the National Science Foundation and from the Office of Naval Research, and in 1994 he was awarded the Alcoa Engineering Research Achievement prize at North Carolina State University. He has published over 100 papers in the areas of software verification and validation, formal methods, model checking, software specification formalisms, and verification tools. Cleaveland received B.S. degrees in Mathematics and Computer Science from Duke University in 1982 and his M.S. and Ph.D. degrees from Cornell University in 1985 and 1987 respectively.