nach oben

2016 | Buch

Kapitel lesen Erstes Kapitel lesen

Reliable Software Technologies – Ada-Europe 2016

21st Ada-Europe International Conference on Reliable Software Technologies, Pisa, Italy, June 13-17, 2016, Proceedings

herausgegeben von: Marko Bertogna, Luis Miguel Pinho, Eduardo Quiñones

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 refereed proceedings of the 21st Ada-Europe International Conference on Reliable Software Technologies, Ada-Europe 2016, held in Pisa, Italy, in June 2016.

The revised 12 full papers presented together with one invited paper were carefully reviewed and selected from 28 submissions. They are organized in topical sections on concurrency and parallelism, testing and verification, program correctness and robustness, and real-time systems.

Inhaltsverzeichnis

Frontmatter

Invited Paper

Frontmatter

Why the Expressive Power of Programming Languages Such as Ada Is Needed for Future Cyber Physical Systems

Abstract

If Cyber Physical Systems (CPS) are to be built with efficient resource utilisation it is imperative that they exploit the wealth of scheduling theory available. Many forms of real-time scheduling, and its associated analysis, are applicable to CPS, but it is not clear how the system developer/programmer can gain access to this theory when real CPS are being constructed. This short paper gives the background to the associated presentation where the facilities available in the Ada programming language are highlighted and reviewed. The aim of the presentation is to show that Ada provides most of the programming abstractions needed to deliver future CPS.

Alan Burns

Concurrency and Parallelism

Frontmatter

Modeling and Analysis of Data Flow Graphs Using the Digraph Real-Time Task Model

Abstract

Data flow graphs are widely used for modeling and analysis of real-time streaming applications in which having a predictable and reliable implementation is an essential requirement. In this paper, we consider scheduling a set of data flow graphs such that liveness and boundedness properties are guaranteed, which leads to a predictable and correct behavior of the application. A formal translation method is proposed to map a given set of data flow graphs to a set of graph-based real-time tasks. Additionally, sufficient conditions are derived under which the obtained task set provides a semantically correct implementation of the given data flow graphs. It is shown that the proposed approach provides a higher level of design flexibility compared to the existing methods which use a simpler, i.e. periodic, task model.

Morteza Mohaqeqi, Jakaria Abdullah, Wang Yi

Eliminating Data Race Warnings Using CSP

Abstract

Embedded systems commonly use state to synchronize concurrent programs. This state-based synchronization avoids serious errors like data races and can supersede other means of synchronization like locks and global disabling of interrupts. However, it makes reasoning difficult and static analysis tools struggle to comprehend it. In this paper we explain how we model C programs conservatively using static analysis and then use CSP refinement checkers to analyse synchronization. This paper demonstrates how this process aids program understanding and leads to the dismissal of data race warnings in industrial systems. We examine real-world synchronisation schemes and explain how and why they work.

Martin Wittiger

Real-Time Stream Processing in Java

Abstract

This paper presents a streaming data framework for the Real-Time Specification for Java, with the goal of levering as much as possible the Java 8 Stream processing framework whilst delivering bounded latency. Our approach is to buffer the incoming streaming data into micro batches which are then converted to collections for processing by the Java 8 infrastructure which is configured with a real-time ForkJoin thread pool. Deferrable servers are used to limit the impact of stream processing activity on hard real-time activities.

HaiTao Mei, Ian Gray, Andy Wellings

Testing and Verification

Frontmatter

Addressing the Regression Test Problem with Change Impact Analysis for Ada

Abstract

The regression test selection problem—selecting a subset of a test-suite given a change—has been studied widely over the past two decades. However, the problem has seen little attention when constrained to high-criticality developments and where a “safe” selection of tests need to be chosen. Further, no practical approaches have been presented for the programming language Ada. In this paper, we introduce an approach to solving the selection problem given a combination of both static and dynamic data for a program and a change-set. We present a change impact analysis for Ada that selects the safe set of tests that need to be re-executed to ensure no regressions. We have implemented the approach in the commercial, unit-testing tool VectorCAST, and validated it on a number of open-source examples. On an example of a fully-functioning Ada implementation of a DNS server (Ironsides), the experimental results show a 97% reduction in test-case execution.

Andrew V. Jones

Test Case Prioritization Using Online Fault Detection Information

Abstract

The rapid evolution of software necessitates effective fault detection within increasingly restricted execution times. To improve the effectiveness of the regression testing required for extensive fault detection, test cases have to be prioritized. The test cases with the higher chance of capturing faults are executed earlier in the series. This prioritization enables faster feedback for fixing more faults earlier. Various prioritization techniques have been proposed based on the information provided by offline (static) test execution history on previous versions of the software. In this paper, we propose a family of new test case prioritization techniques, which utilize online (dynamic) information about the locations of previously revealed faults in the detection of other faults. Our empirical studies demonstrate that the new techniques are more effective than the existing traditional test case prioritization techniques.

Mohsen Laali, Huai Liu, Margaret Hamilton, Maria Spichkova, Heinz W. Schmidt

An Experience in Ada Multicore Programming: Parallelisation of a Model Checking Engine

Abstract

Even if multicore architectures are nowadays extremely wide-spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine-tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.

Franco Mazzanti

Program Correctness and Robustness

Frontmatter

Lessons Learned in a Journey Toward Correct-by-Construction Model-Based Development

Abstract

This paper discusses lessons learned in the attempt to apply the long-known principles of correct-by-construction (CbyC) first promoted by Dijkstra, to modern model-based development practices. We recall the intent and scrutinize the outcomes of a string of research projects that focused explicitly on the pursuit of CbyC by means of model-driven methods and technologies. The lessons learned show that when CbyC extends from the algorithmic and functional dimension to extra-functional concerns, some of the strength of original CbyC concept and its pull dilute. One of the possible causes of that phenomenon, is that – in some situation – the assertive style of algorithm refinement gives way to more tentative exploration of an unknown solution space where the known truths are insufficient to steer the development.

Laura Baracchi, Silvia Mazzini, Stefano Puri, Tullio Vardanega

Extension of the Ocarina Tool Suite to Support Reliable Replication-Based Fault-Tolerance

Abstract

Replication is a reliability technique that involves redundancy of software or hardware components to guarantee availability for fault tolerance purposes. Several studies focused on modelling fault tolerance of real-time embedded systems using replication of AADL (Architecture Analysis & Design Language) components. Manual replication with AADL is a tedious task, error-prone and increases design time.

To support the automatic replication of AADL components, we propose in this paper an extension of the AADL Ocarina tool suite. For that, based on a set of transformation rules, we assist the designer to automatically generate standard AADL models enriched with variants and adjudicators. This is based on a three-step model driven approach. First, we enable the designer to model his or her core application using AADL. Second, the designer enriches the model with a property set that we defined to describe replication concepts. Finally, applying a set of transformation rules, we generate an intermediate AADL model enriched with different replicas using Ocarina. This generated model can be analysed, formally verified, used for application code generation or even replication of other components. To illustrate our approach, we apply an active replication to a robot system chosen as a case study.

Wafa Gabsi, Bechir Zalila, Mohamed Jmaiel

Kronecker Algebra for Static Analysis of Barriers in Ada

Abstract

Kronecker algebra until now has been applied to concurrent programs that use semaphores and protected objects for synchronization. Like many other programming languages, Ada uses barriers, too. In this paper, we present a new synchronization construct for barriers. By applying this, we are able to statically analyze Ada multi-tasking programs that employ barriers for synchronization issues. It turns out that we can use our existing Kronecker algebra implementation completely unmodified for concurrent program graphs using such barrier synchronization primitives.

Robert Mittermayr, Johann Blieberger

Real-Time Systems

Frontmatter

An Empirical Investigation of Eager and Lazy Preemption Approaches in Global Limited Preemptive Scheduling

Abstract

Global limited preemptive real-time scheduling in multiprocessor systems using Fixed Preemption Points (FPP) brings in an additional challenge with respect to the choice of the task to be preempted in order to maximize schedulability. Two principal choices with respect to the preemption approach exist (1) the scheduler waits for the lowest priority job to become preemptible, (2) the scheduler preempts the first job, among the lower priority ones, that becomes preemptible. We refer to the former as the Lazy Preemption Approach (LPA) and the latter as the Eager Preemption Approach (EPA). Each of these choice has a different effect on the actual number of preemptions in the schedule, that in turn determine the runtime overheads.

In this paper, we perform an empirical comparison of the run-time preemptive behavior of Global Preemptive Scheduling and Global Limited Preemptive Scheduling with EPA and LPA, under both Earliest Deadline First (EDF) and Fixed Priority Scheduling (FPS) paradigms. Our experiments reveal interesting observations some of which are counter-intuitive. We then analyse the counter-intuitive observations and identify the associated reasons. The observations presented facilitate the choice of appropriate strategies when using limited preemptive schedulers on multiprocessor systems.

Abhilash Thekkilakattil, Kaiqian Zhu, Yonggao Nie, Radu Dobrin, Sasikumar Punnekkat

The Polling Effect on the Schedulability of Distributed Real-Time Systems

Abstract

The usage of polling tasks continues to be quite common in today’s distributed real-time systems, despite the availability of event-driven software mechanisms and response time analysis techniques that can be applied to this kind of systems. This paper proposes a model for polling tasks that allows current response time analysis techniques for event-driven distributed systems to be applied, and it also studies the impact that polling has in the schedulability of a distributed system, using analytic results. A performance evaluation on an Ada-based platform is also provided. As expected, polling produces response times much higher than a pure event-driven alternative. The analysis techniques and the evaluation presented in the paper allows engineers to assess the negative effect of polling on the schedulability of distributed real-time systems.

Héctor Pérez, J. Javier Gutiérrez, Michael González Harbour, J. Carlos Palencia

Combining Time-Triggered Plans with Priority Scheduled Task Sets

Abstract

Time-triggered and concurrent priority-based scheduling are the two major approaches in use for real-time and embedded systems. Both approaches have their own advantages and drawbacks. On the one hand, priority-based systems facilitate separation of concerns between functional and timing requirements by relying on an underlying real-time operating system that takes all scheduling decisions at run time. But this is at the cost of indeterminism in the exact timing pattern of execution of activities, namely variable release jitter. On the other hand, time-triggered schedules are more intricate to design since all scheduling decisions must be taken beforehand in the design phase, but their advantage is determinism and more chances for minimisation of release jitter. In this paper we propose a software architecture that enables the combined and controlled execution of time-triggered plans and priority-scheduled tasks. We also describe the implementation of an Ada library supporting it. Our aim is to take advantage of the best of both approaches by providing jitter-controlled execution of time-triggered tasks (e.g., control tasks), coexisting with a set of priority-scheduled tasks, with less demanding jitter requirements.

Jorge Real, Sergio Sáez, Alfons Crespo

Backmatter

Titel: Reliable Software Technologies – Ada-Europe 2016
herausgegeben von: Marko Bertogna
Luis Miguel Pinho
Eduardo Quiñones
Verlag: Springer International Publishing
Electronic ISBN: 978-3-319-39083-3
Print ISBN: 978-3-319-39082-6
DOI: https://doi.org/10.1007/978-3-319-39083-3