Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben

2013 | Buch

Logic and Epistemology in Safety Cases Kapitel lesen Erstes Kapitel lesen

Computer Safety, Reliability, and Security

32nd International Conference, SAFECOMP 2013, Toulouse, France, September 24-27, 2013. Proceedings

herausgegeben von: Friedemann Bitsch, Jérémie Guiochet, Mohamed Kaâniche

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 32nd International Conference on Computer Safety, Reliability, and Security, SAFECOMP 2013, held in Toulouse, France, in September 2013.

The 20 revised full papers presented together with 5 practical experience reports were carefully reviewed and selected from more than 88 submissions. The papers are organized in topical sections on safety requirements and assurance, testing and verification, security, software reliability assessment, practical experience reports and tools, safety assurance in automotive, error control codes, dependable user interfaces, and hazard and failure mode analysis.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Logic and Epistemology in Safety Cases
Abstract
A safety case must resolve concerns of two different kinds: how complete and accurate is our knowledge about aspects of the system (e.g., its requirements, environment, implementation, hazards) and how accurate is our reasoning about the design of the system, given our knowledge.
The first of these is a form of epistemology and requires human experience and insight, but the second can, in principle, be reduced to logic and then checked and automated using the technology of formal methods.
We propose that reducing epistemic doubt is the main challenge in safety cases, and discuss ways in which this might be achieved.
John Rushby

Safety Requirements and Assurance

Comparative Conformance Cases for Monitoring Multiple Implementations of Critical Requirements
Abstract
The paper presents the concept and the mechanism of comparative conformance cases which support conformance monitoring in situations where a standard or other set of requirements are being implemented at multiple sites. The mechanism is enabled by NOR-STA services which implement the TRUST-IT methodology and are deployed in the cloud in accordance with the SaaS model. In the paper we introduce the concept of comparative conformance cases, explain the software services used to implement them and present a case study of monitoring the implementation of the EC Regulation No. 994/2010, related to risk management of gas supply infrastructures across Europe.
Janusz Górski, Aleksander Jarzębowicz, Jakub Miler
A Formal Basis for Safety Case Patterns
Abstract
By capturing common structures of successful arguments, safety case patterns provide an approach for reusing strategies for reasoning about safety. In the current state of the practice, patterns exist as descriptive specifications with informal semantics, which not only offer little opportunity for more sophisticated usage such as automated instantiation, composition and manipulation, but also impede standardization efforts and tool interoperability. To address these concerns, this paper gives (i) a formal definition for safety case patterns, clarifying both restrictions on the usage of multiplicity and well-founded recursion in structural abstraction, (ii) formal semantics to patterns, and (iii) a generic data model and algorithm for pattern instantiation. We illustrate our contributions by application to a new pattern, the requirements breakdown pattern, which builds upon our previous work.
Ewen Denney, Ganesh Pai

Testing and Verification

Testing Autonomous Robot Control Software Using Procedural Content Generation
Abstract
We present a novel approach for reducing manual effort when testing autonomous robot control algorithms. We use procedural content generation, as developed for the film and video game industries, to create a diverse range of test situations. We execute these in the Player/Stage robot simulator and automatically rate them for their safety significance using an event-based scoring system. Situations exhibiting dangerous behaviour will score highly, and are thus flagged for the attention of a safety engineer. This process removes the time-consuming tasks of hand-crafting and monitoring situations while testing an autonomous robot control algorithm. We present a case study of the proposed approach – we generated 500 randomised situations, and our prototype tool simulated and rated them. We have analysed the three highest rated situations in depth, and this analysis revealed weaknesses in the smoothed nearness-diagram control algorithm.
James Arnold, Rob Alexander
Fine-Grained Implementation of Fault Tolerance Mechanisms with AOP: To What Extent?
Abstract
The benefits of using aspect oriented programming (AOP) for separation of concerns is well-known and has been demonstrated in many works, including for dependable computing. In this paper, we use this composition capability of AOP to develop micro-aspects that can be combined together to realize a given fault tolerance mechanism. The toolbox of micro-aspects can be used to make mechanisms easily configurable and by the way to simplify their update. We show that the composition of micro aspects leads to undesirable side effects of the interactions between them, called interferences. We propose an approach to detect interferences with executable assertions, using an extension of AspectJ called AIRIA that enables control over an aspect chain at a shared join point. We finally draw the lessons learnt and discuss to what extent AOP can be used to develop fault tolerance mechanisms.
Jimmy Lauret, Jean-Charles Fabre, Hélène Waeselynck
Formalisation of an Industrial Approach to Monitoring Critical Data
Abstract
A large class of safety-critical control systems contains monitoring subsystems that display certain system parameters to (human) operators. Ensuring that the displayed data are sufficiently fresh and non-corrupted constitutes an important part of safety requirements. However, the monitoring subsystems are typically not a part of a safety kernel and hence often built of SIL1–SIL2 components. In this paper, we formalise a recently implemented industrial approach to architecting dependable monitoring systems, which ensures data freshness and integrity despite unreliability of their components. Moreover, we derive an architectural pattern that allows us to formally reason about data freshness and integrity. The proposed approach is illustrated by an industrial case study.
Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis, Dubravka Ilić, Timo Latvala

Security

Protecting Vehicles Against Unauthorised Diagnostics Sessions Using Trusted Third Parties
Abstract
Wireless vehicle diagnostics is expected to provide great improvements to the maintenance of future cars. By using certificates, vehicles can identify diagnostics equipment for a diagnostics session, even over long distances. However, since the diagnostics equipment contains authentication keys used to authenticate such sessions, it is critical that neither the keys nor the equipment is lost. Such a loss can give unauthorised access to any vehicle accepting these keys until the theft is detected and the certificates are revoked. In this paper, we propose a method to protect vehicles against unauthorised diagnostics sessions. A trusted third party is introduced to authorise sessions, thus we do not rely solely on proper identification and authentication of diagnostics equipment. Our approach enables vehicles to verify the validity of diagnostics requests. It is transparent to the diagnostics protocol being used, supports different levels of trust, and can control what commands are permitted during diagnostics sessions.
Pierre Kleberger, Tomas Olovsson
Vulnerability Analysis on Smart Cards Using Fault Tree
Abstract
In smart card domain, attacks and countermeasures are advancing at a fast rate. In order to have a generic view of all the attacks, we propose to use a Fault Tree Analysis. This method used in safety analysis helps to understand and implement all the desirable and undesirable events existing in this domain. We apply this method to Java Card vulnerability analysis. We define the properties that must be ensured: integrity and confidentiality of smart card data and code. By modeling the conditions, we discovered new attack paths to get access to the smart card contents. Then we introduce a new security api which is proposed to mitigate the undesirable events defined in the tree models.
Guillaume Bouffard, Bhagyalekshmy N. Thampi, Jean-Louis Lanet
Does Malware Detection Improve with Diverse AntiVirus Products? An Empirical Study
Abstract
We present results of an empirical study to evaluate the detection capability of diverse AntiVirus products (AVs). We used malware samples collected in a geographically distributed honeypot deployment in several different countries and organizations. The malware was collected in August 2012: the results are relevant to recent and current threats observed in the Internet. We sent these malware to 42 AVs available from the VirusTotal service to evaluate the benefits in detection from using more than one AV. We then compare these findings with similar ones performed in the past to evaluate effectiveness of diversity with AVs. In general we found that the new findings are consistent with previous ones, despite some differences. This study provides additional evidence that detection capabilities are improved by diversity with AVs.
Ilir Gashi, Bertrand Sobesto, Vladimir Stankovic, Michel Cukier

Software Reliability Assessment

Software Fault-Freeness and Reliability Predictions
Abstract
Many software development practices aim at ensuring that software is correct, or fault-free. In safety critical applications, requirements are in terms of probabilities of certain behaviours, e.g. as associated to the Safety Integrity Levels of IEC 61508. The two forms of reasoning – about evidence of correctness and about probabilities of certain failures – are rarely brought together explicitly. The desirability of using claims of correctness has been argued by many authors, but not been taken up in practice. We address how to combine evidence concerning probability of failure together with evidence pertaining to likelihood of fault-freeness, in a Bayesian framework. We present novel results to make this approach practical, by guaranteeing reliability predictions that are conservative (err on the side of pessimism), despite the difficulty of stating prior probability distributions for reliability parameters. This approach seems suitable for practical application to assessment of certain classes of safety critical systems.
Lorenzo Strigini, Andrey Povyakalo
Does Software Have to Be Ultra Reliable in Safety Critical Systems?
Abstract
It is difficult to demonstrate that safety-critical software is completely free of dangerous faults. Prior testing can be used to demonstrate that the unsafe failure rate is below some bound, but in practice, the bound is not low enough to demonstrate the level of safety performance required for critical software-based systems like avionics. This paper argues higher levels of safety performance can be claimed by taking account of: 1) external mitigation to prevent an accident: 2) the fact that software is corrected once failures are detected in operation. A model based on these concepts is developed to derive an upper bound on the number of expected failures and accidents under different assumptions about fault fixing, diagnosis, repair and accident mitigation. A numerical example is used to illustrate the approach. The implications and potential applications of the theory are discussed.
Peter Bishop

Practical Experience Reports and Tools I

The SafeCap Platform for Modelling Railway Safety and Capacity
Abstract
This paper describes a tooling platform that supports reasoning about railway capacity while ensuring system safety. It uses a Domain Specific Language (DSL) that allows signalling engineers to design stations and junctions, to check their safety and to evaluate the potential improvements of capacity while applying various alteration patterns that change the railway schemas. The platform uses a combination of model checking and SMT solving to verify system safety in the most efficient and user-friendly way. It includes several plug-ins that evaluate various capacity parameters. The tool uses the Eclipse technology, including its EMF and GMF frameworks. It has been developed in close cooperation with the Invensys Rail engineers and applied in a variety of mediumscale projects, which has demonstrated its ability to help understand the effects that changes in the plans and schemas can potentially have on capacity.
Alexei Iliasov, Ilya Lopatkin, Alexander Romanovsky
Embedded System Platform for Safety-Critical Road Traffic Signal Applications
Abstract
Road traffic signals are used to signal information to drivers (e.g., red signal to stop). A controller residing in a local cabinet is managing the traffic signal. Depending on the desired traffic situation, the corresponding traffic signal is switched on or off via the power line. For the time being, there is no programmable logic included in each traffic signal. As a result, there is a single type for each application available e.g., due to different power supply levels or light output. In addition, functionality of traffic signals is limited so that its status information cannot be retrieved.
This paper presents an approach to traffic signals for safety-critical applications based on an embedded system. It includes a presentation of safetyrelated hardware and a microcontroller with embedded safety-related firmware. The result is a platform to be used in various applications and meeting safety and performance requirements according to standard EN 50556 and VDE 0832.
Thomas Novak, Christoph Stoegerer
Low-Level Attacks on Avionics Embedded Systems
Abstract
Improving the security of computing systems embedded into commercial airplanes has become a major concern for the avionics industry. This paper deals with one of the techniques that can be applied to improve the security of such systems: vulnerability assessment. More precisely, this paper presents experiments carried out on an experimental embedded operating system in order to assess vulnerabilities in its low-level implementation layers. The main characteristics of this embedded system, the platform used to carry out our experiments, as well as the first results of these experiments are described.
Anthony Dessiatnikoff, Eric Alata, Yves Deswarte, Vincent Nicomette

Safety Assurance in Automotive

Safety Cases and Their Role in ISO 26262 Functional Safety Assessment
Abstract
Compliance with the automotive standard ISO 26262 requires the development of a safety case for electrical and/or electronic (E/E) systems whose malfunction has the potential to lead to an unreasonable level of risk. In order to justify freedom from unreasonable risk, a safety argument should be developed in which the safety requirements are shown to be complete and satisfied by the evidence generated from the ISO 26262 work products. However, the standard does not provide practical guidelines for how it should be developed and reviewed. More importantly, the standard does not describe how the safety argument should be evaluated in the functional safety assessment process. In this paper, we categorise and analyse the main argument structures required of a safety case and specify the relationships that exist between these structures. Particular emphasis is placed on the importance of the product-based safety rationale within the argument and the role this rationale should play in assessing functional safety. The approach is evaluated in an industrial case study. The paper concludes with a discussion of the potential benefits and challenges of structured safety arguments for evaluating the rationale, assumptions and evidence put forward when claiming compliance with ISO 26262.
John Birch, Roger Rivett, Ibrahim Habli, Ben Bradshaw, John Botham, Dave Higham, Peter Jesty, Helen Monkhouse, Robert Palin
Structuring Safety Requirements in ISO 26262 Using Contract Theory
Abstract
ISO 26262 - ”Road vehicles-Functional Safety” is a standard for the automotive industry, administered in an attempt to prevent potential accidents due to systematic and random failures in the Electrical/Electronic-system. ISO 26262 is based on the principle of relying on safety requirements as the main source of information to enforce correctness of design. We show that the contract theory from the SPEEDS FP6 project provides a suitable foundation to structure safety requirements in ISO 26262. Contracts provide the necessary support to separate the responsibilities between a system and its environment by explicitly imposing requirements on the environment as assumptions, in order to guarantee the safety requirements. We show this by characterizing two levels of safety requirements with contracts for an industrial system where we also show how contract theory supports the verification of consistency and completeness of safety requirements.
Jonas Westman, Mattias Nyberg, Martin Törngren

Error Control Codes

Flexible Unequal Error Control Codes with Selectable Error Detection and Correction Levels
Abstract
Unequal Error Control (UEC) codes provide means for handling errors where the codeword digits may be exposed to different error rates, like in two-dimensional optical storage media, or VLSI circuits affected by intermittent faults or different noise sources. However, existing UEC codes are quite rigid in their definition. They split codewords in only two areas, applying different (but limited) error correction functions in each area. This paper introduces Flexible UEC (FUEC) codes, which can divide codewords into any required number of areas, establishing for each one the adequate error detection and/or correction levels. At design time, an algorithm automates the code generation process. Among all the codes meeting the requirements, different selection criteria can be applied. The code generated is implemented using simple logic operations, allowing fast encoding and decoding. Reported examples show their feasibility and potentials.
Luis-J. Saiz-Adalid, Pedro-J. Gil-Vicente, Juan-Carlos Ruiz-García, Daniel Gil-Tomás, J. -Carlos Baraza, Joaquín Gracia-Morán
Safety Transformations: Sound and Complete?
Abstract
Safety transformations transform unsafe original software into safe software that, in contrast to the unsafe version, detects if its execution was incorrect due to execution errors. Especially transformations based on arithmetic codes such as an AN- or ANB-code apply complex and error-prone transformations, while at the same time aiming for safety- or mission-critical applications. Testing and error injection are used so far to ensure correctness and error detection capabilities. But both are incomplete and might miss errors that change functionality or reduce error detection rates. Our research provides tools for a complete analysis of AN-encoding safety transformations. This paper presents our analysis tools and results for the AN-encoded operations. While we were able to demonstrate functional correctness, we discovered bugs that prevent propagation of errors almost completely for AN-encoded divisions and reduce propagation significantly for logical bitwise operations.
Ute Schiffel

Invited Paper

It Is (Almost) All about Human Safety: A Novel Paradigm for Robot Design, Control, and Planning
Abstract
In this paper we review our work on safe control, acting, and planning in human environments. In order for a robot to be able to safely interact with its environment it is necessary to be able to react to unforeseen events in real-time on basically all levels of abstraction. Having this goal in mind, our contributions reach from fundamental understanding of human injury due to robot-human collisions as the underlying metric for “safe” behavior, various interaction control schemes that ground on the basic components impedance control and collision behavior, to safe real-time motion planning and behavior based control as an interface level for task planning. Based on this foundation, we also developed joint interaction planners for role allocation in human-robot collaborative assembly, as well as reactive safety oriented replanning algorithms. A very recent step was the development of novel programming paradigms that act as a simple yet powerful interface between programmer, automatic planning, and the robot. A significant amount of our work on robot safety and control has found found its way into international standardization committees, products, and was applied in numerous real-world applications.
Sami Haddadin, Sven Parusel, Rico Belder, Alin Albu-Schäffer

Dependable User Interfaces

Understanding Functional Resonance through a Federation of Models: Preliminary Findings of an Avionics Case Study
Abstract
FRAM has been proposed as a method for the analysis of complex socio-technical systems, which may be able to overcome the limitations of traditional methods that focus on simple cause and effect relationships. FRAM on its own may be most useful for modeling the system at a high level of abstraction. There is less evidence about its utility for modeling interactions at greater levels of detail. We applied different modeling approaches to investigate situations that may give rise to functional resonance in an avionics case study. FRAM was used to model higher-level dependencies, HAMSTERS was used to provide a deeper understanding of human functions, and ICO-Petshop was used to model technical system functions. The paper describes preliminary results of the application of this federation of models, and highlights potential benefits as well as challenges that may have to be overcome.
Célia Martinie, Philippe Palanque, Martina Ragosta, Mark Alexander Sujan, David Navarre, Alberto Pasquini
Model-Based Development of the Generic PCA Infusion Pump User Interface Prototype in PVS
Abstract
A realistic user interface is rigorously developed for the US Food and Drug Administration (FDA) Generic Patient Controlled Analgesia (GPCA) pump prototype. The GPCA pump prototype is intended as a realistic workbench for trialling development methods and techniques for improving the safety of such devices. A model-based approach based on the use of formal methods is illustrated and implemented within the Prototype Verification System (PVS) verification system. The user interface behaviour is formally specified as an executable PVS model. The specification is verified with the PVS theorem prover against relevant safety requirements provided by the FDA for the GPCA pump. The same specification is automatically translated into executable code through the PVS code generator, and hence a high fidelity prototype is then developed that incorporates the generated executable code.
Paolo Masci, Anaheed Ayoub, Paul Curzon, Insup Lee, Oleg Sokolsky, Harold Thimbleby

Practical Experience Reports and Tools II

Characterization of Failure Effects on AADL Models
Abstract
Prior works on model-based Failure Modes and Effects Analysis (FMEA) automatically generate a FMEA table given the system model, a set of failure modes, and a set of possible effects. The last requirement is critical as bias may occur: since the considered failure effects are restricted to the anticipated ones, unexpected effects - the most interesting ones - are disregarded in the FMEA.
In this paper, we propose and investigate formal concepts that aim to overcome this bias. They support the construction of FMEA tables solely based on the system model and the failure modes, i.e., without requiring the set of effects as input. More concretely, given a system specification in the Architecture Analysis and Design Language (AADL), we show how to derive relations that characterize the effects of failures based on the state transition system of that specification. We also demonstrate the benefits and limitations of these concepts on a satellite case study.
Bernhard Ern, Viet Yen Nguyen, Thomas Noll
Derived Hazard Analysis Method for Critical Infrastructures
Abstract
Within the Austrian national security research programme KIRAS, a study on security against electromagnetic threats was conducted. Apart from a survey on existing literature about respective events and analyses on existing threats and possible protection measures, a novel risk analysis method was developed, based on a qualitative FMEA (Failure modes and effects analysis). The traditional FMEA sheet was split into several tables taking advantage from the limited set of electromagnetic interference causes and a general set of high-level consequences. The resulting tables of risk priority numbers allowed a good overview on which defence and which protection measures should be prioritized. Finally, the method was validated based on three scenarios of road vehicle convoys with respect to its applicability. This paper describes the approach developed for the modified FMEA method and its application to three vehicle convoy scenarios, discussing the value of the method and interpreting the results of the validation.
Thomas Gruber, Georg Neubauer, Andreas Weinfurter, Petr Böhm, Kurt Lamedschwandner
A Study of the Impact of Single Bit-Flip and Double Bit-Flip Errors on Program Execution
Abstract
This paper presents the results of an extensive experimental study of bit-flip errors in instruction set architecture registers and main memory locations. Comprising more than two million fault injection experiments conducted with thirteen benchmark programs, the study provides insights on whether it is necessary to consider double bit-flip errors in dependability benchmarking experiments. The results show that the proportion of silent data corruptions in the program output, is almost the same for single and double bit errors. In addition, we present detailed statistics about the error sensitivity of different target registers and memory locations, including bit positions within registers and memory words. These show that the error sensitivity varies significantly between different bit positions and registers. An important observation is that injections in certain bit positions always have the same impact regardless of when the error is injected.
Fatemeh Ayatolahi, Behrooz Sangchoolie, Roger Johansson, Johan Karlsson

Hazard and Failure Mode Analysis

OpenMADS: An Open Source Tool for Modeling and Analysis of Distributed Systems
Abstract
In this paper, we present OpenMADS, an open source tool for modeling and analysis of distributed systems. OpenMADS generates comprehensive availability models by using the input of SysML specifications and MARTE annotations, which are automatically translated into deterministic and stochastic Petri nets. The integrated use of analytic models (e.g., Petri Nets or Markov chains) with semi-formal modeling languages, like SysML or UML, can provide important insights to the designers regarding different distributed infrastructures, and consequently, allows them to choose the infrastructure that fits the company budget or satisfies a given service level agreement. To show the applicability of OpenMADS, we demonstrate the process of availability modeling and evaluation based on the example of a Web server system.
Ermeson C. Andrade, Marcelo Alves, Rubens Matos, Bruno Silva, Paulo Maciel
A Controlled Experiment on Component Fault Trees
Abstract
In safety analysis for safety-critical embedded systems, methods such as FMEA and fault trees (FT) are strongly established in practice. However, the current shift towards model-based development has resulted in various new safety analysis methods, such as Component Integrated Fault Trees (CFT). Industry demands to know the benefits of these new methods. To compare CFT to FT, we conducted a controlled experiment in which 18 participants from industry and academia had to apply each method to safety modeling tasks from the avionics domain. Although the analysis of the solutions showed that the use of CFT did not yield a significantly different number of correct or incorrect solutions, the participants subjectively rated the modeling capacities of CFT significantly higher in terms of model consistency, clarity, and maintainability. The results are promising for the potential of CFT as a model-based approach.
Jessica Jung, Andreas Jedlitschka, Kai Höfig, Dominik Domis, Martin Hiller
DFTCalc: A Tool for Efficient Fault Tree Analysis
Abstract
Effective risk management is a key to ensure that our nuclear power plants, medical equipment, and power grids are dependable; and it is often required by law. Fault Tree Analysis (FTA) is a widely used methodology here, computing important dependability measures like system reliability. This paper presents DFTCalc, a powerful tool for FTA, providing (1) efficient fault tree modelling via compact representations; (2) effective analysis, allowing a wide range of dependability properties to be analysed (3) efficient analysis, via state-of-the-art stochastic techniques; and (4) a flexible and extensible framework, where gates can easily be changed or added. Technically, DFTCalc is realised via stochastic model checking, an innovative technique offering a wide plethora of powerful analysis techniques, including aggressive compression techniques to keep the underlying state space small.
Florian Arnold, Axel Belinfante, Freark Van der Berg, Dennis Guck, Mariëlle Stoelinga
Backmatter
Metadaten
Titel
Computer Safety, Reliability, and Security
herausgegeben von
Friedemann Bitsch
Jérémie Guiochet
Mohamed Kaâniche
Copyright-Jahr
2013
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-40793-2
Print ISBN
978-3-642-40792-5
DOI
https://doi.org/10.1007/978-3-642-40793-2

Premium Partner

    Bildnachweise