Date and Time: Thursday, 27 August 2009, 10:00 - 11:00

Location: HG 6.96

Speaker: Rance Cleaveland (University of Maryland, USA)

Title: Validating Automotive Control Software using Instrumentation-Based Verification

Abstract:

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.