Reliable Software Technologies – Ada-Europe 2009

This paper discusses the requirements on the selection of a programming language as the target of automated code generation in a high-integrity model driven engineering environment. We show that the dominant point of view for this selection becomes that of the designer of the model-to-code transformation engine. We then illustrate the application of the proposed requirements on a simple example.

High-integrity computer systems are usually required to go through a strict verification and validation process, often leading to certification according to some safety or security standard. Verification activities may include some kind of static analysis because some types of errors cannot be removed just with testing. Temporal analysis techniques are available for systems with hard real-time requirements, but they are limited to systems complying with a well-defined computational model and with a restricted semantics that ensures a predictable temporal behaviour. The Ravenscar profile implements such a model for Ada programs running on single processor platforms, but it cannot be used in distributed high-integrity real-time systems, which are becoming more and more common. This papers discusses the feasibility of designing a real-time middleware for distributed high-integrity Ada programs with an statically analysable behaviour, and the necessary language restrictions that should be used in order to enable the required predictability and timeliness properties.

Design and validation of safety-critical systems are crucial because faults or security issues could have significant impacts (loss of life, mission failure, etc.). Each year, millions of dollars are lost due to these kinds of issues. Consequently, safety and security requirements must be enforced. Systems must be validated against these requirements to improve safety and security and to make them more reliable and robust. We present our approach to avoid such issues by modeling safe and secure systems with both safety and security requirements. We rely on a modeling language (AADL) to model and design partitioned systems with their requirements and constraints. We then validate these models to ensure security and safety enforcement. We also discuss how this approach can be used to automatically generate and build safe and secure partitioned systems.

Various test case selection criteria have been proposed for quality testing of software. It is a common phenomenon that test sets satisfying different criteria have different sizes and fault-detecting ability. Moreover, test sets that satisfy a stronger criterion and detect more faults usually consist of more test cases. A question that often puzzles software testing professionals and researchers is: when a testing criterion C1 helps to detect more faults than another criterion C2, is it because C1 specifically requires test cases that are more fault-sensitive than those for C2, or is it essentially because C1 requires more test cases than C2? In this paper, we discuss several methods and approaches for investigating this question, and empirically compare several common coverage criteria for testing logical decisions, taking into consideration the different sizes of the test sets required by these criteria. Our results demonstrate evidently that the stronger criteria under study are more fault-sensitive than the weaker ones, not solely because the former require more test cases. More importantly, we have illustrated a general approach, which takes into account the size factor of the generated test sets, for demonstrating the superiority of a testing criterion over another.

Ada has proved to be one of the best languages to learn computer programming. Nevertheless, learning to program is difficult and when it is combined with lack of motivation by the students, dropout rates can reach up to 70%. In order to face up to this problem, we have developed a first-year course for computing majors on programming based on two key ideas: supplementing the final exam with a series of activities in a continuous evaluation context; and making those activities more appealing to the students. In particular, some of the activities are designed as on-line Ada programming competitions; they are carried out by using a web-based automatic evaluation system, the on-line judge. Human instructors remain essential to assess the quality of the code. To ensure the authorship of the programs, a source-code plagiarism detection environment is used. Experimental results show the effectiveness of the proposed approach. The dropout rate decreased from 61% in the autumn semester 2007 to 48% in the autumn semester 2008.

With the development of embedded and mobile systems, Java is being widely used for application programs and is also considered for implementing systems kernel or application platforms. It is the aim of this paper to exemplify some subtle programming errors that may result from the process queuing and awaking policy, which corresponds to a weak fairness semantic and which has been chosen for implementing the monitor concept in this language. Two examples show some subtle deadlocks resulting from this policy. The first example deals with process synchronization: processes seeking after partners for a peer-to-peer communication call a symmetrical rendezvous server. The second example concerns resource sharing according to a solution of the dining philosophers paradigm. In this example, several implementations are presented, the last ones aiming to provide deterministic process awakening. All these examples have been validated and simulated and this allows comparing their concurrency complexity and effectiveness. Our conclusion is, first, that the use of Java for multithreading programming necessitates sometimes additional shielding code for developing correct programs and, second, that a good acquaintance with several styles of concurrent programming helps designing more robust Java solutions, once the choice of the implementation language is irrevocable.

The Ada 2005 task dispatching model includes new scheduling policies such as EDF and round robin, in addition to the traditional fixed priority dispatching, and allows mixing these policies into a hierarchy of schedulers. This hierarchical scheduling model is a very interesting solution that allows us to have in the same system the best properties of the three policies: the high performance of EDF, the predictability of fixed priorities, and the fair distribution of unused capacity provided by a round robin scheduler. The paper presents one of the first implementations of this hierarchical dispatching model, built with GNAT over MaRTE OS. An evaluation of the implementation is provided and examples of usage are shown.

Earliest Deadline First (EDF) and Fixed Priority (FP) scheduling represent the two main dispatching policies within the research domain of real-time systems engineering. Both dispatching policies are now supported by Ada. In this paper the two approaches are combined to maximize the advantages of both schemes. From EDF comes efficiency, from FP predictability. A system model is presented in which a relatively small number of high-integrity tasks are scheduled by FP, with the rest of the tasks being handled via an EDF domain of lower priority. Two aspects of integration are covered in this paper. Firstly, Response-Time Analysis (for FP) and Processor-Demand Analysis (for EDF) are brought together to provide a single analysis framework. Secondly, the programming of systems which combine FP and EDF is addressed within the facilities provided by Ada 2005. Both partitioned and dynamic schemes are covered.

Tightness in WCET estimation is highly desirable for an efficient utilisation of resources. In order to obtain accurate WCET values, more program execution-history must be accounted for. In this paper we propose the use of Predicated WCET Analysis with constraint logic-programming to model context sensitive execution-times of program segments.

Our method achieves considerable tightness in comparison to traditional calculation methods that exceeded 20% in some cases during evaluation. Computing the WCET of programs modeled using our approach reveals a great ease of expressing execution-time dependencies and manageable WCET-calculation time-complexity.

Reactive systems are complex systems which behavior can be adequately modeled using the statechart formalism. The UML standard enriches this formalism with object-oriented concepts. However, manual transformation of these expressive models to object-oriented languages is an error-prone process. Model-Driven Engineering approach advocates for an automatic process to translate models into high-level programing languages. This work deals with the conversion of UML State Machines models into Ada 2005 code and the challenges that arise in this process.

We describe the tool supported approach we developed for real-time systems modelling and schedulability analysis performed at the architecting phase of the software lifecycle. This approach integrates the “Pipelines of Processes in Object Oriented Architectures” (or PPOOA for short) method and tool for architecting real-time systems using UML notation, with the Cheddar tool for simulation and schedulability analysis of real-time software intensive systems. PPOOA and Cheddar were developed independently, so we have to adapt PPOOA, the method and tool we had developed, to be integrated with the Cheddar tool developed by the University of Brest. The goal of the paper is to show how this approach can be applied seamlessly to the architecting of small and medium real-time systems, identifying and solving concurrency problems at the architecture phase thus saving later testing and debugging efforts. An illustrative example of modelling and evaluation of an elevator control system is presented.

The concept of formal metamodel will contribute significantly to the core principles of the OMG Model Driven Architecture (MDA). The OMG standard for metamodeling is the Meta Object Facility (MOF) meta-metamodel that defines a common way for capturing the diversity of modeling standards and interchange constructs that are used in MDA. A combination of UML (Unified Modeling Language), OCL (Object Constraint Language) and natural language is used to describe the abstract syntax and semantics of MOF. In this paper, we propose an algebraic formalization of MOF metamodels. We describe how to translate MOF metamodels into algebraic specifications. As an example, we describe a formalization of the core of the Query, View, Transformation (QVT) metamodel, the OMG standard for expressing transformations. The goal of this formalization is, on the one hand, to reason about ambiguity and consistency of metamodels and, on the other hand, to support tests and proofs in model transformations.

This paper presents translation schemas for some constructs of the Architecture Analysis & Design Language (AADL) in the formal language BIP(Behavior, Interaction, Priority). We focus here on deterministic data communications and show how BIP can support them. BIP provides a language and a theory for incremental composition of heterogeneous components. As a full-size exercise, we deal here with the modeling of immediate and delayed data communications supporting undersampling and oversampling of AADL.

We describe a formal verification toolchain for AADL, the SAE Architecture Analysis and Design Language, enriched with its behavioral annex. Our approach is based on tools that are integrated in the Topcased environment. We give a high-level view of the tools involved and illustrate the successive transformations that take place during the verification process.

We present a toolset for the behavioral verification and validation of architectural models of embedded systems expressed in the language AADL. The toolset provides simulation and timing analysis of AADL models. Underlying both tools is a process-algebraic implementation of AADL semantics. The common implementation of the semantics ensures consistency in the analysis results between the tools.

Developing safety-critical distributed applications is a difficult challenge. A failure may cause important damages as loss of human life or mission’s failure. Such distributed applications must be designed and built with rigor. Reducing the tedious and error-prone development steps is required; we claim that automatic code generation is a natural solution. In order to ease the process of verification and certification, the user can use modeling languages to describe application critical aspects. In this paper we introduce the use of AST as a modeling language for Distributed Real-time Embedded (DRE) systems. Then we present our tool-suite ocarina which allows automatic code generation from AST models. Finally, we present a comparison between ocarina and traditional approaches.

Systems designers have to cope with the ever growing complexity of nowadays systems. This issue becomes dramatic in the aeronautics domain, due to the huge number of functions the systems have to support, the significant number of sub-system elements required to implement these functions and their inter-connections. Although requirements engineering is a good answer to the issue of system specification, as it enables the definition of a contract specifying the constraints the system architecture has to take into account, it does not scale very well when the size and the complexity of the systems increase significantly. Model Driven Engineering (MDE) approaches are currently used by software engineers to enhance software quality and increase capitalization in product line delivery for complex systems, but are not yet widely used at the system architecture level. As such, there is still a big gap between the system engineering world and the software engineering world, that is particularly obvious in requirement processing, leading to misreadings and misinterpretations of the system requirements by software engineers, with important consequences at the software architecture level. In this paper, we propose an MDE approach to address this issue at the system architecture level, contributing to bridge the gap between system and software architectures. In particular, we will describe an approach to deal with the expression of requirements in a MDE context, which relies on the notion of system conceptual modeling.

An activity is described by a chronicle that expresses relationships between events in a sequence ordered in time. A chronicle language provides a syntax for the different chronicle operators considered. The recognition of chronicles is used in the processing of complex system simulations so as to detect activities or analyse behaviours. This work models formally the chronicle recognition, and coloured Petri nets (CPN) are used to model the recognition of a chronicle within a flow of events. The occurrence of an event to be detected is modelled by the firing of the corresponding transition. We provide coloured Petri nets to model the recognition of chronicles expressed with logical and temporal operators, as well as minimum and maximum time delays. We show how the composition of operators can be modelled by a composition of the coloured subnets associated with the different operators. The algebraic properties of the operators are reflected in the coloured nets. In this work, composition is achieved through place fusion, and a comprehensive modelling is provided, including more delicate issues such as chronicle with repetitions, and the absence of sub-chronicles.