Thématique de la journée

Un système embarqué est un ensemble cohérent de constituants informatiques (matériels et logiciels). Il est souvent invisible à l’utilisateur d’un équipement. Il donne à l’équipement la capacité de remplir un ensemble de missions spécifiques en le dotant d’intelligence. Il effectue des traitements numériques et gère les échanges d’informations de l’équipement nécessaires à l’accomplissement de ses missions. D’autre part, un système informatique embarqué doit faire face, à des degrés divers, à des contraintes temps réel dont la nature conduit à distinguer les systèmes temps réel durs ou critiques (devant respecter des bornes de temps de réponses, faute de quoi la mission de l’équipement ne peut être remplie) et les systèmes temps réel mous (devant tendre à respecter des contraintes dont le non respect temporaire engendre au plus un dysfonctionnement partiel qui ne remet pas en cause sa mission). On parle de système embarqué critique lorsqu’un équipement réalise une mission dont l’échec a potentiellement un impact majeur sur la vie, la santé de personnes, sur l’état de l’environnement,... plus généralement sur l’accomplissement de missions critiques auquel il participe. Que ce soit à cause de leur coût de fabrication, leur caractère critique, leur complexité ou encore leur inaccessibilité pendant leur utilisation, l’ingénierie de ces systèmes nécessite l’utilisation de méthodes, de procédés, de modèles et d’outils spécifiques.

Sponsors et partenaires de la journée :

  AdaCore (http://www.adacore.com)
  Ellidiss technologies (http://www.ellidiss.com)
  Jessica France (http://www.jessica-france.fr/)

Programme de la journée

Matinée

9h-9h30. Accueil des participants, café.

9h30-10h15. Premiers retours d’un chercheur sur l’utilisation de l’IDM pour le temps réel. Jérôme Delatour, ESEO (Angers) .

10h15-11h. AADL : état et perspectives. Pierre Dissaux, Ellidiss Technologies (Brest) .

11h-11h45. Validation de systèmes temps-réel et embarqué à partir d’un modèle MARTE : expérimentation. Eric Maes, THALES Research and Technology (Palaiseau) .

11h45-12h30. AUTOSAR : Streamlining automotive systems and processes. Francois Dupont, Geensys (Brest) .

Après-midi

Pause déjeuner, café.

14h30-15h15. Expérimentation d’unités de preuve pour la validation formelle de logiciels embarqués critiques. Philippe Dhaussy*, Pierre Yves Pilain*, Dominique Kerjean* Stéphane de Belloy**, Arnaud Monégier du Sorbier**, Hugues Bonnin +, Frédéric Boniol***. * Laboratoire DTN, ENSIETA (Brest), ** THALES AIR SYSTEMS (Rungis), + CS-SI (Toulouse), *** IRIT-ENSEEIHT (Toulouse).

15h15-16h. Ada 2005 pour les systèmes embarqués temps réel. José F. Ruiz, AdaCore (Paris) .

16h-16h45. Les outils de retro-ingénierie de code Ada. Eric Audrezet, Sodius (Nantes).

16h45. Fin de la journée, bilan et annonce de la journée suivante.

Inscription et informations pratiques

La participation à cette journée est gratuite. Les pauses café ainsi qu’un déjeuner seront offerts par les sponsors. Pour des raisons de logistiques (repas, salles), l’inscription à cette journée est obligatoire. La date limite d’inscription est fixée au 1er décembre.

L’inscription peut être effectuée en renvoyant le bulletin ci-dessous par email à F. Singhoff (singhoff@univ-brest.fr).

Nom :

Prénom :

Profession :

Organisme/établissement :

Adresse professionelle :

Téléphone :

E-mail :

La journée se déroule à l’ENST-Bretagne. Un plan d’accès (avion, bus, voiture, train) est disponible ici : http://www.enst-bretagne.fr/ecole/campus_de_brest/plan_d_acces/

Résumés des présentations

Premiers retours d’un chercheur sur l’utilisation de l’IDM pour le temps réel

Jérôme Delatour, ESEO (Angers)

Une nouvelle approche de développement, l’Ingénierie Dirigée par les Modèles (IDM, ou MDA en anglais), est apparue en 2000. Le domaine des systèmes temps réel et/ou enfouis (embedded and real-time systems) s’est très vite intéressé à cette nouvelle approche. Sept ans après son apparition, cet exposé propose de faire un premier état des lieux sur les intérêts mais aussi les limites de cette approche pour le développement de système temps réel. Un rapide panorama de la terminologie de l’IDM, ainsi que des outils et techniques disponibles sera effectué. Cet exposé sera illustré par des exemples issus des travaux effectués dans ce domaine par l’équipe de recherche TRAME (TRAnsformations de Modèles pour l’Embarqué).

AADL : état et perspectives

Pierre Dissaux, Ellidiss Technologies (Brest)

Le langage AADL (Architecture Analysis and Design Language) a fait l’objet d’une publication en tant que norme internationale auprès de la SAE (Society for Automotive Engineering) en novembre 2004. Une nouvelle version du standard est actuellement en cours de finalisation. Cette présentation débutera par un brève revue des principaux concepts de AADL et de son comité de standardisation, sera suivi d’une synthèse des trois années de mise en oeuvre du standard en terme de réalisation d’outillage, de prise en compte dans des programmes de recherche et d’évaluation industrielle, et se terminera par un panorama des nouveautés attendues pour la nouvelle version avec un éclairage plus focalisé sur l’annexe comportementale. Une des interrogation fréquente des utilisateurs potentiels d’AADL concerne son positionnement vis à vis du monde UML. Dans chaque partie de l’exposé, les intéractions existantes ou futures avec UML seront évoquées.

Validation de systèmes temps-réel et embarqué à partir d’un modèle MARTE : expérimentation

Eric Maes, THALES Research and Technology (Palaiseau)

Un processus de modélisation pour les systèmes temps-réels et embarqués implique l’utilisation de différents modèles dédiés chacun aux différentes phases du développement (spécification, conception, test, ...) et aux interactions avec des outils (vérification de modèle, analyse de performance, analyse d’ordonnançabilité, ...). Centraliser ces différentes informations généralement traitées par des intervenants différents au niveau d’un seul modèle permet d’avoir une vue générale du système, d’en garantir la cohérence et d’en faciliter la validation tout au long du processus de développement afin de réduire le coût de ce développement.

Le nouveau standard MARTE (« Modeling and Analysis of Real-time and Embedded systems ») est le profil UML de l’OMG permettant de répondre à cette problématique dans le domaine du temps-réel et de l’embarqué. Il propose un langage intégrant l’ensemble des concepts propres à ce domaine et ceci pour les différents stades du processus de développement. MARTE permet d’étendre un modèle UML avec des caractéristiques spécifiques aux systèmes-temps réels. Celles-ci peuvent alors être utilisées pour faire des prédictions quantitatives relatives aux fonctionnalités temps-réel et embarqué d’un système, tout en tenant compte, tant des aspects matériels que des caractéristiques logicielles. Cela facilite une interopérabilité entre les outils utilisés pour la spécification , la conception, l’analyse et la vérification.

Afin de montrer le gain obtenu par l’utilisation d’une telle démarche, il est nécessaire d’établir un processus outillé et de construire une étude concrète permettant de démontrer l’interopérabilité entre les outils. Un processus outillé recquiert : 1) une démarche de modélisation, 2) la prise en compte de l’ensemble des concepts nécessaires pour appliquer une analyse utile et 3) l’automatisation du processus pour envisager une interaction rapide et sûre avec des outils de validation. Un tel processus outillé doit convaincre les utilisateurs industriels à adhérer à la démarche. Nous proposons de définir et de mettre en oeuvre un tel processus outillé dans le cadre particulier d’un cas d’étude classique du monde temps-réel et embarqué que nous souhaitons valider à l’aide d’un outil d’analyse.

Le cas d’étude, un robot autonome relevant la température à intervalles réguliers de temps, le long d’une route prédéterminée, a été modélisé en utilisant MARTE, en y intégrant les notions propres à sa conception et à son analyse. Les caractéristiques du modèle sont ensuite prises en compte pour pouvoir en réaliser une analyse d’ordonnançabilité avec l’outil cheddar. Mettant en évidence la détection de disfonctionnements possible du système, cette expérimentation permet aussi et surtout de proposer une démarche pour modéliser les systèmes temps-réel en utilisant MARTE et de valider l’approche qui consiste à travailler avec un modèle unique.

AUTOSAR : Streamlining automotive systems and processes

Francois Dupont, Geensys (Brest)

The talk explains the AUTOSAR initiative for reducing industrial costs and streamlining the relationships between actors by leveraging the benefits of meta-modeling embedded distributed systems and its impact on related development and industrial processes.

Expérimentation d’unités de preuve pour la validation formelle de logiciels embarqués critiques

Philippe Dhaussy*, Pierre Yves Pilain*, Dominique Kerjean* Stéphane de Belloy**, Arnaud Monégier du Sorbier**, Hugues Bonnin +, Frédéric Boniol***. * Laboratoire DTN, ENSIETA (Brest), ** THALES AIR SYSTEMS (Rungis), + CS-SI (Toulouse), *** IRIT-ENSEEIHT (Toulouse)

Contexte : les systèmes d’information embarqués

Les concepteurs de logiciels embarqués critiques ont aujourd’hui à leur disposition de nombreux outils de spécification, de conception et de validation facilitant le développement des logiciels dans leur processus d’ingénierie. De nombreux travaux universitaires dans le domaine de la validation formelle ont exploré différents formalismes ou langages et ont contribué à la conception de techniques d’analyse et de preuve exploitables en contexte industriel. Néanmoins, nous constatons aujourd’hui encore une faible pénétration dans le processus d’ingénierie système et logicielle comparativement aux énormes besoins en terme de recherche de fiabilité et sûreté de fonctionnement des systèmes critiques. Cette contradiction trouve en partie ses causes dans la difficulté réelle de manipuler des concepts théoriques et des méthodes formelles dans un cadre industriel. Il nous apparaît donc indispensable de poursuivre les efforts pour contribuer à une meilleure intégration des techniques formelles dans les processus d’ingénierie.

Apport de l’IDM : opportunité et composants MDA

L’Ingénierie Dirigée par les Modèles (IDM) apparaît par ailleurs au niveau industriel comme une réponse potentielle pour la réalisation des systèmes à logiciels prépondérants qui englobent les systèmes embarqués et les systèmes d’information. Il est donc à notre avis pertinent de profiter des réflexions de la communauté IDM pour étudier les conditions d’une meilleure intégration des méthodes formelles. Ces approches peuvent nous permettre, par le biais de la notion de méta modèles et leur exploitation dans la manipulation et la transformation de modèles, de poser les bases des principes mis en Å“uvre dans les futurs outils à concevoir. Ceux-ci doivent permettre à l’ingénieur une utilisation plus importante des techniques de vérification et une meilleure capitalisation de son savoir-faire. Il semble donc pertinent d’identifier des composants MDA spécifiques pour la validation pouvant être manipulés comme des composants à part entière d’un processus de développement et se poser le problème de leur intégration dans les processus d’ingénierie.

Contribution

Pour contribuer à répondre à ce défi, le laboratoire DTN de l’ENSIETA, en partenariat avec THALES, CS-SI et l’IRIT, a développé une approche pour la vérification formelle basée sur la définition de composants MDA, nommés unités de preuves. Celles-ci encapsulent toutes les données nécessaires à la preuve de propriétés sur un modèle logiciel à vérifier et plongé dans un environnement. L’ensemble des unités de preuve, manipulé par l’utilisateur durant l’activité de validation de son modèle, constitue l’ensemble des obligations de preuve devant être démontrées. Elles peuvent être construites à partir des données fournies par les phases d’analyse et de conception du système. Ces composants intègrent des contextes de preuve qui modélisent formellement des exigences de sûreté ou vivacité bornée dans un contexte comportemental donné. Dans une approche IDM, les contextes de preuve sont traduits par transformation en codes exploitables par des outils d’analyse formelle. La présentation proposée rend compte d’expérimentations de cette approche menées sur des cas d’étude fournis par les industriels. Les unités de preuve intègrent une description des contextes de preuve dans un langage nommé CDL (Context Description Language) et sont exploités par l’outil de vérification OBP (Observer-Based Prover), développé au laboratoire ENSIETA-DTN mettant en œuvre le langage à automates temporisés IF et une technique de vérification par observateur.

Ada 2005 pour les systèmes embarqués temps réel

José F. Ruiz, AdaCore (Paris)

The presentation will show some interesting features that Ada offers to develop embedded real-time software, paying special attention to the new capabilities added to the Ada 2005 revision.

Embedded real-time systems typically have strong requirements in terms of predictability, memory footprint and efficiency. Ada defines a standardized mechanism to specify configuration directives which allow developers to constrain the language features to a well-defined subset, in such a way as to preclude complex, inefficient and non-deterministic features. The compiler can hence select a more efficient implementation of the required functionality according to the selected restrictions, including the removal of unnecessary run-time support.

An interesting subset for embedded high-integrity real-time systems is the Ravenscar profile, a reliable concurrency model standardized in Ada 2005. The Ravenscar profile comprises a powerful and expressive computational model that can be supported by a small, reliable, and extremely efficient run-time system. The Ravenscar tasking model has been designed to meet the requirements for determinism, schedulability analysis, and memory boundedness, making it suitable for both hard real-time and high-integrity systems. An additional Ada 2005 tasking feature designed to increase robustness is the support to monitor and control execution time.

These features allow run-time detection of an excessive consumption of computational resources, typically caused by either software errors or design errors made in the computation of worst-case execution times. Ada 2005 defines also some flexible scheduling policies, such as round robin using time slicing, and Earliest Deadline First (EDF) policy, which can also be mixed according to priority levels within a partition. Timing events are a new Ada 2005 feature that allows programmers to define code that is executed at a future point in time in an efficient and elegant way.

Ada 2005 includes also the means to use the powerful notions of object-oriented programming in embedded systems, where we want to limit the usage of memory and processing resources. Type extension and inheritance provide meaningful abstractions to design extensible and reusable modules where code is structured into a hierarchical set of classes with strict control over visibility of encapsulated state, data, and methods. Ada 2005 provides very fine-grained control over inheritance by allowing each operation to declare explicitly whether it is intended to inherit. Multiple inheritance of specification has been introduced in Ada 2005 through the notion of interfaces, which also extends to the unique Ada notions of task and concurrent object, maintaining the important design principle that concurrency is a first class citizen.

The use of Ada high-level constructs for low-level programming facilitates development, code reviews and analysis. Representation clauses in Ada allow close mapping of software data structures to the hardware. The association of this abstract data representation and Ada’s strong typing allows for compile-time verifications that help early detection of errors in the development process. Hardware-specific features, such as vector processing instructions or direct operations on I/O ports, are also supported in Ada, together with the mechanisms for handling hardware interrupts. It is also possible to force read and update operations to be performed either directly to memory, or in an indivisible (atomic) manner.

Les outils de retro-ingénierie de code Ada

Eric Audrezet, Sodius (Nantes)

Les outils de retro-ingénierie de code Ada. Eric Audrezet, Sodius (Nantes). Dans le cadre de la reprise de code Ada soit à des fins de rétrodocumentation ou pour nourrir des modèles à réutiliser, il est essentiel de disposer de solutions flexibles d’analyse de code existant. Toutefois, les différents processus de codage existant, ainsi que la variété des profiles UML destinataires, ne permettent pas d’imaginer une solution universelle. Il est donc impératif de se baser sur des mécanismes flexibles, permettant d’avoir un haut niveau de maîtrise des structures UML à générer. Dans le cadre de la réalisation de notre outil de retro-ingénierie Ada, nous avons mis en place un mécanisme mettant en jeu plusieurs niveaux de méta-modèles, syntaxique et sémantique, liés entre eux par des règles de transformation. La présentation entre dans le détail de ce mécanisme.

Sponsors