nach oben

2017 | Buch

Kapitel lesen Erstes Kapitel lesen

Formal Techniques for Safety-Critical Systems

5th International Workshop, FTSCS 2016, Tokyo, Japan, November 14, 2016, Revised Selected Papers

herausgegeben von: Cyrille Artho, Peter Csaba Ölveczky

Verlag: Springer International Publishing

Buchreihe : Communications in Computer and Information Science

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

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the refereed proceedings of the 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, held in Tokyo, Japan, in November 2016.
The 9 revised full papers presented together with an abstract of an invited talk were carefully reviewed and selected from 23 submissions. The papers are organized in topical sections on specification and verification; automotive and railway systems; circuits and cyber-physical systems; parametrized verification.

Inhaltsverzeichnis

Frontmatter

Specification and Verification

Frontmatter

Specification and Verification of Synchronization with Condition Variables

Abstract

In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables.

Pedro de Carvalho Gomes, Dilian Gurov, Marieke Huisman

An Interval Logic for Stream-Processing Functions: A Convolution-Based Construction

Abstract

We develop an interval-based logic for reasoning about systems consisting of components specified using stream-processing functions, which map streams of inputs to streams of outputs. The construction is algebraic and builds on a theory of convolution from formal power series. Using these algebraic foundations, we uniformly (and systematically) define operators for time- and space-based (de)composition. We also show that Banach’s fixed point theory can be incorporated into the framework, building on an existing theory of partially ordered monoids, which enables a feedback operator to be defined algebraically.

Brijesh Dongol

Automotive and Railway Systems

Frontmatter

Automating Time Series Safety Analysis for Automotive Control Systems in STPA Using Weighted Partial Max-SMT

Abstract

Recently, Systems-Theoretic Process Analysis (STPA) has been studied for automobile safety analysis. When STPA is used later in the design phase, significant effort is required to detect causal scenarios of unsafe control actions (UCAs), especially those related to intermittent disturbances in multiple signals. We propose a method to automate this disturbance detection by checking the satisfiability of trace formulas extended with cushion variables. At a state transition, cushion variable values are used instead of original variable values to determine the next state. A signal disturbance is regarded as assigning different values to variables and corresponding cushion variables. Specifying the equality between variables and cushion variables as soft clauses, a Weighted Partial Max-SMT solver mechanically searches an assignment for a trace to satisfy the UCA property. We applied the proposed technique to a simplified automotive control system to demonstrate some examples of automatic detections of reasonable intermittent multi-signal disturbances.

Shuichi Sato, Shogo Hattori, Hiroyuki Seki, Yutaka Inamori, Shoji Yuen

Uniform Modeling of Railway Operations

Abstract

We present a comprehensive model of railway operations written in the abstract behavioral specification (ABS) language. The model is based on specifications taken from the rulebooks of Deutsche Bahn AG. It is statically analyzable and executable, hence allows to use static and dynamic analysis within one and the same formalism. We are able to combine aspects of micro- and macroscopic modeling and provide a way to inspect changes in the rulebooks. We illustrate the static analysis capability by a safety analysis based on invariant reasoning that only relies on assumptions about the underlying railway infrastructure instead of explicitly exploring the state space. A concrete infrastructure layout and train schedule can be used as input to the model to examine dynamic properties such as delays. We illustrate the capability for dynamic analysis by demonstrating the effect that different ways of dealing with faulty signals have on delays.

Eduard Kamburjan, Reiner Hähnle

Circuits and Cyber-Physical Systems

Frontmatter

Formal Verification of Gate-Level Multiple Side Channel Parameters to Detect Hardware Trojans

Abstract

The enhancements in functionality, performance, and complexity in modern electronics systems have ensued the involvement of various entities, around the globe, in different phases of integrated circuit (IC) manufacturing. This environment has exposed the ICs to malicious intrusions also referred as Hardware Trojans (HTs). The detection of malicious intrusions in ICs with exhaustive simulations and testing is computationally intensive, and it takes substantial effort and time for all-encompassing verification. In order to overcome this limitation, in this paper, we propose a framework to formally model and analyze the gate-level side channel parameters, i.e., dynamic power and delay, for Hardware Trojan detection. We used the nuXmv model checker for the formal modeling and analysis of integrated circuits due to its inherent capability of handling real numbers and support of scalable SMT-based bounded model checking. The experimental results show that the proposed methodology is able to detect the intrusions by analyzing the failure of the specified linear temporal logic (LTL) properties, which are subsequently rendered into behavioural traces, indicating the potential attack paths in integrated circuits.

Imran Hafeez Abbasi, Faiq Khalid Lodhi, Awais Mehmood Kamboh, Osman Hasan

Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications

Abstract

Internet of Things (IoT) has been considered as an intuitive evolution of sensing systems using Wireless Sensor Networks (WSN). In this context, energefficiency is considered as one of the most critical requirement. For that purpose, the randomized node scheduling approach is largely applied. The randomness feature in the node scheduling together with the unpredictable deployment make probabilistic techniques much more appropriate to evaluate the coverage properties of WSNs. Classical probabilistic analysis techniques, such as simulation and model checking, do not guarantee accurate results, and thus are not suitable for analyzing mission-critical WSN applications. Based on the most recently developed probability theory, available in the HOL theorem prover, we develop the formalizations of the key coverage performance attributes: the coverage intensity of a specific point and the expected value of the network coverage intensity. The practical interest of our higher-order-logic developments is finally illustrated through formally analyzing the asymptotic coverage behavior of an hybrid monitoring framework for environmental IoT.

Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid

Shared-Variable Concurrency, Continuous Behaviour and Healthiness for Critical Cyberphysical Systems

Abstract

In the effort to develop critical cyberphysical systems, existing computing formalisms are extended to include continuous behaviour. This may happen in a way that neglects elements necessary for correct continuous properties and correct physical properties. A simple language is taken to illustrate this. Issues and risks latent in this kind of approach are identified and discussed under the umbrella of ‘healthiness conditions’. Modifications to the language in the light of the conditions discussed are described. An example air conditioning system is used to illustrate the concepts presented, and is developed both in the original language and in the modified version.

Richard Banach, Huibiao Zhu

Parametrized Verification

Frontmatter

Applying Parametric Model-Checking Techniques for Reusing Real-Time Critical Systems

Abstract

Due to the increase of complexity in real-time safety-critical systems, verification and validation costs have significantly increased. A straightforward way to reduce costs is to reuse existing systems, adapting them to new requirements, so as to avoid new costly developments. Our aim is to verify during the development strategy definition phase whether the existing products can be reused and adapted for a new customer, by identifying key parameters to be tuned in order to reuse existing products. Performing efficient verification is therefore crucial.

In this paper, we focus on the performance requirement aspects. Nowadays, model-checking techniques have improved significantly to verify the performances of real-time systems. However, model-checking cannot address real-time systems where some timing constants are unknown or uncertain. Parametric model-checking leverage this shortcoming by identifying parameter ranges for which the system is correct. We report here on an experiment of the evaluation of the use of these formal techniques applied to automatize the synthesis of good parameter ranges for system reuse in the setting of the environment requirements for an aerial video tracking system.

Baptiste Parquier, Laurent Rioux, Rafik Henia, Romain Soulat, Olivier H. Roux, Didier Lime, Étienne André

Parameterised Verification of Stabilisation Properties via Conditional Spotlight Abstraction

Abstract

Parameterised verification means to check properties of an arbitrary number of uniform processes composed in parallel. We introduce an approach to parameterised verification of stabilisation properties. Our approach exploits the fact that stabilisation happens incrementally, and thus, also can be verified incrementally. We systematically search for a provable partial stabilisation property and then verify full stabilisation under the assumption of partial stabilisation. In order to prove partial stabilisation we use a novel stabilisation cutoff technique. A proven partial stabilisation property allows us to apply our new technique conditional spotlight abstraction (CSA). CSA summarises an arbitrary number of processes into a finite model such that verification can be performed via model checking. Based on a prototype tool we were able to verify several protocols implemented as parameterised systems.

Nils Timm, Stefan Gruner

Backmatter

Titel: Formal Techniques for Safety-Critical Systems
herausgegeben von: Cyrille Artho
Peter Csaba Ölveczky
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-53946-1
Print ISBN: 978-3-319-53945-4
DOI: https://doi.org/10.1007/978-3-319-53946-1