Skip to main content

Über dieses Buch

This book constitutes the refereed proceedings of the 4th International Symposium on Model-Based Safety and Assessment, IMBSA 2014, held in Munich, Germany, in October 2014.

The 15 revised full papers presented were carefully reviewed and selected from numerous submissions. The papers are organized in topical sections on modeling paradigms, validation and testing, fault detection and handling, safety assessment in the automotive domain, and case studies.



Modeling Paradigms

A Practicable MBSA Modeling Process Using Altarica

With the increasing system scale and complexity, safety analysis based on formal models has been widely used in the development of aircraft products. However, it’s quite difficult to build a complete, accurate and consistent safety model, especially for dynamic complex systems. To solve these problems, a practical safety modeling methodology based on Altarica, which contains three phases like information collection, model construction and model V&V, is proposed to establish a more structured, systematic and efficiency way in this paper. Detailed processes are declared for each phase. At last, a hydraulic system is taken as an example to show how to apply the safety modeling methodology in practical.
Shaojun Li, Su Duo

On Efficiently Specifying Models for Model Checking

Using formal methods for quality assurance is recommended in many standards for safety critical applications. In most industrial contexts, model checking is the only viable option for formal verification, as interactive approaches often require very highly specialized experts. However, model checking typically suffers from the well-known state-space explosion problem. Due to this problem, engineers typically have to decide on a trade-off between readability and completeness of the model on one side, and the state space size, and thus, computational feasibility on the other. In this paper, we propose a method for reducing the state space by restructuring models. The core idea is to introduce as few additional states as possible by model design making state transitions more complex. To avoid unreadability and infeasible model sizes, we introduce a concept for hierarchical boolean formulas to efficiently specify state transitions. For evaluation purposes, we applied this approach to a case study using the VECS toolkit. In this exemplary case study, we were able to reduce the state space size significantly and make verification time feasible.
Mykhaylo Nykolaychuk, Michael Lipaczewski, Tino Liebusch, Frank Ortmeier

A Model-Based Methodology to Formalize Specifications of Railway Systems

In this article, we propose a modeling methodology for the formalization of the specifications of railway systems. Most of the railway systems are actually still specified in natural language. It results lengthly and ambiguous descriptions, which is obviously a concern regarding safety and security. Hence the current trend to move to the model based approach, i.e. to translate textual specifications into models. To achieve this goal, the choice of a suitable modeling formalism and modeling methodology is of paramount importance. The modeling formalism should be close enough to the practitioners way of thinking so to facilitate the acceptance of the approach. It should be also formal enough to avoid ambiguity. We discuss here these issues based on experiments we made on railway automation solution Trainguard©Mass Transit Communication Based Train Control of Siemens.
Melissa Issad, Leïla Kloul, Antoine Rauzy

Validation and Testing

A Systematic Approach to Requirements Driven Test Generation for Safety Critical Systems

We describe ongoing work into the generation of test cases for safety critical systems using Event-B and the Rodin toolset. Verification of software to DO-178C is a two stage process. First a suite of test cases must be validated against the system requirements (requirements coverage), and then the software implementation is verified using the validated test suite. During verification of the implementation structural coverage is also measured.
Our work focuses on the first step, the generation of test cases and their validation against the requirements. We construct closed-system models incorporating both the system to be tested and its environment. These models capture the system requirements, and describe the interactions between the system and its environment. In particular, safety constraints can be represented by invariants, and their preservation ensured through event guards. From these models test cases can be generated, and requirements coverage can be measured from model coverage.
Toby Wilkinson, Michael Butler, John Colley

Model-Based Safety Approach for Early Validation of Integrated and Modular Avionics Architectures

Increasing complexity of avionics systems leads to reconsider methods that are used today to analyze them from a safety point of view
This paper presents how the Model-based techniques can be used for safety assessment in early validation to support flexible and rapid prototyping of integrated systems (such as Integrated Modular Avionics and Cockpit Display), in order to evaluate and compare several envisaged architectures with their compliance to the safety objectives (under nominal and dispatch conditions).
Marion Morel

Exploring the Impact of Different Cost Heuristics in the Allocation of Safety Integrity Levels

Contemporary safety standards prescribe processes in which system safety requirements, captured early and expressed in the form of Safety Integrity Levels (SILs), are iteratively allocated to architectural elements. Different SILs reflect different requirements stringencies and consequently different development costs. Therefore, the allocation of safety requirements is not a simple problem of applying an allocation "algebra" as treated by most standards; it is a complex optimisation problem, one of finding a strategy that minimises cost whilst meeting safety requirements. One difficulty is the lack of a commonly agreed heuristic for how costs increase between SILs. In this paper, we define this important problem; then we take the example of an automotive system and using an automated approach show that different cost heuristics lead to different optimal SIL allocations. Without automation it would have been impossible to explore the vast space of allocations and to discuss the subtleties involved in this problem.
Luís Silva Azevedo, David Parker, Yiannis Papadopoulos, Martin Walker, Ioannis Sorokos, Rui Esteves Araújo

Fault Detection and Handling

An Integrated Process for FDIR Design in Aerospace

The correct operation of complex critical systems increasingly relies on the ability to detect and recover from faults. The design of Fault Detection, Isolation and Recovery (FDIR) sub-systems is highly challenging, due to the complexity of the underlying system, the number of faults to be considered and their dynamics. Existing industrial practices for FDIR are often based on ad-hoc solutions, that are conceived and developed late in the design process, and do not consider the software- and system-level RAMS analyses data (e.g., FTA and FMEA).
In this paper we propose the FAME process: a novel, model-based, integrated process for FDIR design, that addresses the shortcomings of existing practices. This process aims at enabling a consistent and timely FDIR conception, development, verification and validation. The process is supported by the FAME environment, a model-based toolset that encompasses a wide range of formal analyses, and supports the FDIR design by providing functionality to define mission and FDIR requirements, fault propagation modeling, and automated synthesis of FDIR models. The FAME process and environment have been developed within an ESA-funded study, and have been thoroughly evaluated by the industrial partners on a case study derived from the ExoMars project.
Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Regis De Ferluc, Marco Gario, Andrea Guiotto, Yuri Yushtein

Reliability Analysis of Dynamic Systems by Translating Temporal Fault Trees into Bayesian Networks

Classical combinatorial fault trees can be used to assess combinations of failures but are unable to capture sequences of faults, which are important in complex dynamic systems. A number of proposed techniques extend fault tree analysis for dynamic systems. One of such technique, Pandora, introduces temporal gates to capture the sequencing of events and allows qualitative analysis of temporal fault trees. Pandora can be easily integrated in model-based design and analysis techniques. It is, therefore, useful to explore the possible avenues for quantitative analysis of Pandora temporal fault trees, and we identify Bayesian Networks as a possible framework for such analysis. We describe how Pandora fault trees can be translated to Bayesian Networks for dynamic dependability analysis and demonstrate the process on a simplified fuel system model. The conversion facilitates predictive reliability analysis of Pandora fault trees, but also opens the way for post-hoc diagnostic analysis of failures.
Sohag Kabir, Martin Walker, Yiannis Papadopoulos

metaFMEA-A Framework for Reusable FMEAs

Failure mode and effects analysis (FMEA), is a widely used deductive failure analysis for safety critical systems. Since modern safety critical systems tend to increased complexity, automation and tool support have a long history in research and industry. Whereas compact embedded systems can be analyzed using FMEA in a manually maintained table using for example a spreadsheet application, complex systems easily result in an unmanageable long table especially when larger development teams are involved. During the application of the methodology in industry, two central problems were observed. First, textually described effects are interpreted differently and lead to inconsistencies. Second, one component often is used multiple times in a system, e.g. in electronic circuits where huge circuits are build using a small number of electronic devices. Each implementation of a component results in the same failure modes in a FMEA. Manually inserting them is error prone and adding a new failure mode to an existing component can be very time consuming. Therefore, we describe here a meta model that is capable to solve the aforementioned problems of different inconsistencies and analyze the benefits of this meta model in a tool implementation along with a case study.
Kai Höfig, Marc Zeller, Lars Grunske

Safety Assessment in the Automotive Domain

AltaRica 3 Based Models for ISO 26262 Automotive Safety Mechanisms

Cars embed a steadily increasing number of Electric and Electronic Systems. The ISO 26262 defines a number of constraints, rules and requirements that the development of Automotive E/E Systems must obey in order to guaranty their Functional Safety. One of the means at hand to enhance the safety of these systems is to reinforce them with so-called Safety Mechanisms. The Standard discusses at length how to estimate the contribution of these mechanisms to Functional Safety. These calculations rely however on Fault Tree models or ad-hoc formulas that are hard to check for completeness and validity. In this article, we propose generic AltaRica 3 for Electric and Electronic Systems protected by first and second order safety mechanisms. These models are of a great help to clarify the behavior of these systems as well as to determine the domain of validity of simpler models such the above mentioned Fault Trees or ad-hoc formulas.
Abraham Cherfi, Antoine Rauzy, Michel Leeman

A Pattern-Based Approach towards the Guided Reuse of Safety Mechanisms in the Automotive Domain

The reuse of architectural measures or safety mechanisms is widely-spread in practice, especially in well-understood domains, as is reusing the corresponding safety-case to document the fulfillment of the target safety goal(s). This seems to harmonize well with the fact that safety standards recommend (if not dictate) performing many analyses during the concept phase of development as well as the early adoption of multiple measures at the architectural design level. Yet this front-loading is hindered by the fact that safety argumentation is not well-integrated into architectural models in the automotive domain and as such does not support comprehensible and reproducible argumentation nor any evidence for argument correctness. The reuse is neither systematic nor adequate.
Using a simplified description of safety mechanisms, we defined a pattern library capturing known solution algorithms and architectural measures/constraints in a seamless holistic model-based approach with corresponding tool support. Based on a meta-model encompassing both development artifacts and safety case elements, the pattern library encapsulates all the information necessary for reuse, which can then be integrated into existing development environments. This paper explores the model and the approach using an illustrative implementation example, along with the supporting workflow for the usage of the approach in both “designer” and “user” roles.
Maged Khalil, Alejandro Prieto, Florian Hölzl

Towards the Derivation of Guidelines for the Deployment of Real-Time Tasks on a Multicore Processor

The deployment of automotive software on a multicore processor includes the task of mapping executables to cores. Given the number of possible solutions, integrators have to solve a complex problem. Considering multiple, often conflicting goals like minimizing task response times and memory consumption, complexity further increased with the advent of multicore processors. We present a model-based approach for deriving design rules supporting integrators with statically mapping tasks to a multicore ECU. First, an evolutionary algorithm is used to sample the design space. For each sample, a model-based analysis is performed, resulting in the required fitness values according to the system metric objectives. Finally, subsets of the sample population are used to derive deployment guidelines by evaluating similarities between highly ranked solutions. This reduces the number of solutions to be considered by the integrators by orders of magnitude. In a case-study, we demonstrate the developed approach on an artificial automotive engine management system.
Stefan Schmidhuber, Michael Deubzer, Ralph Mader, Michael Niemetz, Jürgen Mottok

Case Studies

Adaptive Error and Sensor Management for Autonomous Vehicles: Model-Based Approach and Run-Time System

Over the past few years semi-autonomous driving functionality was introduced in the automotive market, and this trend continues towards fully autonomous cars. While in autonomous vehicles data from various types of sensors realize the new highly safety critical autonomous functionality, the already complex system architecture faces the challenge of designing highly reliable and safe autonomous driving system. Since sensors are prone to intermittent faults, using different sensors is better and more cost effective than duplicating the same sensor type because of diversity of reaction of different sensor typesto the same environmental condition. Specifying and validating sensors and providing technical means that enable usage of data from different sensors in case of failures is a challenging, time-consuming and error-prone task for engineers. Therefore, in this paper we present our model-based approach and a run-time system that improves the safety of autonomous driving systems by providing reusable framework managing different sensor setups in a vehicle in a case of a error. Moreover, the solution that we provide enables adaptive graceful degradation and reconfiguration by effective use of the system resources. At the end we explain in an example when and how the approach can be applied.
Jelena Frtunikj, Vladimir Rupanov, Michael Armbruster, Alois Knoll

Safety Assessment of an Electrical System with AltaRica 3.0

This article presents the high level, modeling language AltaRica 3.0 through the safety assessment of an electrical system. It shows how, starting from a purely structural model, several variants can be derived.Two of them target a compilation into Fault Trees and two others target a compilation into Markov chains. Experimental results are reported to show that each of these variants has its own interest. It also advocates that this approach made of successive derivation of variants is a solid ground to build a modeling methodology onto.
Hala Mortada, Tatiana Prosvirnova, Antoine Rauzy

Applying Formal Methods into Safety-Critical Health Applications

Software performs a critical role in almost every aspect of our daily life specially in the embedded systems of medical equipments. A key goal of software engineering is to make it possible for developers to construct systems that operate reliably regardless of their complexity. In this paper, by employing Model-Based Design for large and safety-related applications and applying formal verification techniques, we define specific properties to ensure that a software system satisfies its correctness criteria. We use the formal approach to study and verify the properties of a medical device known as Endotracheal intubation. We present how the system is modeled in the Simulink and Stateflow and present a functionality formalization. In order to formally prove some critical properties, we employ Simulink Design Verifier toolset.
Mohammad-Reza Gholami, Hanifa Boucheneb


Weitere Informationen

Premium Partner