Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

2013 | Book

Empirical Assessment of Resilience Read chapter Read first chapter

Software Engineering for Resilient Systems

5th International Workshop, SERENE 2013, Kiev, Ukraine, October 3-4, 2013. Proceedings

Editors: Anatoliy Gorbenko, Alexander Romanovsky, Vyacheslav Kharchenko

Publisher: Springer Berlin Heidelberg

Book Series : Lecture Notes in Computer Science

Part of: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Login to get access
insite
SEARCH

About this book

This book constitutes the refereed proceedings of the 5th International Workshop on Software Engineering for Resilient Systems, SERENE 2013, held in Kiev, Ukraine, in October 2013. The 13 revised full papers were carefully reviewed and selected from 21 submissions. The papers are organized in topical sections on resilient software and design, rigorous reasoning, applications, concepts, and analysis.

Table of Contents

Frontmatter

Keynote Talks

Empirical Assessment of Resilience
Abstract
Resilience is the ability of a system to return to its normal operation state after a change or disturbance. Frequently, resilience of a system can be only empirically estimated due to the complexity of the underlying mechanisms. While traditional dependability uses quantitative characteristics based on averaging the impacts of faults, resilience requires more focused attributes on the impacts of disturbances. The paper summarizes the main requirements on the statistical background needed for resilience characterization and presents an approach based on Exploratory Data Analysis (EDA) helping to understand disturbance impacts and their respective quantitative characterization.
András Pataricza, Imre Kocsis, Ágnes Salánki, László Gönczy
Security-Informed Safety: If It’s Not Secure, It’s Not Safe
Abstract
Traditionally, safety and security have been treated as separate disciplines, but this position is increasingly becoming untenable and stakeholders are beginning to argue that if it’s not secure, it’s not safe. In this paper we present some of the work we have been doing on “security-informed safety”. Our approach is based on the use of structured safety cases and we discuss the impact that security might have on an existing safety case. We also outline a method we have been developing for assessing the security risks associated with an existing safety system such as a large-scale critical infrastructure.
Robin Bloomfield, Kateryna Netkachova, Robert Stroud

Resilient Software and Design

Engineering a Platform for Mission Planning of Autonomous and Resilient Quadrotors
Abstract
Quadrotors and UAVs in general are becoming as attractive instruments to safely and efficiently perform environmental monitoring missions. In professional use, quadrotors are manually controlled by expert operators via a remote controller. In research, several projects provide various degrees of automation for the execution of the mission; however, those projects are based on the use of programming languages which are too distant from the background of the stakeholders operating in the field (e.g., fire fighters, policemen, etc.).
In this paper we propose FLYAQ, a platform enabling to (i) graphically define monitoring missions via a web interface, (ii) decompose the mission according to the number and nature of available quadrotors, and (iii) generate the implementation code orchestrating all the quadrotors of the swarm to fulfil the common goal of the mission. The FLYAQ platform enables operators to focus on the mission itself, rather than on technical concerns arising from the use of quadrotors.
A reconfiguration engine is specifically designed to make the swarm resilient to faults and external events that may compromise the mission. Moreover, under some limitations explained in the paper, the reconfiguration engine permits to change the mission at run-time. The FLYAQ platform will be distributed as an open-source product.
Davide Di Ruscio, Ivano Malavolta, Patrizio Pelliccione
Towards Agile Development of Critical Software
Abstract
The paper presents a case study aiming at collecting opinions of software engineers on the risks related to integration of agile practices to safety-critical software development projects. The study has been performed within the scope of our research targeting at providing critical software developers with a solution allowing to incorporate agile practices into software development process while still being conformant with the software assurance requirements imposed by the application domain. We describe the tasks performed by the participants and the results of these tasks together with the overall conclusions derived during the workshop summarizing the case study.
Janusz Górski, Katarzyna Łukasiewicz
Supporting the Evolution of Free and Open Source Software Distributions
Abstract
This paper overviews Mancoosi, an European project in the 7th Research Framework Programme (FP7) of the European Commission, on managing software complexity. The focus of the project has been on managing the evolution of Free and Open Source Software distributions. Evolution of these distributions is realized through the upgrade, the addition, and the removal of software packages. The project has two main objectives: (i) develop a model-based approach to safely support the upgrade of FOSS systems, (ii) develop better algorithms and tools to plan upgrade paths based on various information sources about software packages and on optimization criteria.
The paper focuses on the first objective of the project. The main result of this objective is an approach that promotes the simulation of upgrades to predict failures before affecting the real system. Both fine-grained static aspects (e.g., configuration incoherences) and dynamic aspects (e.g., the execution of configuration scripts) are taken into account, improving over the state of the art of package managers.
Davide Di Ruscio, Patrizio Pelliccione

Rigorous Reasoning

Optimizing Verification of Structurally Evolving Algebraic Petri Nets
Abstract
System models are subject to evolve during the development life cycle, along which an initial version goes through a series of evolutions, generally aimed at progressively reaching all the requested qualities (completeness, correctness etc.). Among the existing development methodologies the iterative and incremental one has been proved to be efficient for system development but lacks of support for an adequate verification process. When considering Algebraic Petri nets (APNs) for modeling and model checking for verification, all the proofs must be redone after each iteration which is impractical both in terms of time and space. In this work, we introduce an Algebraic Petri net slicing technique that optimizes the model checking of static or structurally evolving APN models. Furthermore, our approach is proposing a classification of evolutions dedicated to the improvement of model checking.
Yasir Imtiaz Khan
A Case Study in Refinement-Based Modelling of a Resilient Control System
Abstract
In this paper, we present a case study in modelling a resilient control system in Event-B. We demonstrate how to formally define the basic safety properties and fault tolerance mechanisms, as well as the system modes describing the system behaviour under different execution and fault conditions. Our formal development helps us to identify the diagnosability conditions for resilience, i.e., identify the limitations to be imposed on possible component changes to guarantee its controllability and hence dependability.
Yuliya Prokhorova, Elena Troubitsyna, Linas Laibinis
Synthesis of Resilient Choreographies
Abstract
A possible Service Engineering (SE) approach to build service-based systems is to compose together distributed services by considering a global specification of their interactions, namely a choreography. BPMN2 (Business Process Modeling Notation v2.0) provides a dedicated notation, called Choreography Diagrams, to define the global expected behavior between interacting participants. An interesting problem worth considering concerns choreography realizability enforcement, while ensuring a resilient evolution upon facing changes. The strategy that we adopt to solve this problem is twofold: given a BPMN2 choreography specification and a set of existing services discovered as possible participants, (i) adapt their interaction protocol to the choreography roles and (ii) coordinate their (adapted) interaction so to fulfill the global collaboration prescribed by the choreography. This paper proposes a synthesis approach able to automatically generate, out of a BPMN2 choreography specification, the needed adaptation and coordination logic, and distribute it between the participants so to enforce the choreography. Our approach supports choreography evolution through adaptation to possible changes in the discovered services, while still keeping the prescribed coordination.
Marco Autili, Amleto Di Salle, Massimo Tivoli

Applications

Formal Development and Quantitative Assessment of a Resilient Multi-robotic System
Abstract
Ensuring resilience of multi-robotic systems is a notoriously difficult task. Decentralised architectures and asynchronous communication require powerful modelling techniques to demonstrate system resilience. In this paper, resilience of a multi-robotic system is defined as the ability to achieve goals despite robot failures. We demonstrate how to rigorously specify and verify essential properties of resilience mechanisms of multi-robotic systems by refinement in Event-B. To assess the desired resilience characteristics, we augment our formal models with statistical data and rely on probabilistic verification. The automated support provided by the PRISM model checker allows us to calculate the probability of goal reachability in the presence of robot failures and compare different reconfiguration strategies for selected architectures. We demonstrate our approach by a case study – development and assessment of a cleaning multi-robotic system.
Anton Tarasyuk, Inna Pereverzeva, Elena Troubitsyna, Linas Laibinis
The SafeCap Project on Railway Safety Verification and Capacity Simulation
Abstract
This paper introduces the UK SafeCap project on Overcoming the railway capacity challenges without undermining rail network safety. The focus of the project has been on developing methods and tools that will allow signalling engineers to model railway nodes (junctions and stations), to verify their safety and to analyse the node capacity provided the safety is ensured. The paper outlines the project approach, its objectives and the outcomes. The main result of the project is the development of a method for analysing railway safety and capacity in a unified way and the Eclipse-based SafeCap platform supporting this method. The platform is extendable with the new modelling plugins and is openly available at SourceForge. It has been developed in a close cooperation with industry and thoroughly evaluated using the layouts of several UK railway stations.
Alexei Iliasov, Ilya Lopatkin, Alexander Romanovsky
Modeling of Autonomous Vehicle Operation in Intelligent Transportation Systems
Abstract
The past decade has seen autonomous vehicles become the subject of considerable research and development activity. The majority of these advances have focused on individual vehicles, rather than the interactions that result when autonomous (unmanned) and conventional (manned) vehicles come together in an intelligent transportation system. The robustness of autonomous vehicles to contingencies caused by unpredictable human behavior is a critical safety concern. Assuring the reliability, availability, security, and similar non-functional attributes of autonomous vehicles is just as critical.
The doctoral research proposed in this paper centers on developing models capable of accurately representing environments where manned and unmanned vehicles coexist. An established macroscopic transportation model serves as the basis for the proposed work, and will be extended to differentiate between manned and autonomous vehicles. Stochastic methods will be applied to reflect the non-determinism of the operating environment, especially as related to driver behavior, and will facilitate analysis of robustness. The goal is to capture both basic operation of autonomous vehicles, as well as advanced capabilities such as platooning and robotic adaptation. The insights gained from these models are expected to facilitate the design of intelligent transportation systems that are both safe and efficient.
Mark Woodard, Sahra Sedigh

Concepts

Preliminary Contributions Towards Auto-resilience
Abstract
The variability in the conditions of deployment environments introduces new challenges for the resilience of our computer systems. As a response to said challenges, novel approaches must be devised so that identity robustness be guaranteed autonomously and with minimal overhead. This paper provides the elements of one such approach. First, building on top of previous results, we formulate a metric framework to compare specific aspects of the resilience of systems and environments. Such framework is then put to use by sketching the elements of a handshake mechanism between systems declaring their resilience figures and environments stating their minimal resilience requirements. Despite its simple formulation it is shown how said mechanism enables scenarios in which resilience can be autonomously enhanced, e.g., through forms of social collaboration. This paves the way to future “auto-resilient” systems, namely systems able to reason and revise their own architectures and organisations so as to optimally guarantee identity persistence.
Vincenzo De Florio
A New Approach to Software Reliability
Abstract
The paper describes a new approach to the software reliability, which is not based on the probability theory, but on the non-equilibrium process theory. It is assumed that defects in the software arise as a result of incoming and outcoming defect flows. Using obtained relations it is possible to predict the amount of identified and entered into the system defects and simulate the reliability of software systems taking into account the secondary defect. The paper shows that the majority of the existing software reliability models ensue from the dynamics of software systems.
Dmitry A. Maevsky

Analysis

Static Analysis Approach for Defect Detection in Multithreaded C/C++ Programs
Abstract
Automatic defect detection in multithreaded programs with pointers and recursion is a real challenge. In this paper we present a static analysis approach targeted to detection of wide range of defect types in multithreaded programs, including some types of synchronization errors. This approach is based on well-known algorithms for interval and points-to analysis, which are extended with the developed algorithms for analysis of parallel execution. We show efficiency of our approach by evaluating it on a set of artificial and real-world multithreaded C/C++ programs based on Pthreads.
Mikhail Moiseev
Stochastic Model-Based Analysis of Railway Operation to Support Traffic Planning
Abstract
The possibility to analyze aspects of the railway capacity at varying the trains population, their travel time and delays, appears to be a useful means to investigate critical situations that affect quality of service in railway systems. In order to satisfy the required levels of the transport service, the capacity may be verified and estimated with good approximation by railway operation simulation models that should be easily applied on every railway plant. This work presents a stochastic model used for railway operation simulation. This model takes in input information about the railway topology and the required service. It reproduces the operation of the elementary devices composing the railway system using the Stochastic Activity Networks (SAN) formalism and the C++ programming language. The model may be applied in railway traffic studies as support for timetable improvements for delay minimization and for planning infrastructural upgrades.
Felicita Di Giandomenico, Alessandro Fantechi, Stefania Gnesi, Massimiliano Leone Itria
Backmatter
Metadata
Title
Software Engineering for Resilient Systems
Editors
Anatoliy Gorbenko
Alexander Romanovsky
Vyacheslav Kharchenko
Copyright Year
2013
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-40894-6
Print ISBN
978-3-642-40893-9
DOI
https://doi.org/10.1007/978-3-642-40894-6

Premium Partner

    Image Credits