TY - GEN
T1 - Monitoring dynamical signals while testing timed aspects of a system
AU - Frehse, Goran
AU - Larsen, Kim G.
AU - Mikučionis, Marius
AU - Nielsen, Brian
PY - 2011/11/21
Y1 - 2011/11/21
N2 - We propose to combine timed automata and linear hybrid automata model checkers for formal testing and monitoring of embedded systems with a hybrid behavior, i.e., where the correctness of the system depends on discrete as well as continuous dynamics. System level testing is considered, where requirements capture abstract behavior and often include non-determinism due to parallelism, internal counters and subtle state of physical materials. The goal is achieved by integrating the tools Uppaal [2] and PHAVer [3], where the discrete and hard real-time aspects are driven and checked by Uppaal TRON and strict inclusion of dynamical trajectories is verified by PHAVer. We present the framework, the underlying theory, and our techniques for integrating the tools. We demonstrate the applicability on an industrial case study.
AB - We propose to combine timed automata and linear hybrid automata model checkers for formal testing and monitoring of embedded systems with a hybrid behavior, i.e., where the correctness of the system depends on discrete as well as continuous dynamics. System level testing is considered, where requirements capture abstract behavior and often include non-determinism due to parallelism, internal counters and subtle state of physical materials. The goal is achieved by integrating the tools Uppaal [2] and PHAVer [3], where the discrete and hard real-time aspects are driven and checked by Uppaal TRON and strict inclusion of dynamical trajectories is verified by PHAVer. We present the framework, the underlying theory, and our techniques for integrating the tools. We demonstrate the applicability on an industrial case study.
UR - https://www.scopus.com/pages/publications/81255124173
U2 - 10.1007/978-3-642-24580-0_9
DO - 10.1007/978-3-642-24580-0_9
M3 - Conference contribution
AN - SCOPUS:81255124173
SN - 9783642245794
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 115
EP - 130
BT - Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Proceedings
T2 - 23rd IFIP WG 6.1 International Conference on Testing Software and Systems, ICTSS 2011
Y2 - 7 November 2011 through 10 November 2011
ER -