Therefore, we from Bosch provided a concrete automotive benchmark for the Formal Methods for Timing Verification (FMTV) challenge 2016, a full blown performance model of a modern engine management system (downloadable http://www.ecrts.org/forum/viewtopic.php?f=27&t=62), with the goal to challenge existing timing analysis approaches with respect to their expressiveness and precision.
The focus of the challenge lies on determining tight end-to-end latency bounds for a set of given cause-effect chains. This is challenging since the dynamic behavior of a engine management software is quite complex and contains mechanisms that explore the limits of existing academic approaches:
- preemptive and cooperative priority based scheduling
- periodic, sporadic, and engine synchronous tasks
- multi-core platform with distributed cause-effect chains including cross-core communication
- label (i.e. data) placement dependent execution times of runnables
