Quantitative Verification for Software Performance Engineering
Quantitative verification is a mathematically based technique for analysing the correctness, reliability, performance and other quality-of-service properties of systems characterised by stochastic behaviour. This two-lecture course will cover the use of the technique in software performance engineering at design and run time, with an emphasis on advanced topics linked to recent research in the area.
Tuesday 3rd May, 2016 – GSSI – Room B (9.30 – 12.30)
Lecture 1: Introduction to Quantitative Verification for Software Performance Engineering
The first lecture will introduce the main concepts, principles and methods underlying quantitative verification, and will illustrate the use of the technique through short interactive exercises and a case study. The lecture will cover stochastic models including discrete-time and continuous-time Markov chains, the probabilistic temporal logics used to specify key performance and dependability properties that can be analysed using these models, and quantitative verification with the widely used probabilistic model checker PRISM.
Thursday 5th May, 2016 – GSSI – Room B (9.30 – 12.30)
Lecture 2: Recent Advances and Open Research Questions in Quantitative Verification for Software Performance Engineering
The second lecture will explore advanced research topics and will discuss open research questions. The lecture will cover stochastic model synthesis and its use in software design, quantitative verification at runtime and dynamic synthesis of controllers for self-adaptive systems, and stochastic model learning and refinement. Each topic will include a brief description of its motivation and research challenges, an overview of the state of the art that will include the presentation of a recent solution, and a discussion of open research questions aimed at inspiring new work in the area.