Search

International audience; Formal methods have become a recommended practice in safety-critical software engineering. To be formally verified, a system should be specified with a specific formalism such as Petri nets, automata and process algebras, which requires a formal expertise and may become complex especially with large systems. In this paper, we report our experience in the formal verification of safety-critical real-time systems. We propose a formal mapping for a real-time task model using the LNT language, and we describe how it is used for the integration of a formal verification phase in an AADL model-based development process. We focus on real-time systems with event-driven tasks, asynchronous communication and preemptive fixed-priority scheduling. We provide a complete tool-chain for the automatic model transformation and formal verification of AADL models. Experimentation illustrates our results with the Flight control system and Line follower robot case studies.

This article deals with the design exploration and verification of real-time critical systems. Assigning the functions to the tasks of the target real-time operating system is a part of the design process. Finding a suitable design involves many important design decisions that have a strong impact on the system quality criteria. However, with the increasing complexity and scale of today’s systems and the large number of possible design solutions, making design decisions while balancing conflicting quality criteria becomes error-prone and unmanageable for designers. We propose an automated method using a multi-objective evolutionary algorithm guided by an architectural clustering technique. This method allows designers to search the design space for schedulable solutions with respect to multiple competing performance criteria. To assess our method, several evaluations were performed. One of them shows that we were able to produce the exact optimal solution sets for $$55\%$$ of the studied problem instances.

AADL (Architecture Analysis & Design Language) is a modelling language enabling the design of embedded real-time systems. This language has proven its power in several domains like aeronautics and space. The AADL core language describe both software and hardware components and it can be extensible by properties to provide information about these components or annexes to enable a designer to extend and customize the AADL core specification with other concepts specified in a language other than AADL. In particular, the AADL Error Model Annex (EMA) was proposed to model such requirements separately from the core model since dependability requirements is of major importance in real-time embedded systems. This annex can not only model different kinds of errors but also error propagation, error detection and error recovery. In this paper, we ensure a comparative study of existing tools and compilers of the AADL language and its error model annex. We present, then, our work aiming at integrating a new compiler of the EMA annex into the Ocarina tool suite to support dependability requirements.

The analysis of real-time systems designed by architectural languages such as architecture analysis and design language (AADL) is a challenging research topic. In such a context, formal methods become an advocated practice in software engineering for rigorous analysis. Yet, they are applied on specific formalisms to be analysed on dedicated tools. This paper studies the formal verification of real-time systems modelled with the AADL language and its behaviour annex. We define a formal semantics of an AADL behavioural subset using the LNT language. This work is illustrated with a robot case study.

Fault tolerance, one of the means of dependability, is defined as the capability of a system to continue providing offered services even in the presence of errors. Modelling fault tolerant systems is becoming a serious challenge due to emerging requirements suh as dynamism, distribution and system evolution. In this context, AADL is extended by the Error Model Annex to design architectural error model even for critical systems for analysis and assessment purposes. In this paper, we define a model driven approach to generate fault tolerant application code using aspect oriented programming. First, we integrate fault tolerance elements since the modelling step of a system using AADL and its annex Error Model Annex. Second, we define a set of transformation rules from the EMA annex to the AO4AADL annex, an extension of the AADL language by architectural aspects. The model transformation is generic and not specific to a language. AO4AADL is transformed into aspect code using the same target language as the functional code. Therefore, we ensure separation of concerns at the model level as well as the application level. To validate our approach, we apply it to an infant incubator system.

Aspect-Oriented Programming (AOP) supports the separation of concerns cutting across the implementation of a software application in order to avoid scattering and tangling. We focus on the integration of this paradigm into the development of real-time systems. AOP is based on the weaving process to automatically integrate separately-created segments of code (specified by aspects), into the application by replacing them in the final implementation code. In the context of real-time systems, this can harm determinism by including constructs that may violate real-time constraints beyond the control of the developer such as dynamic allocation. We both studied and tested the AspectAda language, an existing aspect mechanism, in order to adapt its implementation to respect real-time constraints. We studied this language's grammar, runtime and especially weaving operation. In this paper, we briefly discuss both the limitations of the existing language and the proposed solutions. Then, we present a new architecture of the compiler/weaver to overcome the problems of the existing one and we detail the implementation of its different parts based on tree manipulation. Finally, we illustrate our contribution using a case study.

International audience; Real-time embedded systems may be composed of a large number of time constrained functions. When such systems are implemented on top of multitasks real-time operating systems (RTOS), the functions have to be assigned to tasks of the target RTOS. This is a challenging work due to the large number of valid candidate functions to tasks assignment solutions. Moreover, the impact of the assignment on the system performance criteria (often conflicting) should be taken intoaccount in the architecture exploration. The automation of the software design exploration by the use of metaheuristics such as multi-objective evolutionary algorithm (MOEA) is a suitable way to help the designers. Indeed, MOEAs approximate near optimal alternatives at a reasonable time when compared to an exhaustive and exact search method. However, for large scale systems (i.e having a huge number of functions) even a MOEA method is impractical due to the increased time required to solve a problem instance. This may raise a threat to the scalability of the software design exploration method. To tackle this problem, we present in this article a parallel implementation of the Pareto Archived Evolution Strategy (PAES) algorithm used as a MOEA for the software design exploration. The proposed parallelization method is based on the well-known master-slave paradigm. Additionally, it involves a new selection scheme in the PAES algorithm. Results of experimentations provide evidence that, on one hand, the parallel approach can considerably speed up the design exploration and the optimization processes. On the other hand, the proposed selection strategy improves the quality of obtained solutions as compared to the original PAES selection schema.

The implementation of hard real-time systems is an extremely tedious task today due to safety and dynamic reconfiguration requirements. For that, whatever the taken precautions, the occurrence of faults in such systems is sometimes unavoidable. So, developers have to take into account the presence of faults since the design level. In this context, we notice the need of techniques ensuring the dependability of real-time distributed dynamically reconfigurable systems. We focus on fault-tolerance, that means avoiding service failures in the presence of faults. In this paper, we have defined a development process for modelling and generating fault tolerance code for real-time systems using aspect-oriented programming. First, we integrate fault tolerance elements since the modelling step of a system in order to take advantage of features of analysis, proof and verification possible at this stage using AADL and its annex error model annex. Second, we extend an aspect-oriented language and adapt it to comply with real-time requirements. Finally, we define a code generation process for both functional preoccupations and cross-cutting ones like fault tolerance and we propose an extension of an existent middleware. To validate our contribution, we use AADL and its annexes to design a landing gear system as an embedded distributed one.

11 pp; International audience; This article deals with real-time embedded system design and verification. Real-time embedded systems are frequentlydesigned according to multi-tasking architectures that have timing constraints to meet. The design of real-time embeddedsystems expressed as a set of tasks raises a major challenge since designers have to decide how functions of the system mustbe assigned to tasks. Assigning each function to a different task will result in a high number of tasks, and then in higherpreemption overhead. In contrast, mapping many functions on a limited number of tasks leads to a less flexible design whichis more expensive to change when the functions of the system evolve. This article presents a method based on an optimizationtechnique to investigate the assignment of functions to tasks. We propose a multi-objective evolution strategy formulation whichboth minimizes the number of preemptions and maximizes task laxities. Our method allows designers to explore the search spaceof all possible function to task assignments and to find good tradeoffs between the two optimization objectives among schedulablesolutions. After explaining our mapping approach, we present a set of experiments which demonstrates its effectiveness fordifferent system sizes.

The development of computer systems is extremely complex due to real-time, distribution and dynamism requirements. For this reason, whatever the taken precautions, the occurrence of faults is sometimes unavoidable. In this context, we notice the need of techniques ensuring the dependability of realtime distributed dynamically reconfigurable systems. We focus on fault-tolerance, that means avoiding service failures in the presence of faults. In this paper, we have defined a development process for modeling and generating fault tolerance code using aspect oriented programming. First, we integrate fault tolerance elements since the modeling step of a system in order to take advantage of features of analysis, proof and verification possible at this stage using AADL and its annex Error Model Annex. Second, we extend an aspect oriented language and adapt it to respect real-time requirements. Finally, we define a code generation process for both functional preoccupations and crosscutting ones like fault tolerance.

International audience

In this paper, we propose a framework allowing the modeling and verification of reconfigurable Distributed Real-time Embedded (DRE) systems. In fact, as reconfiguration significantly complicates system design and execution, many non-functional properties and constraints cannot be easily preserved. Verifying the continuous satisfaction of non-functional properties should be thus accomplished after applying reconfiguration actions. For this purpose, we develop an integrated model-based development approach allowing modeling and verification of reconfigurable DRE systems.

In this paper, we propose a methodology to design Distributed Real-time Embedded (DRE) systems and particularly reconfigurable ones. Due to the complexity of the development of these systems and their hard temporal and resource constraints, a development process is required to make easier the construction of these systems. For this, we propose an MDE-based approach which offers a development process from model to code.

An embedded software system is reconfigurable when it can modify its behavior or its architecture. The reconfigurations are launched according to the evolution of context requirements and the variation of execution environment constraints. The constant growth of the complexity in embedded systems makes the reconfiguration more important and more difficult to achieve. The challenges concern as much the design model level as the runtime support level. Here we focus our attention on design model level. In our work, we aim at providing an automated development process from model to implementation for the dynamic software part of these systems. The contributions of this paper are twofold. First, we use the notion of structure to capture configurations instead of defining each of them. Second, we propose a set of tools to be used in a model driven approach to specify and configure reconfigurable software architectures of distributed real time embedded (DRE) systems.

Building middleware for distributed applications is a complex task, mixing antagonistic concerns: heterogeneity, performance, reliability, quality of services. Optimization and fine-tuning of middleware for a particular application is even a harder task, usually done manually or through complex design patterns. The advent of "schizophrenic" middleware which separates concerns between distribution model, communication protocols, and their implementation by refining the definition and role of "personalities" brought some elements to solve this problem by enabling full tailoring of the middleware by the developer. In this paper we extend this approach to full automation by generating middleware from an architectural model of the system expressed in a modeling language. This enables precise tuning and configuration of the middleware by generating exactly the required code, prior to runtime. We finally show how this approach fits the requirements of high-integrity or real-time distributed systems.