DiRePro: Directed Model Checking in the Analysis of Real-Time and Probabilistic Systems

Institutions
  • FB Informatik und Informationswissenschaft
Publications
    Aljazzar, Husain; Leitner-Fischer, Florian; Leue, Stefan; Simeonov, Dimitar(2011): DiPro : A Tool for Probabilistic Counterexample Generation Model Checking Software / Groce, Alex; Musuvathi, Madanlal (Hrsg.). - Berlin, Heidelberg : Springer Berlin Heidelberg, 2011. - (Lecture Notes in Computer Science ; 6823). - S. 183-187. - ISBN 978-3-642-22305-1

DiPro : A Tool for Probabilistic Counterexample Generation

×
The computation of counterexamples for probabilistic model checking has been an area of active research over the past years. In spite of the achieved theoretical results in this field, there is no freely available tool that allows for the computation and representation of probabilistic counterexamples. We present an open source tool called DiPro that can be used with the PRISM and MRMC probabilistic model checkers. It allows for the computation of probabilistic counterexamples for discrete time Markov chains (DTMCs), continuous time Markov chains (CTMCs) and Markov decision processes (MDPs). The computed counterexamples can be rendered graphically.

Origin (projects)

  Haverkort, Boudewijn R.; Kuntz, Matthias; Leitner-Fischer, Florian; Remke, Anne; Roolvink, Stephan(2010): Probabilistic verification of Architectural software models using SoftArc and Prism Reliability, risk and safety : back to the future ; ESREL (European Safety and Reliability) … annual conference ; Island of Rhodes, [5 - 9 September 2010] / Ale, Ben J. M. et al. (Hrsg.). - London : CRC Press, 2010. - S. 852-860. - ISBN 978-0-415-60427-7

Probabilistic verification of Architectural software models using SoftArc and Prism

×
In this paper we will describe the SoftArc approach. With the SoftArc approach it is possible to model and analyse safety-critical embedded and distributed systems that consist of both hard- and software. We are going to present the SoftArc modelling language, its syntax and semantics. The semantics of the SoftArc modelling language is defined in terms of stochastic reactive modules. We will show how important measures of interest for probabilistic dependability analysis like availability, unavailability, and survivability, can be analysed. We will demonstrate the feasibility of our approach by means of two case studies, that involve hard- and software elements. First, we are presenting two industrial case studies from the automotive industry. We will analyse the non volatile random access manager (NVRAM) from the AUTOSAR open system architecture, Second, we are going to present the survivability analysis of a simplified version of the Google replicated file system.

Origin (projects)

    Aljazzar, Husain; Kuntz, Matthias; Leitner-Fischer, Florian; Leue, Stefan(2010): Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation Proceedings of the 2010 ICSE Workshop on Quantitative Stochastic Models in the Verification and Design of Software Systems - QUOVADIS '10. - New York, New York, USA : ACM Press, 2010. - S. 25-32. - ISBN 978-1-60558-972-5

Directed and Heuristic Counterexample Generation for Probabilistic Model Checking - A Comparative Evaluation

×
The generation of counterexamples for probabilistic model checking has been an area of active research over the past five years. Tangible outcome of this research are novel directed and heuristic algorithms for efficient generation of probabilistic counterexamples, such as K* and XBF. In this paper we present an empirical evaluation of the efficiency of these algorithms and the well-known Eppstein's algorithm. We will also evaluate the effect of optimizations applied to Eppstein, K* and XBF. Additionally, we will show, how information produced during model checking can be used to guide the search for counterexamples. This is a first step towards automatically generating heuristic functions. The experimental evaluation of the various algorithms is done by applying them to one case study, known from the literature on probabilistic model checking and one case study taken from the automotive industry.

Origin (projects)

    Aljazzar, Husain; Fischer, Manuel; Grunske, Lars; Kuntz, Matthias; Leitner-Fischer, Florian; Leue, Stefan(2009): Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples 2009 Sixth International Conference on the Quantitative Evaluation of Systems. - IEEE, 2009. - S. 299-308. - ISBN 978-0-7695-3808-2

Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples

×
Failure mode and effects analysis (FMEA) is a technique to reason about possible system hazards that result from system or system component failures. Traditionally, FMEA does not take the probabilities with which these failures may occur into account. Recently, this shortcoming was addressed by integrating stochastic model checking techniques into the FMEA process. A further improvement is the integration of techniques for the generation of counterexamples for stochastic models, which we propose in this paper. Counterexamples facilitate the redesign of a potentially unsafe system by providing information which components contribute most to the failure of the entire system. The usefulness of this novel approach to the FMEA process is illustrated by applying it to the case study of an airbag system provided by our industrial partner, the TRW Automotive GmbH.

Origin (projects)

Funding sources
NameProject no.DescriptionPeriod
Deutsche Forschungsgemeinschaft824/0716.10.2007 – 15.10.2008
Deutsche Forschungsgemeinschaft709/0501.09.2005 – 31.08.2008
Further information
Period: 16.10.2007 – 15.10.2008