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 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 pro...
| Hoofdauteurs: | , , , |
|---|---|
| Formaat: | Report |
| Gepubliceerd in: |
DCS
2014
|
| _version_ | 1826282403258171392 |
|---|---|
| author | Diciolla, M Kim, C Kwiatkowska, M Mereacre, A |
| author_facet | Diciolla, M Kim, C Kwiatkowska, M Mereacre, A |
| author_sort | Diciolla, M |
| collection | OXFORD |
| description | 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, |
| first_indexed | 2024-03-07T00:43:19Z |
| format | Report |
| id | oxford-uuid:83cd442a-1b9f-493b-a979-a3f21f0233c6 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:43:19Z |
| publishDate | 2014 |
| publisher | DCS |
| record_format | dspace |
| spelling | oxford-uuid:83cd442a-1b9f-493b-a979-a3f21f0233c62022-03-26T21:46:40ZSynthesising Optimal Timing Delays for Timed I/O AutomataReporthttp://purl.org/coar/resource_type/c_93fcuuid:83cd442a-1b9f-493b-a979-a3f21f0233c6Department of Computer ScienceDCS2014Diciolla, MKim, CKwiatkowska, MMereacre, AIn 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, |
| spellingShingle | Diciolla, M Kim, C Kwiatkowska, M Mereacre, A Synthesising Optimal Timing Delays for Timed I/O Automata |
| title | Synthesising Optimal Timing Delays for Timed I/O Automata |
| title_full | Synthesising Optimal Timing Delays for Timed I/O Automata |
| title_fullStr | Synthesising Optimal Timing Delays for Timed I/O Automata |
| title_full_unstemmed | Synthesising Optimal Timing Delays for Timed I/O Automata |
| title_short | Synthesising Optimal Timing Delays for Timed I/O Automata |
| title_sort | synthesising optimal timing delays for timed i o automata |
| work_keys_str_mv | AT diciollam synthesisingoptimaltimingdelaysfortimedioautomata AT kimc synthesisingoptimaltimingdelaysfortimedioautomata AT kwiatkowskam synthesisingoptimaltimingdelaysfortimedioautomata AT mereacrea synthesisingoptimaltimingdelaysfortimedioautomata |