Abstract: Control engineers use tools like MATLAB(r), Simulink(r) and Stateflow(r) to develop models of control systems for applications such as anti-lock braking and flight control. These models may be simulated, and the simulation results used to predict behavior of the eventually implemented controller. The models also hold promise as specifications for the on-board software that controls systems now routinely include. This talk will discuss how such models can be used to improve embedded software development, and how they may themselves best be verified against system requirements. Specifically, we introduce the notion of instrumentation-based specification and show how it may be used in support model verification and validation.

Rance Cleaveland is Professor of Computer Science at the University of Maryland in College Park, where he is also Executive and Scientific Director of the Fraunhofer USA Center for Experimental and Software Engineering. He has published over 100 papers in the areas of formal methods, model checking, software specification formalisms, and verification tools. In 1992 he received Young Investigator Awards from the National Science Foundation and from the Office of Naval Research. Cleaveland obtained 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. He is a member of IEEE, the Association for Computing Machinery, and the Society for Automotive Engineering. He is also co-founder and Chairman of Reactive Systems Inc., a model-based V&V company.