Danny Bøgsted Poulsen

Danny Bøgsted Poulsen

Postdoctoral Researcher

Personal Profile

I am a post-doctoral researcher working at Christian Albrechts University zu Kiel under the supervision of Professor Dirk Nowotka. I received my PhD from Aalborg university where I was involved in the integration of Statistical Model Checking into Uppaal. This was under the supervision of Kim Guldstrand Larsen and Alexandre David

Publications

Importance Sampling for Stochastic Timed Automata

SETTA - 2016, Cyrille Jegourel, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Sean Sedwards

Modelling Attack-defense Trees Using Timed Automata

FORMATS - 2016, Olga Gadyatskaya, René Rydhof Hansen, Kim Guldstrand Larsen, Axel Legay, Mads Chr. Olesen, Danny Bøgsted Poulsen

Statistical model checking for biological systems

STTT - 2015, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Sean Sedwards:

Uppaal SMC tutorial.

STTT - 2015, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen

Quantified Dynamic Metric Temporal Logic for Dynamic Networks of Stochastic Hybrid Automata.

ACSD - 2014,Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen

Statistical Model Checking of Dynamic Networks of Stochastic Hybrid Automata.

AVOCS - 2013, Alexandre David, Kim G. Larsen, Axel Legay, Danny Bøgsted Poulsen

Runtime Verification of Biological Systems.

ISOLA - 2012, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Sean Sedwards

Monitor-Based Statistical Model Checking for Weighted Metric Temporal Logic.

LPAR - 2012, Peter E. Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen, Amélie Stainer

Checking and Distributing Statistical Model Checking.

NFM - 2012, Peter E. Bulychev, Alexandre David, Kim Guldstrand Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen

Rewrite-Based Statistical Model Checking of WMTL.

RV - 2012, Peter E. Bulychev, Alexandre David, Kim G. Larsen, Axel Legay, Guangyuan Li, Danny Bøgsted Poulsen

UPPAAL-SMC: Statistical Model Checking for Priced Timed Automata.

QAPL - 2012, Peter E. Bulychev, Alexandre David, Kim Guldstrand Larsen, Marius Mikucionis, Danny Bøgsted Poulsen, Axel Legay, Zheng Wang

Statistical Model Checking for Stochastic Hybrid Systems

HSB - 2012, Alexandre David, Dehui Du, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Sean Sedwards:

Statistical Model Checking for Networks of Priced Timed Automata

FORMATS - 2011, Alexandre David, Kim G. Larsen, Axel Legay, Marius Mikucionis, Danny Bøgsted Poulsen, Jonas van Vliet, Zheng Wang

Education

PhD, Computer Science

Statistical Model Checking of Rich Systems and Properties

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 the environment 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 WMTL formula. 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.

Master, Computer Science

Concrete Delays for Symbolic Executions