Software controls cars, planes, medical equipment, nuclear power plants and many other safety-critical embedded and cyber-physical systems. The malfunctioning of those systems can harm people physically, threaten the environment or cause significant financial losses. When developing such safety-critical systems it is essential to evaluate different design alternatives. Especially in the early design stages a safety assessment of the architectural design is desirable. Manual safety analysis methods (Fault Tree Analysis, FMEA) required by applicable safety standards and industrial best practices are costly and unreliable. 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. At the same time, model–based systems engineering based on UML /SysML architecture models and related design tools (IBM Rhapsody, Enterprise Architect, Artisan Studio, etc.) is an increasingly popular system design approach.
The manufacturers of safety-critical systems and their suppliers need software tools that support automated safety analysis of their system models in order to follow best practices and applicable standards in a cost-effective manner. QuantUM is a tool environment that offers automated model-based functional safety analysis (Fault Tree Analysis, FMEA). It can directly process architecture models edited by the mentioned software design tools. The engineer or developer does not have to be schooled in the use of formal verification methods or tools, yet can use the benefits due to the automatic translation and verification that is done by QuantUM. Results can then be presented in different formats like UML Sequence Diagrams or Fault Trees.
Compatible with international safety standards and best practices in many domains (automotive, avionic, medical equipment, etc.)
Tight integration into system engineering development processes.
Our approach depicted in the Figure above can be summarized by identifying the following steps:
- A UML / SysML Model is created in the usual engineering process.
- Our UML / SysML extension, in the form of stereotypes, is used to annotate the UML / SysML model with all information that is needed to perform a safety analysis directly in the editor normally used in the engineering process. This information includes the specification of (safety-) requirements and failure mode specifications.
- The annotated UML / SysML model is then exported in the XML Metadata Interchange (XMI) format which is the standard format for exchanging UML / SysML models.
- Subsequently, our QuantUM Tool parses the generated XMI file and generates an analysis model in the input languages for several state of the art model checkers.
- For the analysis we use the probabilistic model checker PRISM and the explicit state model checker Spin 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 / SysML model. Alternatively, they can be mapped onto a UML / SysML sequence diagram which can be displayed in the UML / SysML modeling tool containing the original UML / SysML 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 / SysML 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 by the analysis.
Result Representation in UML / SysML
System executions violating safety requirements or causing a hazard can be displayed as UML / SysML 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, …).
Selected Publications are listed below. The full set of publications can be found in list of publications.
- Florian Leitner-Fischer: Causality Checking of Safety-Critical Software and Systems. Doctoral Dissertation, University of Konstanz, 2015.
Download: [PDF] [Bibtex]
- Florian Leitner-Fischer and Stefan Leue : SpinCause: A Tool for Causality Checking. Proceedings of the International SPIN Symposium on Model Checking of Software (SPIN 2014), San Jose, CA, USA. (2014).
Download: [pdf] [BibTex] [www]
- Florian Leitner-Fischer and Stefan Leue: Probabilistic Fault Tree Synthesis using Causality Computation, International Journal of Critical Computer-Based Systems, Vol. 4, No. 2, pp.119–143, 2013.
- F. Leitner-Fischer and S.Leue : Causality Checking for Complex System Models, In Proceedings of 14th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI2013),pp. 248-267, Lecture Notes in Computer Science, Volume 7737. Springer Verlag., 2013. http://se.uni-konstanz.de/#
- Adrian Beer: Quantitative Analysis of Concurrent System Architectures, Master Thesis, University of Konstanz, 2012.http://se.uni-konstanz.de/#
- Adrian Beer, Uwe Kühne, Florian Leitner-Fischer, Stefan Leue and Rüdiger Prem: Analysis of an Airport Surveillance Radar using the QuantUM approach, Technical Report soft-12-01, Chair for Software Engineering, University of Konstanz. 2012.
- Matthias Kuntz, Florian Leitner-Fischer and Stefan Leue: From Probabilistic Counterexamples via Causality to Fault Trees, In Proceedings of 30th International Conference on Computer Safety, Reliability and Security (SAFECOMP 2011), 2011.
- Florian Leitner-Fischer: Quantitative Safety Analysis of UML Models. Master Thesis, University of Konstanz, 2010.
If you need additional information or want to evaluate QuantUM, please feel free to contact Stefan Leue.