The last few months I had not much time to blog, but today I want to write about a current research project
I’m involved in.
The QuantUM Approach
When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Also, it is necessary that the description methods used do not require a profound knowledge of formal methods. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. All inputs of the analysis are specified at the level of a UML model. This model is then automatically translated into the analysis model, and the results of the analysis are consequently represented on the level of the UML model. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
Our approach depicted in the Figure above can be summarized by identifying the following steps:
- Our UML extension is used to annotate the UML model with all information that is needed to perform a dependability analysis.
- The annotated UML model is then exported in the XML Metadata Interchange (XMI) format which is the standard format for exchanging UML models.
- Subsequently, our QuantUM Tool parses the generated XMI file and generates the analysis model in the input language of the probabilistic model checker PRISM as well the properties to be verified.
- For the analysis we use the probabilistic model checker PRISM together with DiPro in order to compute probabilistic counterexamples representing paths leading to a hazard state.
- The resulting counterexamples can then be transformed into a fault tree that can be interpreted at the level of the UML model. Alternatively, they can be mapped onto a UML sequence diagram which can be displayed in the UML modeling tool containing the original UML model.
Key Features of QuantUM
- QuantUM Profile for UML and SysML
Extension of the UML and SysML with stereotypes. Specification of safety requirements, dependability characteristics (failure modes, …), failure propagation, component dependencies, safety mechanisms (repair management, redundancy structures) directly in the architectural model with your existing UML / SysML CASE tool.
- Probabilistic Analsysis / pFMEA
The annotated UML Model is automatically translated into the input language of a probabilistic model checker, which computes the probability of safety requirements of hazards. In addition a probabilistic FMEA can be performed automatically.
- Automated Fault Tree Generation
(Quantitative) Fault Trees identifying the events causing the violation of a safety requirement or a hazard are automatically generated the analysis.
- Result Representation in UML / SysML
System executions violating safety requirements or causing a hazard can be displayed as UML sequence diagrams.
The QuantUM approach was applied in several industrial case studies and can be used with all major UML / SysML case tools (e.g. IBM Rational Rhapsody, IBM Rational Software Architect, Sparxsystem Enterprise Architect, …)
More Information on the theory and methods behind QuantUM can be found on the publications site. As soon as the first prototype is available
it will be announced here! Stay tuned!
After many months of implementation and testing we finally released the DiPro tool for probabilistic counterexample generation tool.
I will give a talk on DiPro’s features on the SPIN 2011 Workshop (July 14-15), co-located with CAV 2011 in Snowbird Utah.
What is DiPro?
Current stochastic model checkers do not make counterexamples for property violations readily available. DiPro is a tool, that applies directed explicit state space search to discrete- and continuous-time Markov chains in order to compute counterexamples for the violation of PCTL or CSL properties.
Directed explicit state space search algorithms explore the state space on-the-fly which makes DiPro very efficient and highly scalable. They can also be guided using heuristics which usually improve the performance of the method.
Counterexamples provided by DiPro have two important properties. First, they include those traces which contribute the most amount of probability to the property violation. Hence, they show the most probable offending execution scenarios of the system. Second, the obtained counterexamples tend to be small. Hence, they can be effectively analyzed by a human user. Both properties make the counterexamples obtained by our method very useful for debugging purposes.
DiPro allows for the computation of counterexamples for the stochastic model checkers PRISM or MRMC.
Download DiPro here.
My master’s thesis is now available online here.
When developing a safety-critical system it is essential to obtain an assessment of different design alternatives. In particular, an early safety assessment of the architectural design of a system is desirable. In spite of the plethora of available formal quantitative analysis methods it is still difficult for software and system architects to integrate these techniques into their every day work. This is mainly due to the lack of methods that can be directly applied to architecture level models, for instance given as UML diagrams. Another obstacle is, that the methods often require a profound knowledge of formal methods, which can rarely be found in industrial practice. Our approach bridges this gap and improves the integration of quantitative safety analysis methods into the development process. We propose a UML profile that allows for the specification of all inputs needed for the analysis at the level of a UML model. The QuantUM tool which we have developed, automatically translates an UML model into an analysis model. Furthermore, the results gained from the analysis are lifted to the level of the UML specification or other high-level formalism to further facilitate the process. Thus the analysis model and the formal methods used during the analysis are hidden from the user.
Yesterday, on September the first I had my first work day as a PhD student and researcher staff member at the Chair for Software Engineering at the University Konstanz.
My main research topics are the analysis of safety-critical systems, in particular probabilistic and stochastic analysis methods. I will also continue to work on QuantUM tool for quantitative analysis of UML model which I have developed during my master thesis.
Apart from research I will also do some teaching and I will supervise bachelor and master theses.
Since I was a part-time employee of the chair before and worked almost fulltime because I really like my job, there is not much that changes. But it is still yet another station on the road of my live and I look forward to the rest of the journey!
On saturday I will fly to Cape Town, South Africa, to attend the International Conference on Software Engineering. On May 3 I will present our paper “Directed and Heuristic Counterexample Generation for Probabilistic Model Checking – A Comparative Evaluation” at the First International workshop on Quantitative Stochastic Models in the Verification and Design of Software System (QUOVADIS 2010).
I’m really looking forward to the conference where well-known scientists from around the world will present their work. Highlights are also the opening keynote given by Archbishop Desmond Tutu and the Microsoft Research New Horizons Evening.
Our recently published case study “Safety Analysis of an Airbag System using Probabilistic FMEA and Probabilistic Counter Examples” is the cover story over the newest issue of UNIKON the magazine of the University of Konstanz.
Read the Article
The paper “Simulink Design Verifier vs. SPIN – A Comparative Case Study” which was joint work with Stefan Leue and was presented at FMICS 08 is now available online.The paper is more or less a summary of my bachelor thesis.
My bachelor thesis “Evaluation of the Matlab Simulink Design verifier vs. the model checker SPIN” is now available online at http://www.ub.uni-konstanz.de/kops/volltexte/2008/6125/
I recently finished my bachelor thesis and will present a part of it as a short paper at the 13th International Workshop on Formal Methods for Industrial Critical Systems (FMICS) in L’Aquila, Italy.
Simulink Design Verifier vs. SPIN – A Comparative Case Study Florian Leitner and Stefan Leue
State Space Exploration, Matlab Simulink, SPIN, Automotive Software
An increasing number of industrial strength software design tools come along with verification tools that offer some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Verifier and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.