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).
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.