Model Checking Stochastic Systems using Rare Event Simulation (McStores), funded by NWO.
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.
Duration
2009-2013