Model Checking Stochastic Systems using Rare Event Simulation

Description of research

In the design of dependable (embedded) computer and communication systems, the use of architecture description languages (ADLs) such as AADL becomes more and more widespread. In order to establish the correct and timely operation of such systems by design, the use of model checking has become more prevalent in recent years. In particular, model checking techniques have been developed to deal with models including time and rewards, so-called Markov reward models, for which the logic CSRL has been developed to express properties. For CSRL model checking, numerical algorithms have been developed, however, the algorithms fall short for realistically sized models, as they arise when using ADLs.

To overcome this, we propose to develop new, efficient rare-event simulation techniques for model checking large Markov-rewards models specified using ADLs. We will develop efficient simulation techniques based on the rare-event simulation technique known as importance sampling, which is particularly powerful in case the probabilities for the events of interest can be considered rare (e.g., when these express undesirable behaviour, like failures). The developed methods, and the corresponding tool support, will allow us to model check such properties, efficiently, and in a statistically sound way, which is crucial for evaluating design alternatives for dependable (embedded) systems.

Advisor(s)

Prof.dr. ir. Boudewijn Haverkort

Prof. dr. Richard J. Boucherie

Dr. ir. Pieter-Tjerk de Boer

Dr. ir. W.R.W. Scheinhardt

Duration

2009-2013

Project

McSTORES

Funding institution

NWO

Strategic Research Orientation

Dependable Systems and Networks

Links to relevant web pages:

http://www.ctit.utwente.nl/research/projects/national/nwo/open/mc-stores.doc/

http://www.nwo.nl/projecten.nsf/pages/2300152130

http://dacs.ewi.utwente.nl

http://www.math.utwente.nl/sor/

Pictures

	CTIT Home > Meet the PhDs > Daniel Reijsbergen
Home CTIT symposium 2013 About CTIT News NIRICT Research Meet the PhDs Working at CTIT Internal Information Conferences Open Calls (updated May 3, 2013) Library and Videos Knowledge Transfer Links Sitemap Search	Model Checking Stochastic Systems using Rare Event Simulation Description of research In the design of dependable (embedded) computer and communication systems, the use of architecture description languages (ADLs) such as AADL becomes more and more widespread. In order to establish the correct and timely operation of such systems by design, the use of model checking has become more prevalent in recent years. In particular, model checking techniques have been developed to deal with models including time and rewards, so-called Markov reward models, for which the logic CSRL has been developed to express properties. For CSRL model checking, numerical algorithms have been developed, however, the algorithms fall short for realistically sized models, as they arise when using ADLs. To overcome this, we propose to develop new, efficient rare-event simulation techniques for model checking large Markov-rewards models specified using ADLs. We will develop efficient simulation techniques based on the rare-event simulation technique known as importance sampling, which is particularly powerful in case the probabilities for the events of interest can be considered rare (e.g., when these express undesirable behaviour, like failures). The developed methods, and the corresponding tool support, will allow us to model check such properties, efficiently, and in a statistically sound way, which is crucial for evaluating design alternatives for dependable (embedded) systems. Advisor(s) Prof.dr. ir. Boudewijn Haverkort Prof. dr. Richard J. Boucherie Dr. ir. Pieter-Tjerk de Boer Dr. ir. W.R.W. Scheinhardt Duration 2009-2013 Project McSTORES Funding institution NWO Strategic Research Orientation Dependable Systems and Networks Links to relevant web pages: http://www.ctit.utwente.nl/research/projects/national/nwo/open/mc-stores.doc/ http://www.nwo.nl/projecten.nsf/pages/2300152130 http://dacs.ewi.utwente.nl http://www.math.utwente.nl/sor/ Pictures