Abstract modeling of timing properties is often based on events. An event can be seen as a sequence of times. Timing constraints can then be expressed as constraints on events: an example is the TADL2 language that has been developed in the automotive domain.
Event-based constraints can express timing properties of implementations as well as timing requirements. An important step in timing verification is then to show that any events that comply with the properties of the implementation, i.e., that describe the timings of its possible behaviours, also satisfy the requirements.
Real-time software is often organised as a set of periodically repeating tasks, especially in domains with time-critical systems like automotive and avionics. This implementation naturally yields periodic events, where each event occurrence belongs to a periodically repeating time window. An interesting question is then: if some events are periodic in this fashion, will they then fulfil a timing constraint that describes a timing requirement? We show, for a number of TADL2 timing constraints, how to translate this implication into an equivalent Presburger formula. Since Presburger logic is decidable, this yields an automated method to decide whether the periodic implementation satisfies the timing requirements or not. Initial experiments with a Presburger solver indicate that the method is practical.
Björn Lisper recieved his PhD from the Royal Institute of Technology in Stockholm in 1987. He has been full professor in Computer Engineering at Mälardalen University since 1999, where he leads the Programming Languages group. His research mostly deals with analysis of software, such as static analysis, program slicing, and the combination of static analysis and testing. In particular he has focussed his research on WCET analysis. He was the coordinator of the EU FP7 projects ALL-TIMES and APARTS, and he chaired the Cost Action TACLe.
Date & Time: Mon., October 22, 2018, 11:00 s.t.
Venue: CPS-Library, Treitlstraße 1-3, 3rd floor (DE 0328)