The course focuses on quantitative aspects relevant for the evaluation of complex systems, in particular time, resource usage, physical quantities, and probabilities. It introduces quantitative modelling formalisms as well as simulation- and verification-based analysis techniques. Its goal is that, by the end of the course, the student
- understands representative mathematical formalisms for modelling quantitative aspects in the evaluation of complex systems,
- can apply basic algorithms for the analysis of quantitative properties on these formalisms,
- can evaluate the appropriateness and limitations of different analysis techniques given a concrete problem, and make a justified choice,
- can apply modelling languages and analysis tools for quantitative formal models,
- can analyse a system based on a realistic problem description using an appropriate formalism and associated algorithm and/or tool, and
- can create a tool-based solution that combines modelling, implementation of algorithms, and interfacing with existing tools, for a real-life problem involving quantitative aspects.
|
 |
|
The course provides an overview over the kind of formalisms and analysis techniques that are used when quantitative aspects like time, resource usage and probability play a role in the evaluation of complex systems. Students learn how to abstractly model systems, understand the limitations and tradeoffs of established formalisms and techniques, and gain experience with different verification and simulation tools.
As an application example, the course follows a recent line of work on battery-aware task scheduling for resource-constrained nano satellites. The idea is to first pre-compute a cost-optimal schedule using a simpler modelling formalism and to validate its correctness on a more complex model in a second stage.
We introduce all relevant formalisms and techniques to enable the students to reproduce results along these lines and strive for a good mix of theoretical knowledge and hands-on experience using state-of-the-art tools. In the first half of the course, we introduce the theoretical foundations as well as modelling formalisms and analysis tools for variants of hybrid automata (timed automata, priced timed automata and general hybrid automata). This includes all relevant material for the case study, i.e., computing optimal task schedules in a guided assignment.
The second half covers probabilistic models from basic discrete-time Markov chains to probabilistic extensions of the models introduced in the first half. Next to formally covering their syntax and semantics, we will introduce analysis tools to deal with larger model instances.
Prerequisites
- Prior knowledge for the EMSYS master on “Logic reasoning and formal methods” and “Programming languages” as described at https://www.utwente.nl/en/emsys/PriorKnowledge/
- Familiarity with model checking and CTL, e.g., as taught in the System Validation course (192140122)
|
|
|