Statistical Model Checking of Rich Models and Properties

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

149 Downloads (Pure)

Resumé

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.
OriginalsprogEngelsk
Udgivelses stedAalborg
ForlagAalborg Universitetsforlag
Antal sider204
ISBN (Elektronisk)978-87-7112-527-6
DOI
StatusUdgivet - 2015
NavnPh.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet
ISSN2246-1248

Bibliografisk note

Kim Guldstrand Larsen, Hovedvejleder

Citer dette

Poulsen, D. B. (2015). Statistical Model Checking of Rich Models and Properties. Aalborg: Aalborg Universitetsforlag. Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet https://doi.org/10.5278/vbn.phd.engsci.00031
Poulsen, Danny Bøgsted. / Statistical Model Checking of Rich Models and Properties. Aalborg : Aalborg Universitetsforlag, 2015. 204 s. (Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet).
@phdthesis{af78115dc07448bfb52479c190b8c701,
title = "Statistical Model Checking of Rich Models and Properties",
abstract = "Software is in increasing fashion embedded within safety- and business criticalprocesses of society. Errors in these embedded systems can lead to humancasualties or severe monetary loss. Model checking technology has provenformal methods capable of finding and correcting errors in software. However,software is approaching the boundary in terms of the complexity and size thatmodel checking can handle. Furthermore, software systems are nowadays morefrequently interacting with their environment hence accurately modelling suchsystems requires modelling the environment as well - resulting in undecidabilityissues for the traditional model checking approaches.Statistical model checking has proven itself a valuable supplement to modelchecking and this thesis is concerned with extending this software validationtechnique to stochastic hybrid systems. The thesis consists of two parts: the firstpart motivates why existing model checking technology should be supplementedby new techniques. It also contains a brief introduction to probability theoryand concepts covered by the six papers making up the second part. The first twopapers are concerned with developing online monitoring techniques for decidingif a simulation satisfies a property given as a WMTL[a;b] formula. The followingpapers develops a framework allowing dynamical instantiation of processes,in contrast to traditional static encoding of systems. A logic, QDMTL, isdeveloped to express properties of these dynamically evolving systems. Thefifth paper shows how stochastic hybrid automata are useful for modellingbiological systems and the final paper is concerned with showing how statisticalmodel checking is efficiently distributed. In parallel with developing the theorycontained in the papers, a substantial part of this work has been devoted toimplementation in Uppaal SMC.",
author = "Poulsen, {Danny B{\o}gsted}",
note = "Kim Guldstrand Larsen, Hovedvejleder",
year = "2015",
doi = "10.5278/vbn.phd.engsci.00031",
language = "English",
series = "Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet",
publisher = "Aalborg Universitetsforlag",

}

Poulsen, DB 2015, Statistical Model Checking of Rich Models and Properties. Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet, Aalborg Universitetsforlag, Aalborg. https://doi.org/10.5278/vbn.phd.engsci.00031

Statistical Model Checking of Rich Models and Properties. / Poulsen, Danny Bøgsted.

Aalborg : Aalborg Universitetsforlag, 2015. 204 s. (Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet).

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandlingForskning

TY - BOOK

T1 - Statistical Model Checking of Rich Models and Properties

AU - Poulsen, Danny Bøgsted

N1 - Kim Guldstrand Larsen, Hovedvejleder

PY - 2015

Y1 - 2015

N2 - Software is in increasing fashion embedded within safety- and business criticalprocesses of society. Errors in these embedded systems can lead to humancasualties or severe monetary loss. Model checking technology has provenformal methods capable of finding and correcting errors in software. However,software is approaching the boundary in terms of the complexity and size thatmodel checking can handle. Furthermore, software systems are nowadays morefrequently interacting with their environment hence accurately modelling suchsystems requires modelling the environment as well - resulting in undecidabilityissues for the traditional model checking approaches.Statistical model checking has proven itself a valuable supplement to modelchecking and this thesis is concerned with extending this software validationtechnique to stochastic hybrid systems. The thesis consists of two parts: the firstpart motivates why existing model checking technology should be supplementedby new techniques. It also contains a brief introduction to probability theoryand concepts covered by the six papers making up the second part. The first twopapers are concerned with developing online monitoring techniques for decidingif a simulation satisfies a property given as a WMTL[a;b] formula. The followingpapers develops a framework allowing dynamical instantiation of processes,in contrast to traditional static encoding of systems. A logic, QDMTL, isdeveloped to express properties of these dynamically evolving systems. Thefifth paper shows how stochastic hybrid automata are useful for modellingbiological systems and the final paper is concerned with showing how statisticalmodel checking is efficiently distributed. In parallel with developing the theorycontained in the papers, a substantial part of this work has been devoted toimplementation in Uppaal SMC.

AB - Software is in increasing fashion embedded within safety- and business criticalprocesses of society. Errors in these embedded systems can lead to humancasualties or severe monetary loss. Model checking technology has provenformal methods capable of finding and correcting errors in software. However,software is approaching the boundary in terms of the complexity and size thatmodel checking can handle. Furthermore, software systems are nowadays morefrequently interacting with their environment hence accurately modelling suchsystems requires modelling the environment as well - resulting in undecidabilityissues for the traditional model checking approaches.Statistical model checking has proven itself a valuable supplement to modelchecking and this thesis is concerned with extending this software validationtechnique to stochastic hybrid systems. The thesis consists of two parts: the firstpart motivates why existing model checking technology should be supplementedby new techniques. It also contains a brief introduction to probability theoryand concepts covered by the six papers making up the second part. The first twopapers are concerned with developing online monitoring techniques for decidingif a simulation satisfies a property given as a WMTL[a;b] formula. The followingpapers develops a framework allowing dynamical instantiation of processes,in contrast to traditional static encoding of systems. A logic, QDMTL, isdeveloped to express properties of these dynamically evolving systems. Thefifth paper shows how stochastic hybrid automata are useful for modellingbiological systems and the final paper is concerned with showing how statisticalmodel checking is efficiently distributed. In parallel with developing the theorycontained in the papers, a substantial part of this work has been devoted toimplementation in Uppaal SMC.

U2 - 10.5278/vbn.phd.engsci.00031

DO - 10.5278/vbn.phd.engsci.00031

M3 - Ph.D. thesis

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

BT - Statistical Model Checking of Rich Models and Properties

PB - Aalborg Universitetsforlag

CY - Aalborg

ER -

Poulsen DB. Statistical Model Checking of Rich Models and Properties. Aalborg: Aalborg Universitetsforlag, 2015. 204 s. (Ph.d.-serien for Det Teknisk-Naturvidenskabelige Fakultet, Aalborg Universitet). https://doi.org/10.5278/vbn.phd.engsci.00031