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

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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