QUPES: Verification of Quantitative Properties
of Embedded Software
T. Han, J.-P. Katoen, M. Neuhäußer, D. Willems
(funded by the NWO)
The research challenge faced by the QUPES project is to adapt and enrich model checking, a successful technique for checking the logical correctness of system designs, to meet the requirements of state-of-the-art embedded software engineering. Embedded software typically executes on devices that, first and foremost, are not computers. This imposes high requirements on performance and economical resource usage. Due to its embedded nature, its robustness is of prime importance, and timely reactions to stimuli from its—mostly physical—environment are essential. This project proposes to assess these “non-functional” aspects (e.g., timeliness and robustness) as an integral part of the embedded software validation phase. The aim is to obtain a single framework that supports both the validation of qualitative (i.e., functional) as well as quantitative aspects of embedded software.
To accomplish this, model-checking techniques will be extended with ample means to reason about costs (power consumption, memory usage, and the like), efficiency, and robustness. In particular, we aim to develop verification algorithms for real-time systems that exhibit both (continuous-time) randomness as non-determinism and extend this approach with cost aspects. Furthermore, advances to model checking of stochastic systems will be made by developing aggressive abstraction techniques and methods that effectively exploit the (compositional) structure of embedded software specifications for verification purposes. The latter activities are aimed at making stochastic model checking applicable to state spaces that are several orders of magnitude larger than currently can be handled. Our techniques will be tailored to hierarchical design notations (statechart diagrams) for embedded software.
This project takes place in the context of the DFG-NWO bilateral project VOSS2 (Validation of Stochastic Systems). In this project, we cooperate with the Universities of Bonn (Prof. Christel Baier), Saarland (Prof. Holger Hermanns), Nijmegen (Prof. Frits Vaandrager), Twente (Prof. Boudewijn Haverkort), and Federal Armed Forces Munich (Prof. Markus Siegle).
T. Han, J.-P. Katoen, M. Neuhäußer, D. Willems
(funded by the NWO)
The research challenge faced by the QUPES project is to adapt and enrich model checking, a successful technique for checking the logical correctness of system designs, to meet the requirements of state-of-the-art embedded software engineering. Embedded software typically executes on devices that, first and foremost, are not computers. This imposes high requirements on performance and economical resource usage. Due to its embedded nature, its robustness is of prime importance, and timely reactions to stimuli from its—mostly physical—environment are essential. This project proposes to assess these “non-functional” aspects (e.g., timeliness and robustness) as an integral part of the embedded software validation phase. The aim is to obtain a single framework that supports both the validation of qualitative (i.e., functional) as well as quantitative aspects of embedded software.
To accomplish this, model-checking techniques will be extended with ample means to reason about costs (power consumption, memory usage, and the like), efficiency, and robustness. In particular, we aim to develop verification algorithms for real-time systems that exhibit both (continuous-time) randomness as non-determinism and extend this approach with cost aspects. Furthermore, advances to model checking of stochastic systems will be made by developing aggressive abstraction techniques and methods that effectively exploit the (compositional) structure of embedded software specifications for verification purposes. The latter activities are aimed at making stochastic model checking applicable to state spaces that are several orders of magnitude larger than currently can be handled. Our techniques will be tailored to hierarchical design notations (statechart diagrams) for embedded software.
This project takes place in the context of the DFG-NWO bilateral project VOSS2 (Validation of Stochastic Systems). In this project, we cooperate with the Universities of Bonn (Prof. Christel Baier), Saarland (Prof. Holger Hermanns), Nijmegen (Prof. Frits Vaandrager), Twente (Prof. Boudewijn Haverkort), and Federal Armed Forces Munich (Prof. Markus Siegle).