nach oben

2018 | Buch

Kapitel lesen Erstes Kapitel lesen

Reliable Software Technologies – Ada-Europe 2018

23rd Ada-Europe International Conference on Reliable Software Technologies, Lisbon, Portugal, June 18-22, 2018, Proceedings

herausgegeben von: António Casimiro, Pedro M. Ferreira

Verlag: Springer International Publishing

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

This book constitutes the proceedings of the 23rd Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2018, held in Lisbon, Portugal, in June 2018.

The 10 papers presented in this volume were carefully reviewed and selected from 27 submissions. They were organized in topical sections named: safety and security; Ada 202X; handling implicit overhead; real-time scheduling; and new application domains.

Inhaltsverzeichnis

Frontmatter

Safety and Security

Frontmatter

Using Safety Contracts to Verify Design Assumptions During Runtime

Abstract

A safety case comprises evidence and argument justifying how each item of evidence supports claims about safety assurance. Supporting claims by untrustworthy or inappropriate evidence can lead to a false assurance regarding the safe performance of a system. Having sufficient confidence in safety evidence is essential to avoid any unanticipated surprise during operational phase. Sometimes, however, it is impractical to wait for high quality evidence from a system’s operational life, where developers have no choice but to rely on evidence with some uncertainty (e.g., using a generic failure rate measure from a handbook to support a claim about the reliability of a component). Runtime monitoring can reveal insightful information, which can help to verify whether the preliminary confidence was over- or underestimated. In this paper, we propose a technique which uses runtime monitoring in a novel way to detect the divergence between the failure rates (which were used in the safety analyses) and the observed failure rates in the operational life. The technique utilises safety contracts to provide prescriptive data for what should be monitored, and what parts of the safety argument should be revisited to maintain system safety when a divergence is detected. We demonstrate the technique in the context of Automated Guided Vehicles (AGVs).

Omar Jaradat, Sasikumar Punnekkat

Tool-Supported Safety-Relevant Component Reuse: From Specification to Argumentation

Abstract

Contracts are envisaged to support compositional verification of a system as well as reuse and independent development of their implementations. But reuse of safety-relevant components in safety-critical systems needs to cover more than just the implementations. As many safety-relevant artefacts related to the component as possible should be reused together with the implementation to assist the integrator in assuring that the system they are developing is acceptably safe. Furthermore, the reused assurance information related to the contracts should be structured clearly to communicate the confidence in the component. In this work we present a tool-supported methodology for contract-driven assurance and reuse. We define the variability on the contract level in the scope of a trace-based approach to contract-based design. With awareness of the hierarchical nature of systems subject to compositional verification, we propose assurance patterns for arguing confidence in satisfaction of requirements and contracts. We present an implementation extending the AMASS platform to support automated instantiation of the proposed patterns, and evaluate its adequacy for assurance and reuse in a real-world case study.

Irfan Sljivo, Barbara Gallina, Jan Carlson, Hans Hansson, Stefano Puri

Ada 202X

Frontmatter

Safe Dynamic Memory Management in Ada and SPARK

Abstract

Handling memory in a correct and efficient way is a step toward safer, less complex, and higher performing software-intensive systems. However, languages used for critical software development such as Ada, which supports formal verification with its SPARK subset, face challenges regarding any use of pointers due to potential pointer aliasing. In this work, we introduce an extension to the Ada language, and to its SPARK subset, to provide pointer types (“access types” in Ada) that provide provably safe, automatic storage management without any asynchronous garbage collection, and without explicit deallocation by the user. Because the mechanism for these safe pointers relies on strict control of aliasing, it can be used in the SPARK subset for formal verification, including both information flow analysis and proof of safety and correctness properties. In this paper, we present this proposal (which has been submitted for inclusion in the next version of Ada), and explain how we are able to incorporate these pointers into formal analyses.

Maroua Maalej, Tucker Taft, Yannick Moy

Safe Non-blocking Synchronization in Ada2x

Abstract

The mutual-exclusion property of locks stands in the way to scalability of parallel programs on many-core architectures. Locks do not allow progress guarantees, because a task may fail inside a critical section and keep holding a lock that blocks other tasks from accessing shared data. With non-blocking synchronization, the drawbacks of locks are avoided by synchronizing access to shared data by atomic read-modify-write operations.

To incorporate non-blocking synchronization in Ada 202x, programmers must be able to reason about the behavior and performance of tasks in the absence of protected objects and rendezvous. We therefore extend Ada’s memory model by synchronized types, which support the expression of memory ordering operations at a sufficient level of detail. To mitigate the complexity associated with non-blocking synchronization, we propose concurrent objects as a novel high-level language construct. Entities of a concurrent object execute in parallel, due to a fine-grained, optimistic synchronization mechanism. Synchronization is framed by the semantics of concurrent entry execution. The programmer is only required to label shared data accesses in the code of concurrent entries. Labels constitute memory-ordering operations expressed through aspects and attributes. To the best of our knowledge, this is the first approach to provide a non-blocking synchronization construct as a first-class citizen of a high-level programming language. We illustrate the use of concurrent objects by several examples.

Johann Blieberger, Bernd Burgstaller

Handling Implicit Overhead

Frontmatter

On the Effect of Protected Entry Servicing Policies on the Response Time of Ada Tasks

Abstract

Real-time multiprocessor systems are being used extensively in industrial applications. Ada provides ample support for such systems, including a complete tasking model providing time predictability, especially when restricted by the Ravenscar profile. A fundamental element of this tasking model is inter-task communication by means of protected objects. The definition of resource locking policies with bounded priority inversion is a fundamental aspect of protected objects, which has received considerable attention, with some interesting results that can be used in multiprocessor real-time systems. However, there is another important subject, the service policy for protected entries, that has received less attention in the research community and is also important in order to guarantee a predictable time behaviour. The impact of the service model on the response time analysis of multiprocessor real-time systems is evaluated in the paper for the self-service model and the proxy model, and their relation to the MSRP and the MrsP locking policies is discussed. Extensions to response time analysis for the proxy model with both locking policies are also contributed.

Jorge Garrido, Juan Zamorano, Alejandro Alonso, Juan A. de la Puente

Improved Cache-Related Preemption Delay Estimation for Fixed Preemption Point Scheduling

Abstract

Cache-Related Preemption Delays (CRPD) can significantly increase tasks’ execution time in preemptive real-time scheduling, potentially jeopardising the system schedulability. In order to reduce the cumulative CRPD, Limited Preemptive Scheduling (LPS) has emerged as a scheduling approach which limits the maximum number of preemptions encountered by real-time tasks, thus decreasing CRPD compared to fully preemptive scheduling. Furthermore, an instance of LPS, called Fixed Preemption Point Scheduling (LP-FPP), defines the exact points where the preemptions are permitted within a task, which enables a more precise CRPD estimation. The majority of the research, in the domain of LP-FPP, estimates CRPD with pessimistic upper bounds, without considering the possible sources of over-approximation: (1) accounting for the infeasible preemption combinations, and (2) accounting for the infeasible cache block reloads. In this paper, we improve the analysis by accounting for those two cases towards a more precise estimation of the CRPD upper bounds. The evaluation of the approach on synthetic tasksets reveals a significant reduction of the pessimism in the calculation of the CRPD upper bounds, compared to the existing approaches.

Filip Marković, Jan Carlson, Radu Dobrin

Real-Time Scheduling

Frontmatter

Combined Scheduling of Time-Triggered and Priority-Based Task Sets in Ravenscar

Abstract

Time-triggered and priority-based are the two major approaches for scheduling real-time systems. Both have their own advantages and drawbacks and none is superior in the general case. While time-triggered schedules excel at determinism and jitter control, they are hard to design and lack flexibility. Priority-based scheduling, on the other hand, keeps the logical and timing aspects of real-time applications conveniently separated from each other, at the cost of indeterminism and larger input and output jitter for all but the highest-priority tasks.

In a previous paper, we presented a model and a related Ada implementation to support the combined execution of time-triggered and priority-based task sets, aiming to obtain the best of both worlds. This paper presents continuation of that work in two directions. One is the extension of the original model to support more behavioural patterns; the other is providing a Ravenscar implementation, targeting high-integrity systems. We conclude that Ravenscar is expressive enough to support most of the patterns in the original full-Ada version, and those that require forbidden features (such as dynamic priorities) are not out of reach if the time-triggered scheduler is implemented at the runtime level.

Jorge Real, Sergio Sáez, Alfons Crespo

Theory and Practice of EDF Scheduling in Distributed Real-Time Systems

Abstract

The behavior of EDF schedulers has been very extensively studied for single-processor systems and there is also a lot of work on scheduling and schedulability analysis techniques dealing with EDF in homogeneous multiprocessor systems. However, if distributed systems are considered, only a small number of schedulability analysis techniques are available and there is only a little information on practical experience with this kind of systems. For distributed systems where a clock synchronization mechanism is not available, a recent work has theoretically shown how a feasible deadline assignment can significantly increase the utilization of processing resources while keeping the system schedulable (i.e., meeting all the timing requirements). On the other hand, Ada provides support for building applications scheduled by EDF. This paper proposes a set of experiments to contrast the theoretical results on scheduling deadline assignment in a distributed real-time application against those obtained through its real execution.

J. Javier Gutiérrez, Héctor Pérez

New Application Domains

Frontmatter

Safe Parallelism: Compiler Analysis Techniques for Ada and OpenMP

Abstract

There is a growing need to support parallel computation in Ada to cope with the performance requirements of the most advanced functionalities of safety-critical systems. In that regard, the use of parallel programming models is paramount to exploit the benefits of parallelism.

Recent works motivate the use of OpenMP for being a de facto standard in high-performance computing for programming shared memory architectures. These works address two important aspects towards the introduction of OpenMP in Ada: the compatibility of the OpenMP syntax with the Ada language, and the interoperability of the OpenMP and the Ada runtimes, demonstrating that OpenMP complements and supports the structured parallelism approach of the tasklet model.

This paper addresses a third fundamental aspect: functional safety from a compiler perspective. Particularly, it focuses on race conditions and considers the fine-grain and unstructured capabilities of OpenMP. Hereof, this paper presents a new compiler analysis technique that: (1) identifies potential race conditions in parallel Ada programs based on OpenMP or Ada tasks or both, and (2) provides solutions for the detected races.

Sara Royuela, Xavier Martorell, Eduardo Quiñones, Luis Miguel Pinho

Microservice-Based Agile Architectures: An Opportunity for Specialized Niche Technologies

Abstract

This work discusses lessons learned from the development of a medium-size peer-to-peer distributed software system centered around asynchronous computation and message-/stream-oriented communication. Albeit foreign to traditional high-integrity systems, these architectural characteristics are making rapid headway into large-scale mission-critical and business-critical software infrastructures, thus becoming candidate solutions for the design of reliable systems. We wanted our software architecture to be agile, that is, versatile, easy to evolve and modify, and resilient enough not to degrade across changes. To meet this goal, we adopted the microservices style, which afforded us the choice of best-of-breed technology to implement the individual system parts. Embracing heterogeneity while seeking agility however challenged our ability to design effective solutions for component coordination and interaction, as well as the goodness of fit of the used technologies for system integration and testing. Reflecting on our experience, we distill the lessons we learned in terms of architectural patterns, highlighting the pros and cons we saw in the microservices style and in our technologies selection.

Stefano Munari, Sebastiano Valle, Tullio Vardanega

Backmatter

Titel: Reliable Software Technologies – Ada-Europe 2018
herausgegeben von: António Casimiro
Pedro M. Ferreira
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-92432-8
Print ISBN: 978-3-319-92431-1
DOI: https://doi.org/10.1007/978-3-319-92432-8