[DKKM14b]
M. Diciolla, P. Kim, M. Kwiatkowska and A. Mereacre.
Synthesising Optimal Timing Delays for Timed I/O Automata.
Technical report RR-14-07, University of Oxford.
September 2014.
[pdf]
|
Abstract.
In many real-time embedded systems, the choice of values for the timing
delays can crucially affect the safety or quantitative characteristics
of their execution. We propose a parameter synthesis algorithm that
finds optimal timing delays guaranteeing that the system satisfies a
given quantitative property. As a modelling framework we consider
networks of Timed Input/Output Automata (TIOA) with priorities and
parametric guards. To express system properties we extend Metric
Temporal Logic (MTL) with counting formulas. We implement the algorithm
using constraint solving and Monte Carlo sampling, and demonstrate the
feasibility of our approach on a simplified model of a pacemaker. We are able to synthesise timing delays that ensure with high probability
that energy usage is minimised, while maintaining the basic safety property of the pacemaker.
|