We consider lightweight usage of model-checking for the debugging of Simulink models. A problem is that model-checkers typically return only one counterexample, which may slow down the debugging process. We propose an approach and a tool to produce several counterexamples, exemplifying different property violation patterns for a given version of the design. The approach uses data collected during the replay of the counterexamples to synthesize queries for the model-checker, so that it finds counterexamples that activate new paths. The approach is applied to an academic example and an industrial model from the automotive domain.

In this paper we present STELAE, a model-driven test development environment for avionics embedded systems, implemented on top of a real integration test platform. It is the result of an R&D project between two research laboratories and a test solution provider, aiming to introduce model-driven engineering methodologies and technologies for the development of tests. Our work was motivated by the multiplicity of proprietary test languages in this industrial context, which no longer respond to the stakeholder needs. We present the early prototype functionalities (test model definition, automatic code generation and execution) on a case study inspired from real-life. Our feedback on the used technologies concludes this paper.

Tests for avionics embedded systems are implemented using proprietary test languages. No standard has emerged and the set of existing test languages is heterogeneous. This is challenging for test solution providers, who have to accommodate the different habits of their clients. In addition, test exchange between aircraft manufacturers and equipment/system providers is hindered. To address these problems, we propose a model-driven approach for test implementation: test models are developed/maintained, with model-tocode transformations towards target executable test languages. This paper presents the test meta-model underlying the approach. It integrates the domain-specific concepts identified from an analysis of a sample of proprietary test languages. The test meta-model is the basis for building test model editors and templatebased automatic code generators, as illustrated by a demonstrator we developed.

Aspect Oriented (AO) Technology is a post-object oriented technology emerged to overcome limitations of Object Oriented (OO) Technology, such as the cross-cutting concern problem. Aspect Oriented Programming (AOP) also offers modularity and traceability benefits. Yet, reasoning, specification, and verification of AO systems present unique challenges especially as such systems evolve over time. Consequently, formal modular reasoning of such systems is highly attractive as it enables tractable evolution, otherwise necessitating that the entire system be reexamined each time a component is changed or is added. Besides, the aspect interactions problem is an open issue in aspect-oriented area. To deal with this problem, we choose to use category theory (CT) and algebraic specification(AS) techniques. In this paper, we present an aspect-oriented modeling (AOM) approach and a weaving algorithm. Our approach is expressive and allows for formal modular reasoning.

Aspect-oriented software development (AOSD) has emerged in recent years as a new paradigm for software development, providing mechanisms to localize cross-cutting concerns (i.e. scattered in many locations) during the software development process. Aspect interaction problems (due to their integration into the base components) is an important issue in AOSD, verification is most often based on a detection and correction strategy. This paper presents an ongoing work which goal is to built a prevention mechanism at the specification phase for aspect-oriented systems. This prevention mechanism will allow to avoid undesirable interactions in a aspect-oriented system. By acting at the specification phase, we believe that verification will be made timeless and costless.

In previous work, we defined a component oriented framework dedicated to the specification of embedded systems in the aeronautics domain. A component is defined as a formal entity with three internal layers together with a collection of models defined in domain-oriented views. A categorical framework has been proposed to provide a unified representation of the component calculus as well as the various formal models used for the analysis of the system. In this paper, we present an implementation of this categorical framework using the EXPRESS data modelling language. EXPRESS is used to give an operational representation of the formalization, which is quite different from classical implementations of category theory based approaches.

This paper presents an approach to automate test generation from a formal specification and a set of functional test objectives while taking into account coverage constraints at the specification level. We use existing test generation techniques and tools, our contribution is on the methodological side. We define an innovative approach adapted to the industrial domain and its constraints

This paper presents a component oriented framework dedicated to the specification of embedded systems in the aeronautics domain. A component is an entity with three internal layers (hardware, operating functions and applicative functions) together with a collection of models in different domain-oriented views. A composition operation allows the expression of composition scenarios, yielding a component calculus for representing composite systems. An institutional framework supports this component calculus, allowing the expression of coherence criteria between heterogeneous views. This framework can be seen as a formal documentation of a system development and analysis, supporting heterogeneous modeling and compositional verification. The approach is illustrated on a non trivial case study.

Avionics embedded systems are confronted to sensors errors or inaccuracies. It is essential to be able to estimate the impact and the propagation of these errors on the system computed outputs. This paper comes from achieved work in the context of an industrial project in the avionics area. It presents a formal approach allowing to analyse the reaction of a LUSTRE program to inaccurate input values. It uses program analysis techniques like abstract interpretation and interval analysis. The approach has been implemented in Java and applied to parts of a flight control system of the AIRBUS aircrafts.

This paper presents an approach enabling a smart card issuer to verify that a new applet securely interacts with already downloaded applets. A security policy has been defined that associates levels to applet attributes and methods and defines author

This paper describes a feasibility study into the use of a formal requirements modeling method (SCR) to assist with independent verification and validation of change requests for space shuttle flight software. The goal of the study was to determine whether a formal modeling technique could automate some of the manual analysis tasks performed on change requests, including consistency checking. To analyze the change request, the key part of the original functionality was modeled in SCR. The model was then updated to reflect the proposed changes. Tool support was used to perform consistency checking and to validate the model against domain properties. The study showed that as an analysis tool, formal modeling offers some advantages over inspection-based approaches. However, the problem of analyzing change requests is sufficiently different from other requirements modeling tasks that some specialist tools will be needed. The paper ends with a discussion of the demands of these needs.

Structure is important in large specifications for understanding, testing and managing change. Category theory has been explored as framework for providing this structure, and has been successfully used to compose specifications. This work has typically adopted a "correct-by-construction" approach: components are specified, proved correct and then composed together in such a way as to preserve their properties. However, in a large project, it is desirable to be able to mix specification and composition steps such that, at any particular moment in the process, we may have established only some of the properties of the components and some of the composition relations. In this paper, we propose adaptations to the categorical framework in order to manage evolving specifications. We demonstrate the utility of the framework on the analysis of a part of a software change request for the Space Shuttle.