Accelerating worst case execution time analysis of timed automata models with cyclic behaviour

Verfasser / Beitragende:
[Omar Al-Bataineh, Mark Reynolds, Tim French]
Ort, Verlag, Jahr:
2015
Enthalten in:
Formal Aspects of Computing, 27/5-6(2015-11-01), 917-949
Format:
Artikel (online)
ID: 605516251
LEADER caa a22 4500
001 605516251
003 CHVBK
005 20210128100713.0
007 cr unu---uuuuu
008 210128e20151101xx s 000 0 eng
024 7 0 |a 10.1007/s00165-015-0340-4  |2 doi 
035 |a (NATIONALLICENCE)springer-10.1007/s00165-015-0340-4 
245 0 0 |a Accelerating worst case execution time analysis of timed automata models with cyclic behaviour  |h [Elektronische Daten]  |c [Omar Al-Bataineh, Mark Reynolds, Tim French] 
520 3 |a The paper presents a new efficient algorithm for computing worst case execution time (WCET) of systems modelled as timed automata (TA). The algorithm uses a set of abstraction techniques that improve significantly the efficiency of WCET analysis of TA models with cyclic behaviour. We show that the proposed abstractions are exact with respect to the WCET problem in the sense that the WCET computed in the abstract model is equal to the one computed in the concrete model. We also compare our algorithm with the one implemented in the model checker UPPAAL which shows that when infinite cycles exist (i.e. cycles that can be run infinitely often), UPPAAL's algorithm may not terminate, and when largely repetitive finite cycles exist (i.e. cycles that can be run a large number of times but finite), UPPAAL's algorithm suffers from the state space explosion, thus leading to a low efficiency or resource exhaustion. 
540 |a British Computer Society, 2015 
690 7 |a Worst-case execution time (WCET)  |2 nationallicence 
690 7 |a Timed automata  |2 nationallicence 
690 7 |a Model checking  |2 nationallicence 
690 7 |a Zone abstraction  |2 nationallicence 
700 1 |a Al-Bataineh  |D Omar  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
700 1 |a Reynolds  |D Mark  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
700 1 |a French  |D Tim  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
773 0 |t Formal Aspects of Computing  |d Springer London  |g 27/5-6(2015-11-01), 917-949  |x 0934-5043  |q 27:5-6<917  |1 2015  |2 27  |o 165 
856 4 0 |u https://doi.org/10.1007/s00165-015-0340-4  |q text/html  |z Onlinezugriff via DOI 
898 |a BK010053  |b XK010053  |c XK010000 
900 7 |a Metadata rights reserved  |b Springer special CC-BY-NC licence  |2 nationallicence 
908 |D 1  |a research-article  |2 jats 
949 |B NATIONALLICENCE  |F NATIONALLICENCE  |b NL-springer 
950 |B NATIONALLICENCE  |P 856  |E 40  |u https://doi.org/10.1007/s00165-015-0340-4  |q text/html  |z Onlinezugriff via DOI 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Al-Bataineh  |D Omar  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a Reynolds  |D Mark  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
950 |B NATIONALLICENCE  |P 700  |E 1-  |a French  |D Tim  |u School of Computer Science and Software Engineering, University of Western Australia, Perth, Australia  |4 aut 
950 |B NATIONALLICENCE  |P 773  |E 0-  |t Formal Aspects of Computing  |d Springer London  |g 27/5-6(2015-11-01), 917-949  |x 0934-5043  |q 27:5-6<917  |1 2015  |2 27  |o 165