Abstract. 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.
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.
Jose L. Fernandez and Gloria Marmol. Modelling and Evaluating Real-Time Software Architectures
Abstract. 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. 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.
Lei Pi, Jean-Paul Bodeveix and Mamoun FILALI-AMINE. Modeling AADL Data Communication with BIP
Abstract. This paper presents some translations schema between the Architecture Analysis & Design Language (AADL) and 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.
Francisco J. Montoya-Dato, Jose Luis Fernández-Alemán and Ginés García-Mateos. An Experience on Ada Programming Using On-line Judging
Abstract. 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 to 48%.
Man Fai Lau and Yuen Tak Yu. On Comparing Testing Criteria for Logical Decisions
Abstract. 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.
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.
Abstract. This paper presents the requirements for the selection of a programming language 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.
Mario Aldea Rivas, Michael González Harbour and José F. Ruiz. Implementation of the Ada 2005 Task Dispatching Model in MaRTE OS and GNAT
Abstract. 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.
Lasnier Gilles, Zalila Bechir, Pautet Laurent and Hugues Jérôme. OCARINA: An Environment for AADL Models Analysis and Automatic Code Generation for High Integrity Applications
Abstract. 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
tedious and error-prone part is natural, to which code generation is a natural
solution. In order to make easier the process of verification and certification,
we must use a modeling language which allows the description of critical aspects
relative to these domains. In this paper we introduce the use of AADL as a modeling
language for Distributed Real-time Embedded (DRE) systems. Then we
present our tool-suite OCARINA which allows automatic code generation from
AADL model. Finally, we present a comparison between several approaches, one
being based on OCARINA.
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
tedious and error-prone part is natural, to which code generation is a natural
solution. In order to make easier the process of verification and certification,
we must use a modeling language which allows the description of critical aspects
relative to these domains. In this paper we introduce the use of AADL as a modeling
language for Distributed Real-time Embedded (DRE) systems. Then we
present our tool-suite OCARINA which allows automatic code generation from
AADL model. Finally, we present a comparison between several approaches, one
being based on OCARINA.
Sergio Sáez, Silvia Terrasa, Vicent Lorente and Alfons Crespo. Implementing Reactive Systems with UML State Machines and Ada 2005
Abstract. 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.
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.
Amine Marref and Guillem Bernat. Predicated Worst-Case Execution-Time Analysis
Abstract. 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.
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.
Abstract. 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, especially for systems with hard
real-time requirements. Temporal analysis techniques are available
for this purpose, but they are limited to systems complying with a well-defined
computational model, 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 analysable real-time behaviour, and the necessary language restrictions
that should be used in order to enable the required predictability and
timeliness properties.
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, especially for systems with hard
real-time requirements. Temporal analysis techniques are available
for this purpose, but they are limited to systems complying with a well-defined
computational model, 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 analysable real-time behaviour, and the necessary language restrictions
that should be used in order to enable the required predictability and
timeliness properties.
Claude Kaiser and Jean-François Pradat-Peyre. Using Java or C# Monitor for a concurrency kernel implies defensive multithreading programming
Abstract. Abstract. With the development of embedded and mobile systems, Java and C#, which are widely used for application programs, are 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 these languages.
Two examples show some subtle deadlocks resulting from this policy. The first example deals with process synchronization: a symmetrical rendezvous server is called by processes seeking after partners for a peer-to-peer communication. 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 Java and C# need defensive multithreading programming for developing correct programs and, second, that the familiarity with several styles of concurrent programming helps designing more robust Java or C# solutions, once the choice of the implementation language is irrevocable.
Two examples show some subtle deadlocks resulting from this policy. The first example deals with process synchronization: a symmetrical rendezvous server is called by processes seeking after partners for a peer-to-peer communication. 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 Java and C# need defensive multithreading programming for developing correct programs and, second, that the familiarity with several styles of concurrent programming helps designing more robust Java or C# solutions, once the choice of the implementation language is irrevocable.
Julien Delange, Laurent Pautet and Feiler Peter. Validating safety and security requirements for partitioned architectures
Abstract. Design and validation of safety-critical systems are crucial because faults or security issues could have signiï¬cant 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. We have to validate systems against these requirements to improve safety and security in order 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 could be used to automatically generate and build safe and secure partitioned systems.
Eric Le Pors and Olivier Grisvard. Conceptual Modeling for System Requirements Enhancement
Abstract. 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 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 misreading and misinterpretation 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
Oleg Sokolsky, Insup Lee and Duncan Clarke. Process-Algebraic Interpretation of AADL Models s
Abstract. We present a toolset for the behavioral veriï¬cation and val-
idation 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 implementa-
tion of AADL semantics. The common implementation of the semantics
ensures consistency in the analysis results between the tools.
idation 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 implementa-
tion of AADL semantics. The common implementation of the semantics
ensures consistency in the analysis results between the tools.
Christine Choppy, Olivier Bertrand and Patrice Carle. Coloured Petri nets for chronicle recognition
Abstract. An activity is described by a chronicle that expresses re-
lationships between events in a sequence ordered in time. A chronicle
language provides a syntax for the different chronicle operators consid-
ered. 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
ï¬ring 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 mod-
elling is provided, including more delicate issues such as chronicle with
repetitions, and the absence of sub-chronicles.
lationships between events in a sequence ordered in time. A chronicle
language provides a syntax for the different chronicle operators consid-
ered. 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
ï¬ring 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 mod-
elling is provided, including more delicate issues such as chronicle with
repetitions, and the absence of sub-chronicles.
Didier Buchs, Levi Lucio and Ang Chen. Model Checking Techniques for Test Generation from Business Process Models
Abstract. We will present a methodology and a tool to generate test
cases from a model expressed in Business Process models and a set of
test intentions for choosing a particular kind of tests. In order to do this
we transform the Business Process models in an intermediate format
called Algebraic Petri Nets. We then use model checking techniques (e.g.
Decision Diagrams) to encode the state space — the semantics — of the
model and producing test cases including their oracles according to that
transition system.
cases from a model expressed in Business Process models and a set of
test intentions for choosing a particular kind of tests. In order to do this
we transform the Business Process models in an intermediate format
called Algebraic Petri Nets. We then use model checking techniques (e.g.
Decision Diagrams) to encode the state space — the semantics — of the
model and producing test cases including their oracles according to that
transition system.
François Vernadat, Bernard Berthomieu, Jean-Paul Bodeveix, Christelle Chaudet, Silvano Dal Zilio and Mamoun Filali. Formal Veriï¬cation of AADL Speciï¬cations in the Topcased Environment
Abstract. We describe a formal veriï¬cation 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 trans-
formations that takes place during the veriï¬cation process.
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 trans-
formations that takes place during the veriï¬cation process.