## Abstrakt

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[a;b] 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.

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[a;b] 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.

Originalsprog | Engelsk |
---|

Udgivelsessted | Aalborg |
---|---|

Forlag | Aalborg Universitetsforlag |

Antal sider | 204 |

ISBN (Elektronisk) | 978-87-7112-527-6 |

DOI | |

Status | Udgivet - 2015 |

Navn | Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet |
---|---|

ISSN | 2246-1248 |