Reliable Software Technologies – Ada-Europe 2015

The development of mixed-criticality systems that integrate applications of different criticality levels (safety, security, real-time and non-real time) in a single embedded system can provide multiple benefits such as product cost-size-weight reduction, reliability increase and scalability. However, the integration of applications of different levels of criticality in a single embedded system leads to several challenges with respect to safety certification standards. This research paper describes a safety concept for a fail-safe wind turbine mixed-criticality control system based on multicore partitioning that meets IEC-61508 and ISO-13849 industrial safety standards. The safety concept has been positively assessed by a certification body.

The Rosetta-Philae space mission is an unprecedented venture. After a ten-year journey across the Solar System and many complicated manoeuvres, the Rosetta spacecraft smoothly approached a small (2-4 km in diameter) celestial body, comet CG/67P. Furthermore, the spacecraft executed additional fine manoeuvres to fly a multitude of low and high altitude orbits around the comet, mapping its shape and surface in detail never seen before, and has continued to observe it for a year since then. The Rosetta spacecraft is equipped with scientific instruments that deliver a wealth of new knowledge about the CG/67P comet, in addition to spectacular pictures. Delivering the Philae lander onto the surface of the comet 500 million km away from Earth was also a remarkable technological success. The direct measurements made by the Philae lander on the surface of the comet provided significant new knowledge. The first half of this paper gives a brief overview of the objectives and highlights of the Rosetta-Philae mission. In the second half the major hardware and software design aspects, including the conceptual design and implementation of the central on-board computer (CDMS) of the Philae lander are outlined. It focuses on the implementation of fault tolerance, autonomous operation and operational flexibility by means of specific linked data structures and code execution mechanisms that can be interpreted as a kind of object oriented model for mission sequencing.

Language extension enables integration of new language constructs without invasive changes to a base language (e. g., C). Such extensions help to build more reliable software by using proper domain-specific abstractions. Language workbenches significantly reduce the effort for building such extensible languages by synthesizing a fully-fledged IDE from language definitions. However, in contemporary tools, this synthesis does not include interactive debugging for programs written with the base language or its extensions. This paper describes a generic framework for extensible debuggers that enables debugging of the language extensions by defining mappings between the base language and the language extensions. The architecture is designed for extensibility, so debug support for future extensions can be contributed with little effort. We show an implementation of our approach for mbeddr, which is an extensible version of the C programming language. We also discuss the debugger implementation for non-trivial C extensions such as components. Finally, the paper discusses the extent to which the approach can be used with other base languages, debugger backends and language workbenches.

We have developed a novel method for static backward program slicing. The method works for well-structured programs, as commonly demanded by coding standards for safety-critical software. It utilises the program structure to obtain a highly efficient slicing process, where control dependencies are inferred from the program structure, and the slicing is done on-the-fly concurrently with the data dependence analysis.

We have evaluated our method experimentally. For applications that require few slices to be taken, like checking for a set of safety properties, we obtain large speedups as compared with the standard method for static backward program slicing. We have also investigated how the speedup varies with various parameters such as code size, size of the slice relative to the full program, and relative frequency of conditions in the code.

Verification and testing are two of the most costly and time consuming steps during the development of safety critical systems. The advent of complex and sometimes partially unpredictable computing architectures such as multicore commercial-of-the-shelf platforms, together with the composable development approach adopted in multiple industrial domains such as avionics and automotive, rendered the exhaustive testing of all situations that could potentially be encountered by the system once deployed on the field nearly impossible. Run-time verification (RV) is a promising solution to help accelerate the development of safety critical applications whilst maintaining the high degree of reliability required by such systems. RV adds monitors in the application, which check at run-time if the system is behaving according to predefined specifications. In case of deviations from the specifications during the runtime, safeguarding measures can be triggered in order to keep the system and its environment in a safe state, as well as potentially attempting to recover from the fault that caused the misbehaviour. Most of the state-of-the-art on RV essentially focused on the monitor generation, concentrating on the expressiveness of the specification language and its translation in correct-by-construction monitors. Few of them addressed the problem of designing an efficient and safe run-time monitoring (RM) architecture. Yet, RM is a key component for RV. The RM layer gathers information from the monitored application and transmits it to the monitors. Therefore, without an efficient and safe RM architecture, the whole RV system becomes useless, as its inputs and hence by extension its outputs cannot be trusted. In this paper, we discuss the design of a novel RM architecture suited to safety critical applications.

This paper discusses the schedulability analysis of a Pulse-Width Modulation (PWM) control algorithm of an on-board spacecraft software system. The UPMSat-2 case study is used to discuss the scheduling approach of the task set of the Attitude Determination and Control System (ADCS). The Ravenscar profile is a key element of the project in order to ensure temporal predictatibilty and analysability. However, the task population must be maintained low as available computational resources are limited. As a result, the PWM task has not a single activation point, which prevents a traditional schedulability analysis. The approach used by the authors to carry out the scheduling analysis is presented in the paper.

Ensuring the correct timing behavior of the control software of a spacecraft is a complex endeavor. This paper describes the real-time aspects of the Intermediate eXperimental Vehicle’s (IXV) On-Board Software (OBSW), including the schedulability analysis performed for the validation of this safety-critical, hard real-time system of the European Space Agency (ESA). We then give details of how the Ravenscar profile has been used to obtain predictability over RTEMS, and quantify the overhead of different mechanisms for measuring computation times. We provide the timing measurements of each task during the different modes of the mission, including the Guidance, Navigation, and Control (GNC) tasks, to aid in the development of future OBSW projects.

Open-source middleware started to be used several years ago for the development of complex applications. When these applications were developed, no real data were available about how maintenance activities could be affected over time. This is especially important for critical applications expected to be maintained over several years. This paper presents maintenance experiences with applications using open-source middleware (TAO and JacORB). These applications are developed using a component model for real-time applications implemented on top of the middleware. Improvements for software reliability have been detected during this time. We present them and how they can be applied to applications using TAO.

The development of high-integrity real-time systems, including their certification, is a demanding endeavour in terms of time, skills and effort involved. This is particularly true in application domains such as the avionics, where composable design is to be had to allow subdividing monolithic systems into components of smaller complexity, to be outsourced to developers subcontracted down the supply chain. Moreover, the increasing demand for computational power and the consequent interest in multicore HW architectures complicates system deployment. For these reasons, appropriate methodologies and tools need to be devised to help the industrial stakeholders master the overall system design complexity, while keeping manufacturing costs affordable. In this paper we present some elements of the CONCERTO platform, a toolset to support the end-to-end system development process from system modelling to analysis and validation, prior to code generation and deployment. The approach taken by CONCERTO is demonstrated for an illustrative avionics setup, however it is general enough to be applied to a number of industrial domains including the space, telecom and automotive. We finally reason about the benefits to an industrial user by comparing to similar initiatives in the research landscape.

The verification of distributed real-time systems designed by architectural languages such as AADL (Architecture Analysis and Design Language) is a research challenge. These systems are often used in safety-critical domains where one mistake can result in physical damages and even life loss. In such domains, formal methods are a suitable solution for rigorous analysis. This paper studies the formal verification of distributed real-time systems modelled with AADL. We transform AADL model to another specification formalism enabling the verification. We choose LNT language which is an input to CADP toolbox for formal analysis. Then, we illustrate our approach with the "Flight Control System" case study.

A safety case contains safety arguments together with supporting evidence that together should demonstrate that a system is acceptably safe. System changes pose a challenge to the soundness and cogency of the safety case argument. Maintaining safety arguments is a painstaking process because it requires performing a change impact analysis through interdependent elements. Changes are often performed years after the deployment of a system making it harder for safety case developers to know which parts of the argument are affected. Contracts have been proposed as a means for helping to manage changes. There has been significant work that discusses how to represent and to use them but there has been little on how to derive them. In this paper, we propose a sensitivity analysis approach to derive contracts from Fault Tree Analyses and use them to trace changes in the safety argument, thus facilitating easier maintenance of the safety argument.

The transition to multicore systems that has started to take place over the last few years, has revived the interest in the synchronization protocols for sharing logical resources. In fact, consolidated solutions for single processor systems are not immediately applicable to multiprocessor platforms and new paradigms and solutions have to be devised. The Multiprocessor resource sharing Protocol (MrsP) is a particularly elegant approach for partitioned systems, which allows sharing global logical resources among tasks assigned to distinct scheduling partitions. Notably, MrsP enjoys two desirable theoretical properties: optimality and compliance to well-known uniprocessor response time analysis. A coarse-grained experimental evaluation of the MrsP protocol on a general-purpose operating system has been already presented by its original authors. No clear evidence, however, has been provided to date as to its viability and effectiveness for industrial-size real-time operating systems. In this paper we bridge this gap, focusing on the challenges posed by the implementation of MrsP on top of two representative real-time operating systems, RTEMS and LITMUS\(^{RT}\). In doing so, we provide a useful insight on implementation-specific issues and offer evidence that the protocol can be effectively implemented on top of standard real-time operating system support while incurring acceptable overhead.

This paper extends the authors earlier proposal for providing Ada with support for fine-grained parallelism with an execution model based on the concept of abstract executors, detailing the progress guarantees that these executors must provide and how these can be assured even in the presence of potentially blocking operations. The paper also describes how this execution model can be applied to real-time systems.

AFDX (Avionics Full Duplex Switched Ethernet) is a standard communication network for avionics based on Ethernet links and special-purpose switches. This paper proposes an AFDX emulator based on standard Ethernet hardware (cards and switches) to build a low cost AFDX network for training or basic research purposes. We also propose the integration of the emulator within an ARINC-653 platform to allow the development of real-time Ada applications. Finally, a performance evaluation has been done in order to show the usability of the emulator.