ECE Seminar: Prove If You Can, Test If You Cannot
Friday, October 20, 2017 - 12:00pm to 1:00pm
Rance Cleaveland, Professor of Computer Science, University of Maryland at College Park
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 describes an approach, called instrumentation-based verification, that is intended to realize this vision. Examples from the automotive domain will be used to illustrate the application of the work.