Danny Bøgsted Poulsen will defend his thesis:
"Statistical Model Checking of Rich Models and Properties"
The defence takes place on Tuesday 23rd of February 2016, 13:00, in room 0.2.13 at Selma Lagerlöfs Vej 300
Software is in increasing fashion embedded within safety- and business critical processes of society. Errors in these embedded systems can lead to human casualties or severe monetary loss.
Model checking technology has proven formal methods capable of finding and correcting errors in software. However, software is approaching the boundary in terms of the complexity and size that model checking can handle. Furthermore, software systems are nowadays more frequently interacting with their environment hence accurately modelling such systems requires modelling theenvironment as well - resulting in undecidability issues for the traditional model checking approaches. Statistical model checking has proven itself a valuable supplement to model checking and this thesis is concerned with extending this software validation technique to stochastic hybrid systems.
The thesis consists of two parts: the first part motivates why existing model checking technology should be supplemented by new techniques. It also contains a brief introduction to probability theory and concepts covered by the six papers making up the second part. The first two papers are concerned with developing online monitoring techniques for deciding if a simulation satisfies a property given as a WMITL ormula. The following papers develops a framework allowing dynamical instantiation of processes, in contrast to traditional static encoding of systems. A logic, QDMTL, is developed to express properties of these dynamically evolving systems. The fifth paper shows how stochastic hybrid automata are useful for modelling biological systems and the final paper is concerned with showing how statistical model checking is efficiently distributed. In parallel with developing the theory contained in the papers, a substantial part of this work has been devoted to implementation in Uppaal SMC.
Members of the assessment committee
Professor Martin Fränzle, Oldenburg University, Professor Wang Yi, Uppsala University and Associate Professor René Rydhof Hansen, Aalborg University. Professor Kim Guldstrand Larsen is Danny Bøgsted Poulsens supervisor. Moderator Associate Professor Lone Leth Thomsen.
All interested parties are welcome. After the defense the department will be hosting a small reception in cluster 1.