View other issues

Contents

Special Theme

Introduction to the Special Theme "Safety-Critical Software"

by Pedro Merino and Erwin Schoitsch

Each day, our lives become more dependent on 'software-intensive systems' - digital information technology embedded in our environment. This includes not only automotive devices and controls, railways, aircraft and aerospace, but also the medical devices sector, 'mobile worlds' and 'e-worlds', the 'smart' home, clothes, factories and numerous other domains. Software is the main driver for innovations in all sectors, and most of the innovative features of new products would not be possible without software. New processors and methods of processing, sensors, actuators, communications and infrastructure are enablers for a truly pervasive computing environment; that is, omnipresent but almost invisible to the user, and as such the basis for an economic push. Software plays a critical role in this context, having an impact in areas such as complexity, security and privacy in a connected world, validation, verification and certification of software-intensive systems, and maintenance of these systems over long periods. The functional safety standards of the International Electrotechnical Commission (IEC) 61508 group (generic and domain-specific standards) and the ISO 26262 standard on 'road vehicles - functional safety' currently under development, include separate software-specific parts (IEC 61508 part 3, ISO 26262 part 6).

Read more...

Software Safety and Rocket Science

by Gerard J. Holzmann

The amount of software that was used for the first moon landing in 1969 was the equivalent of perhaps 7500 lines of C code. Of course at that time the language C didn't exist - the code was written in assembly and had to fit within the 36864 words of memory that the computer in the lunar lander supported. A lot has changed since then. Today, a desktop PC can have up to a million times more memory. What is fascinating, though, is that today there are hardly any applications that require fewer lines of code than that first lunar lander. Clearly, few of these applications solve problems that are more difficult than landing a spacecraft on the moon.

Read more...

Model-Checking of Safety-Critical Software for Avionics

by Darren Cofer, Michael Whalen and Steven Miller

The adoption of model-based development tools is changing the cost-benefit equation for the industrial use of formal methods. The integration of formal methods such as model checking into software development environments makes it possible to fight increasing cost and complexity with automation and rigour.

Read more...

Software Reliability Assessment by Statistical Analysis of Operational Experience

by Sven Söhnlein and Francesca Saglietti

Statistical testing represents a well-founded approach to the estimation of software reliability. Its major drawback - namely the prohibitive testing effort it usually requires - can be overcome by efficient exploitation of operational evidence gained with pre-developed software components and by the loss-free combination of component-specific reliability estimates.

Read more...

Analysing Human Aspects of Safety-Critical Software

by Michael D. Harrison and José Creissac Campos

In focusing on human system interactions, the challenge for software engineers is to build systems that allow users to carry out activities and achieve objectives effectively and safely. A well-designed system should also provide a better experience of use, reducing stress and frustration. Many methods aim to help designers to produce systems that have these characteristics. Our research is concerned with the use of formal techniques to help construct such interactive systems.

Read more...

Model-Driven Development of Embedded Real-Time Systems

by Alexandre David and Brian Nielsen

Model-driven development (MDD) has an enormous potential for improving verification, testing and synthesis of embedded systems. Our UPPAAL tool-suite for MDD of embedded real-time systems has recently been extended with components for automatic test generation and code synthesis. Presentation and demonstration at a European industrial conference on Systematic Testing spawned a lot of interest in these new techniques.

Read more...

Quasimodo

by Brian Nielsen

Existing Model-Driven Development (MDD) tools and methods for real-time embedded systems are rather poor at handling the relevant quantitative constraints. Quasimodo (Quantitative System Properties in Model-Driven Design of Embedded Systems) is a new EU FP7 project whose main goal is to extend current MDD techniques and tools for modelling, verification, testing and code generation with the ability to satisfy these quantitative constraints.

Read more...

From Rigorous Requirements Engineering to Formal System Design

by Christophe Ponsard, Philippe Massonet, Gautier Dallons

The majority of systems that control our daily lives rely on software. Often this software is embedded in the device and remains invisible to users. While the consequences of a failure may be minor, such as failing to deliver part of the requested service, they may also be dramatic, possibly causing human injury or even fatalities (eg car crashes or train collisions). In recent years, CETIC (Centre d'Excellence en Technologies de l'Information et de la Communication) has devoted significant effort to the development of industrial methods and tools that target safety-critical software, with a specific focus on the early phase of system development.

Read more...

Modelling the Role of Software in the Propagation of Failures across Infrastructures

by Chris W. Johnson

In recent years, terrorist attacks, system failures and natural disasters have revealed the problems that many countries face in preparing for national civil contingencies. The diversity of critical infrastructures and the interconnections between different systems make it difficult for planners to anticipate everything. For example, the loss of power distribution networks can disrupt rail and road transportation systems. Knock-on effects can also be felt across telecommunications infrastructures as the uninterruptible power supplies (UPS) that protect mobile phone base stations fail over time. In addition, domestic water supplies are affected when pumping and treatment centres lose power.

Read more...

Model-Based Development of Distributed Embedded Real-Time Systems

by Wolfgang Herzner, Martin Schlager, György Csertan, Bernhard Huber, Thierry Le-Sergent, Erwin Schoitsch and Rupert Schlick

The increasing complexity of distributed embedded systems, as found today in cars, aeroplanes and trains, is becoming a critical cost factor in their development. In the European 'Integrated Project' DECOS (Dependable Embedded Components and Systems), an integrated, model-driven tool-chain has been developed to accompany the system development process from design to deployment.

Read more...

Safe Systems with Software Components in SOFA 2

by Tomáš Bureš and Petr Hnětynka

Embedded devices like mobile phones, PDAs, set-top boxes and vehicular systems are now an inherent part of daily human life. However, software for these devices must meet additional requirements compared to desktop and server computers. We present the SOFA 2 component system, which is suitable for building safe and configurable applications.

Read more...

New Paradigms and Tools for High-Assurance Systems Modelling

by Francesco Flammini, Nicola Mazzocca and Valeria Vittorini

Modern critical computer systems are rapidly growing in complexity. As a consequence, novel frameworks are needed to support multi-paradigm modelling for the dependability evaluation of such systems. OsMoSys (Object-based multi-formalism modelling of systems) is one of the latest projects in this category, whose originality consists in supporting certain aspects of object orientation and in the model analysis.

Read more...

Testing Concurrent Software with Ants

by Francisco Chicano and Enrique Alba

Mimicking the behaviour of ants in nature can lead to the identification of subtle errors in concurrent software systems and thereby boost the efficiency of model checking.

Read more...

Verifying Dynamic Properties of Industrial Critical Systems Using TOPCASED/FIACRE

by Bernard Berthomieu, Hubert Garavel, Frédéric Lang and François Vernadat

The TOPCASED project (Toolkit in Open source for Critical Applications and SystEm Development) of Aerospace Valley ('Pôle de compétitivité' in aerospace activities) has developed an extensible toolbox that provides graphical environments for mission-critical systems engineering. Within this project, the FIACRE intermediate format allows the connection of several graphical models to verification tools such as CADP and TINA, as well as the factoring of expensive developments.

Read more...

A Component-Based Approach for the Verification of Safety-Critical Software

by Jeanine Souquières

The platoon of vehicles is a mixture of distributed and embedded systems. The former are usually hard to understand and debug as they can exhibit obscure behaviours. The latter must satisfy safety/security/confidence requirements, both when standing alone and when composed together. To address these problems, we propose a component-based development approach using the CSP||B framework of well-established formal methods: B for the development of provably correct software, and CSP for Communicating Sequential Processes.

Read more...

Checking and Enforcing Safety: Runtime Verification and Runtime Reflection

by Martin Leucker

Ultimately, a safety-critical software system should meet its safety requirements if it is continuously monitored, and corrected when safety violations are detected. We present Runtime Verification and Runtime Reflection as promising techniques that respectively monitor and steer safety-critical systems so that they always meet their safety requirements.

Read more...

LaQuSo: Using Formal Methods for Analysis of Safety-Cr

by Sjaak Smetsers and Marko van Eekelen

Due to its great complexity, it is inevitable that modern software will suffer from the presence of numerous errors. These software bugs are frequent sources of security vulnerabilities, and in safety-critical systems, they are not simply expensive annoyances: they can endanger lives. The growing demand for high availability and reliability of computer systems has led to a formal verification of such systems.

There are two principal approaches to formal verification: model checking and theorem proving.

Goal

Read more...

The SHADOWS Story on Implementation of Self-Healing Systems

by Marco Bakera and Tiziana Margaria

Industry-grade, large-scale software systems have an inherent need for autonomous mechanisms of adaptation. In our approach, a new game-based model-checking technique succeeds as a natural solution to the verification and adaptation task: the system becomes a player in a hostile world, and competes against any potential problems or mishaps.

Read more...

Test Coverage Analysis and Preservation for Requirements-Based Testing

by Raimund Kirner and Susanne Kandl

The testing process for safety-critical systems is usually evaluated with code coverage criteria such as MC/DC (Modified Condition/Decision Coverage) defined in the standard DO-178B, Software Considerations in Airborne Systems and Equipment Certification (a de-facto standard for certifying software in the civil avionic domain). For requirements-based testing techniques we work on coverage metrics that are defined on a higher level of program representation (eg on the requirements), and that are independent of a specific implementation. For that purpose we analyse the relationship between existing definitions for structural requirement-coverage metrics and structural code-coverage metrics. In addition, we work on techniques that preserve structural code-coverage between different program-representation levels.

Read more...

A Step towards Generating Efficient Test Cases - the Project MOGENTES

by Wolfgang Herzner, Rupert Schlick, Manfred Gruber

The goal of MOGENTES (MOdel-based GENeration of Tests for Embedded Systems) is to significantly enhance testing and verification of dependable embedded systems. This is achieved by automatically generating efficient test cases by relying on the development of new approaches as well as innovative integration of state-of-the-art techniques. In particular, MOGENTES will apply this technology in large industrial systems in the automotive, railway control and off-road vehicle industries.

Read more...

SESAME: A Model-Driven Test Selection Process for Safety-Critical Embedded Systems

by Nicolas Guelfi and Benoît Ries

SESAME (Specification based testing of safety-critical small-sized embedded systems) is an industrial research project in the field of embedded systems test methodologies. The first targeted systems are small embedded systems developed by the Luxembourg company IEE S.A. for the control of airbags through sensors or infrared cameras.

Read more...

ProSE - Promoting Standardization for Embedded Systems

by Erwin Schoitsch and Laila Gide

During the last few years, standardization was identified both by the European Commission (EC) and by industry as a new issue of strategic importance for the creation of markets. It was one of the concerns of the EC, especially of the Embedded Systems Unit of the Directorate General 'Information Society and Media', that the results of funded research projects are having only a minimal impact on standardization. The Standards Working Group of ARTEMIS, the European Technology Platform for Embedded Intelligence and Systems, proposed an FP7 support action ProSE (Promotion of Standardization for Embedded Systems), to promote standardization in the (dependable) embedded systems field. This was accepted and it commenced in May 2008.

Read more...

Bicriteria Multi-Processor Static Scheduling

by Alain Girault and Hamoudi Kalla

The reliability of a system indicates its continuity of service. It is formally defined as the probability that it will function correctly during a given time interval. With the advent of ubiquitous computing and distributed embedded systems, it is becoming an increasingly crucial aspect. We propose a framework for designing highly reliable real-time systems, thanks to a novel bicriteria (length and reliability) static multiprocessor scheduling heuristic. The first criterion is the schedule's length, which assesses the system's real-time property, while the second is reliability, assessing the system's dependability.

Read more...

Enhancing Java ME Security Support with Resource Usage Monitoring

by Fabio Martinelli, Fabio Massacci, Paolo Mori, Christian Schaefer and Thomas Walter

Capabilities and Ubiquity of mobile devices have dramatically increased in the last few years, with many mobile devices now able to run Java applications, create Internet connections, send SMS messages, and perform other expensive or dangerous operations. As a consequence, better security support is required. We propose an approach to enhance the security support of Java Micro Edition using MIDlets to monitor the usage of mobile device resources.

Read more...

TAS Control Platform: A Platform for Safety-Critical Railway Applications

by Andreas Gerstinger, Heinz Kantz and Christoph Scherrer

Within the railway industry, the need for computer systems to perform safety-critical tasks is constantly increasing. A typical application is the railway interlocking system (Figure 1): these systems control the state of the signals and switches on railway lines and are therefore responsible for safe train operation. An incorrect output from such a system may in the worst case lead to a train collision. Other applications in the railway domain are axle counters along railway lines, computer systems on board trains, and field element controllers that operate under rough environmental conditions.

Read more...

Experimenting with Diversity in the Formal Development of Railway Signalling Systems

by Alessandro Fantechi, Stefania Gnesi and Giovanni Lombardi

As a result of collaborations with ALSTOM FERROVIARIA, the Formal Methods & Tools (FMT) group of ISTI-CNR has had access to real-world specifications for signalling equipment together with the complete environment needed to produce an industrial application, from a formal model to the final code. This opportunity has been exploited in an additional research activity aimed at reviewing the existing development process in terms of safety regulations. The underlying idea has been to introduce diversity in order to improve the safety of the equipment produced.

Read more...

Evaluation of Natural Language Requirements in the MODCONTROL Project

by Antonio Bucchiarone, Stefania Gnesi, Gianluca Trentanni and Alessandro Fantechi

We describe QuARS (Quality Analyzer for Requirement Specifications) Express, a customized version of the QuARS tool. It is designed to evaluate natural language requirements, can handle complex and structured data formats containing metadata, and is able to produce an analysis report with categorized information.

Read more...

Development of Safety Software for the Paks Nuclear Power Plant

by Tamás Bartha and István Varga

Software development in a safety-critical environment requires that a rigorous process be followed in all phases of the system life cycle. Members of the Systems and Control Laboratory of SZTAKI are working together with experts at the Paks nuclear power plant in Hungary to develop new tools and support systems that will improve the dependability of the safety software.

Read more...

Catalonia boosts Education and Knowledge in Safety-Critical Software

A recent collaboration has led to the development of a professional training course in quality assurance for safety-critical software and systems, focused on the biomedical, transport and aerospace sectors.

Read more...

Requirements Engineering Lab at IPT São Paulo

To contribute to research in requirements engineering, the Instituto de Pesquisas Tecnológicas do Estado de São Paulo (IPT) decided to create the Requirements Engineering Laboratory.

Read more...