Synthesising Optimal Timing Delays for Timed I/O Automata

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.