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

2011 | Book

Preliminary Interdependency Analysis (PIA): Method and Tool Support Read chapter Read first chapter

Software Engineering for Resilient Systems

Third International Workshop, SERENE 2011, Geneva, Switzerland, September 29-30, 2011. Proceedings

Editor: Elena A. Troubitsyna

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 Third International Workshop on Software Engineering for Resilient Systems, SERENE 2011, held in Geneva, Switzerland, in September 2011.

The 13 revised full papers presented together with 2 invited talks were carefully reviewed and selected from numerous submissions. The papers address all aspects of formal modeling and verification, architecting resilient systems, fault tolerance, requirements engineering and product lines, monitoring and self-adaption, and security and intrusion avoidance.

Table of Contents

Frontmatter

Invited Talk

Preliminary Interdependency Analysis (PIA): Method and Tool Support
Abstract
One of the greatest challenges in enhancing the protection of Critical Infrastructures (CIs) against accidents, natural disasters, and acts of terrorism is establishing and maintaining an understanding of the interdependencies between infrastructures. Understanding interdependencies is a challenge both for governments and for infrastructure owners/operators. Both, to a different extent, have an interest in services and tools that can enhance their risk assessment and management to mitigate large failures that may propagate across infrastructures. The abstract presents an approach (the method and tool support) to interdependency analysis developed recently by Centre for Software Reliability, City University London. The method progresses from a qualitative phase during which a fairly abstract model is built of interacting infrastructures. Via steps of incremental refinement more detailed models are built, which allow for quantifying interdependencies. The tool support follows the methodology and allows analysts to build quickly models at the appropriate level of abstraction (qualitative or very detailed including deterministic models specific for the particular domain, e.g. various flow models). The approach was successfully applied to a large scale case-study with more than 800 modeling elements.
Peter Popov

Formal Modelling and Verification

Use Case Scenarios as Verification Conditions: Event-B/Flow Approach
Abstract
Model-oriented formalisms rely on a combination of safety constraints and satisfaction of refinement obligations to demonstrate model correctness. We argue that for a significant class of models a substantial part of the desired model behaviour would not be covered by such correctness conditions, meaning that a formal development potentially ends with a correct model inadequate for its purpose. In this paper we present a method for augmenting Event-B specifications with additional proof obligations expressed in a visual, diagrammatic way. A case study illustrates how the method may be used to strengthen a model by translating use case scenarios from requirement documents into formal statements over a modelled system.
Alexei Iliasov
Quantitative Verification of System Safety in Event-B
Abstract
Certification of safety-critical systems requires formal verification of system properties and behaviour as well as quantitative demonstration of safety. Usually, formal modelling frameworks do not include quantitative assessment of safety. This has a negative impact on productivity and predictability of system development. In this paper we present an approach to integrating quantitative safety analysis into formal system modelling and verification in Event-B. The proposed approach is based on an extension of Event-B, which allows us to perform quantitative assessment of safety within proof-based verification of system behaviour. This enables development of systems that are not only correct but also safe by construction. The approach is demonstrated by a case study – an automatic railway crossing system.
Anton Tarasyuk, Elena Troubitsyna, Linas Laibinis
Experience-Based Model Refinement
Abstract
The resilience of a software system can be guaranteed, among other techniques, by model checking. In that setting, it consists in exploring every execution of the system to detect violations of resilience properties. One approach is to automatically transform the program into a model. To harness the system complexity and the state space explosion, designers usually abstract details of the studied system. However, abstracting too many details may dramatically impact the validity of the model checking. This includes details about the execution environment on which resilience properties are often based. This article sketches an iterative methodology to verify and refine the transformation. We introduce the concept of witness programs to reveal a set of behaviors that the transformation must preserve.
Didier Buchs, Steve Hostettler, Alexis Marechal

Architecting Resilient Systems

Architecting Resilient Computing Systems: Overall Approach and Open Issues
Abstract
Resilient systems are expected to continuously provide trustworthy services despite changes in the environment or in the requirements they must comply with. In this paper, we focus on a methodology to provide adaptation mechanisms meant to ensure dependability while coping with various modifications of applications and system context. To this aim, we propose a representation of dependability-related attributes that may evolve during the system’s lifecycle, and show why this representation is useful to provide adaptation of dependability mechanisms at runtime.
Miruna Stoicescu, Jean-Charles Fabre, Matthieu Roy
Supporting Architectural Design Decisions Evolution through Model Driven Engineering
Abstract
Architectural design decisions (i.e., those decisions made when architecting software systems) are considered an essential piece of knowledge to be carefully documented and maintained. As any other artifact, architectural design decisions may evolve, having an impact on other design decisions, or on related artifacts (like requirements and architectural elements). It is therefore important to document and analyze the impact of an evolving decision on other related decisions or artifacts. In this work we propose an approach based on a notation-independent metamodel that becomes a means for systematically defining traceability links, enabling inter-decision and extra-decision evolution impact analysis. The purpose of such an analysis is to check the presence of inconsistencies that may occur during evolution. An Eclipse plugin has been realized to implement the approach.
Ivano Malavolta, Henry Muccini, V. Smrithi Rekha

Fault Tolerance

On Enabling Dependability Assurance in Heterogeneous Networks through Automated Model-Based Analysis
Abstract
We present the specification of a basic library of dependability mechanisms that can be used within automated approaches for synthesising dependable connectors in heterogeneous networks. The library builds on classical dependability patterns, such as majority voting and retry, and uses the concept of overlay networks for triggering the synthesis of specific dependability mechanisms in the connector from high-level specifications. We translated such dependability mechanisms into SAN models with the aim to evaluate, through model-based analysis, which dependability mechanisms should be embedded in the synthesised connector for ensuring a given dependability level between networked systems willing to be connected. A case study is also presented to show the application of selected library mechanisms. This work is carried out in the context of connect, a European FET project which is investigating the possibility of enabling long-lasting inter-operation among networked systems by synthesising mediating connectors at run-time.
Paolo Masci, Nicola Nostro, Felicita Di Giandomenico
Supporting Cross-Language Exception Handling When Extending Applications with Embedded Languages
Abstract
Software applications increasingly deploy scripting embedded languages for extensibility, letting introduce custom extensions on top of the original application components. This results in two language layers, the one in which the application is implemented and the embedded language itself in which the extensions are written. During runtime, active calls amongst these two layers may be naturally intermixed, posing challenges for intuitive cross-language exception handling. At present, besides all .NET languages which cooperate by relying on a common language infrastructure, cross-language exception handling is not supported by existing embedded languages like Python, Perl, Ruby and Lua. We discuss the requirements for cross-exception handling and we show how they are accommodated via small-scale amendments in the embedded language API and runtime.
Anthony Savidis

Requirements Engineering and Product Lines

Guaranteeing Correct Evolution of Software Product Lines: Setting Up the Problem
Abstract
The research question that we posed ourselves and which has led to this paper is: how can we guarantee the correct functioning of products of an SPL when core components evolve? This exploratory paper merely proposes an overview of a novel approach that, by extending and adapting assume-guarantee reasoning to evolving SPLs, guarantees the resilience against changes in the environment of products of an SPL. The idea is to selectively model check and test assume-guarantee properties on those SPL components affected by the changes.
Maurice H. ter Beek, Henry Muccini, Patrizio Pelliccione
Idealized Fault-Tolerant Components in Requirements Engineering
Abstract
We have previously proposed a requirements development process, DREP, for dependable systems. In this paper, we draw a parallel between the notions defined in DREP and the elements of idealized fault-tolerant components (IFTCs). We show how the key ideas of IFTCs can be re-interpreted at the requirements engineering level and mapped to DREP concepts.
Sadaf Mustafiz, Jörg Kienzle

Invited Talk

Predictability and Evolution in Resilient Systems
Abstract
This paper gives a short overview of the talk related to the challenges in software development of resilient systems. The challenges come of the resilience characteristic as such; it a system emerging lifecycle property, neither directly measurable nor computable. While software is an essential part of a system, its analysis not enough for determining the system resilience. The talk will discuss about system resilience reasoning, its limitations, and possible approaches in the software design that include resilience analysis.
Ivica Crnkovic

Monitoring and Self-adaptation

Self-organising Pervasive Ecosystems: A Crowd Evacuation Example
Abstract
The dynamics of pervasive ecosystems are typically highly unpredictable, and therefore self-organising approaches are often exploited to make their applications resilient to changes and failures. The SAPERE approach we illustrate in this paper aims at addressing this issue by taking inspiration from natural ecosystems, which are regulated by a limited set of “laws” evolving the population of individuals in a self-organising way. Analogously, in our approach, a set of so-called eco-laws coordinate the individuals of the pervasive computing system (humans, devices, signals), in a way that is shown to be expressive enough to model and implement interesting real-life scenarios. We exemplify the proposed framework discussing a crowd evacuation application, tuning and validating it by simulation.
Sara Montagna, Mirko Viroli, Matteo Risoldi, Danilo Pianini, Giovanna Di Marzo Serugendo
Towards a Model-Driven Infrastructure for Runtime Monitoring
Abstract
In modern pervasive dynamic and eternal systems, software must be able to self-organize its structure and self-adapt its behavior to enhance its resilience and provide the desired quality of service. In this high-dynamic and unpredictable scenario, flexible and reconfigurable monitoring infrastructures become key instruments to verify at runtime functional and non-functional properties. In this paper, we propose a property-driven approach to runtime monitoring that is based on a comprehensive Property Meta-Model (PMM) and on a generic configurable monitoring infrastructure. PMM supports the definition of quantitative and qualitative properties in a machine-processable way making it possible to configure the monitors dynamically. Examples of implementation and applications of the proposed model-driven monitoring infrastructure are excerpted from the ongoing connect European Project.
Antonia Bertolino, Antonello Calabrò, Francesca Lonetti, Antinisca Di Marco, Antonino Sabetta

Security and Intrusion Avoidance

Using Diversity in Cloud-Based Deployment Environment to Avoid Intrusions
Abstract
This paper puts forward a generic intrusion-avoidance architecture to be used for deploying web services on the cloud. The architecture, targeting the IaaS cloud providers, avoids intrusions by employing software diversity at various system levels and dynamically reconfiguring the cloud deployment environment. The paper studies intrusions caused by vulnerabilities of system software and discusses an approach allowing the system architects to decrease the risk of intrusions. This solution will also reduce the so-called system’s days-of-risk which is calculated as a time period of an increased security risk between the time when a vulnerability is publicly disclosed to the time when a patch is available to fix it.
Anatoliy Gorbenko, Vyacheslav Kharchenko, Olga Tarasyuk, Alexander Romanovsky
‘Known Secure Sensor Measurements’ for Critical Infrastructure Systems: Detecting Falsification of System State
Abstract
This paper describes a first investigation on a low cost and low false alarm, reliable mechanism for detecting manipulation of critical physical processes and falsification of system state. We call this novel mechanism Known Secure Sensor Measurements (KSSM). The method moves beyond analysis of network traffic and host based state information, in fact it uses physical measurements of the process being controlled to detect falsification of state. KSSM is intended to be incorporated into the design of new, resilient, cost effective critical infrastructure control systems. It can also be included in incremental upgrades of already installed systems for enhanced resilience. KSSM is based on known secure physical measurements for assessing the likelihood of an attack and will demonstrate a practical approach to creating, transmitting, and using the known secure measurements for detection.
Miles McQueen, Annarita Giani
Backmatter
Metadata
Title
Software Engineering for Resilient Systems
Editor
Elena A. Troubitsyna
Copyright Year
2011
Publisher
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-24124-6
Print ISBN
978-3-642-24123-9
DOI
https://doi.org/10.1007/978-3-642-24124-6

Premium Partner

    Image Credits