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.
Industrial Usage
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
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!