Synthesising Optimal Timing Delays for Timed I/O Automata

Abstract

In many real-time embedded systems, the choice of values for the timing delays can crucially a ect the safety or quantitative charac- teristics of their execution. We propose a parameter synthesis algorithm that nds optimal timing delays guaranteeing that the system satis es 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 Tem- poral 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 simpli ed model of a pacemaker. We are able to synthesise timing delays that ensure with high probability that energy usage is minimised,