Dr. Brat received his M.Sc. and Ph.D. in Electrical & Computer Engineering in 1998 (The University of Texas at Austin, USA). His thesis defined a (max,+) algebra to model and evaluate non-stationary, periodic timed discrete event systems. Since then, he has specialized on the application of static analysis to software verification. From 1997 to June 1999, he worked at MCC where he led a project that developed static analysis tools for software verification. In June 1999, he joined the Automated Software Engineering group at the NASA Ames Research Center and focused on the application of static analysis to the verification of large software systems. For example, he co-developed and applied static analysis tools based on abstract interpretation to the verification of software for the Mars PathFinder, Deep Space One, and Mars Exploration Rover missions at JPL, various International Space Station controllers at MSFC, and the International Space Station Biological Research Project at the NASA Ames Research Center. His current interests also include the verification of planning and execution systems.

In this lecture, I will describe how we applied static analysis to the verification of flight software at NASA. I will explain why disappointing experiences with commercial tools (lack of scalability and precision) led us to develop our own static analyzer, C Global Surveyor (CGS), and, will go on with a detailed description of the tool. CGS has been developed following the abstract interpretation framework, and, it has a few interesting features such as being able to distribute the analysis over several processors or performing dynamic clustering of variables during abstraction. I will conclude by taking a look at our future directions in static analysis, including coupling CGS, or its successor, with a symbolic execution engine.

In this lecture, I discuss how we approach verification and validation for ground software, i.e., software used on the ground to monitor and control spacecrafts. I will discuss the issues of applying formal methods to the verification of human-machine interfaces. I will describe the different models involved (machine, display, and users) and how we use them to validate interfaces. I will also describe our current efforts in the verification of planning and executing systems. These systems are expected to provide substantial improvements in terms of adaptability, response time, and reliability for ground software.

Sylvain Damiani graduated in 2002 as Space Systems engineer from Supaero, Toulouse, France, which was followed by a Ph.D. in Artificial Intelligence carried out at ONERA (French Aerospace research organism) for CNES (French Space Agency) in Toulouse. His thesis focused on autonomous decision requirements for space systems, in particular on-board real-time decision making. In the context of the management of an Earth watching constellation of satellites, it included the definition and the implementation of planning algorithms (for observation and data downlink activities), and the simulation of the complete space system using a multi-agent framework. Since then, he has been working at VEGA in the Mission Planning and Payload Data Systems group, where his tasks have included the design and the implementation of planning algorithms.

In the space domain, mission planning covers the generation of timelines of activities to be carried out by the various entities of a space mission in order to achieve its goal. This lecture will provide a survey of on-ground planning systems operated in missions of the European Space Agency. We will introduce the requirements on such systems, starting with situating the mission planning functionality in a typical space mission ground segment, and introducing the characteristics of the typical planning problem(s) in several contexts (earth-observation, deep-space, navigation, ground station network). The mission planning software architecture developed by VEGA will be described, together with the rationale for our approach to mission planning systems development. We will conclude by looking at the recent developments in automated planning and autonomy in ESA and in Europe.

In this lecture, we will present in more detail the techniques and algorithms underlying the implementation of two specific systems. We will start with the ESA ground station network planning, an operational system that is providing the automated allocation of ground stations services to all spacecraft managed by ESA. The modelling of mission requirements and network constituent capabilities will be introduced. We will show how a constraint network can be constructed from the dynamic input to the system and its configuration, and present the algorithm used for the resolution of the constraint network. The second part of the lecture will introduce the Automated Planning System (APS) for science operations, which was demonstrated on the ESA Venus-Express mission, and is currently being evaluated for its applicability in the context of future missions of the ESA deep-space programme. The specificity of this planning domain requires interfacing with complex simulators and models. The system implements goal-oriented planning, with optimization of the science return from the plan.

Dans cette présentation, je vais décrire comment nous avons essayé d'appliquer des techniques d'analyse statique à des systèmes de vol embarqués de la NASA. Nos expériences avec des analyseurs commerciaux se sont revélées très décevantes. Nous avons donc dû concevoir notre propre analyseur, en nous servant de la théorie de l'interprétation abstraite. Cette présentation portera plus sur les expériences elles-mêmes que sur les détails théoriques des techniques des outils utilisés. J'essaierai de montrer, en me basant sur des études de cas réels, pourquoi l'analyse statique est importante pour la NASA.

Résumé : Depuis une vingtaine d’année, les Interfaces Utilisateurs (IU) sont de plus en plus complexes, d’une part du fait de la taille sans cesse croissante des systèmes à interfaçer, et d’autre part du fait de l’évolution des possibilités d’interaction. En outre ces interfaces assistent des activités qualifiées de critiques : interfaces de pilotage en avionique, pupitre de contrôle des centrales nucléaires, etc. Le développement de ces interfaces nécessite des méthodologies de validation permettant d’assurer la correction, la sécurité et l’utilisabilité du système. Suivant cet objectif, cet article propose d’utiliser les méthodes formelles dans la phase de validation du processus de développement en suivant une approche ascendante. L’idée est d’exploiter le code source de l’application développée. Un modèle formel B événementiel capturant l’aspect comportemental de l’interface est extrait par analyse statique du code source. Ce modèle formel ensapsule les réactions de l’interface aux actions de l’utilisateur sous forme de système à base d’événements. Le noyau fonctionnel du système est quand à lui abstrait. Ce modèle est alors exploité pour vérifier que l’application répond aux exigences exprimées dans le cahier des charges, notamment en terme d’utilisabilité de l’interface. Plus précisément, l’objectif est de prouver que l’interface supporte un modèle de tâche CTT. Un modèle de tâche décrit en compréhension un ensemble de scénarii d’interaction que l’utilisateur doit pouvoir effectuer sur l’interface. La démarche de validation consiste à formaliser le modèle de tâche CTT en un modèle B événementiel. Ce modèle est alors raffiné par adjonctions de variables et d’événements issues du modèle B extrait du code source. Cette opération de raffinement permet de coupler les actions utilisateur du modèle de tâches avec les réactions du système décrites par le code source. Les preuves de correction du raffinement et la preuve de vivacité du modèle raffiné opéréés permettent de conclure que les scénarii d’utilisation de l’IHM sont conformes à ceux spécifiés par le modèle CTT. L’approche présentée est générique (exploitable quel soit le langage de programmation utilisé) et automatisable. Tout au long du papier, un exemple codé en Java-Swing illustre les différentes étapes de notre démarche.

Résumé : Un des principaux obstacles à l’utilisation d’approches formelles est l’absence de modèles. Nous nous intéressons ici au problème du test de composants logiciels. Dans la pratique industrielle actuelle, il est de plus en plus fréquent de travailler en intégrant des composants logiciels externes dont aucun modèle n’est disponible. La documentation fournit en général une spécification insuffisante. Afin de guider l’intégration, nous proposons d’utiliser des algorithmes d’inférence de machines pour extraire des modèles des composants. L’interaction entre ces modèles dans une composition permet de déduire d’autres tests qui peuvent être confrontés au système. L’ingénieur chargé de l’intégration dispose ainsi d’outils lui permettant de découvrir les interactions effectives entre les composants et de guider le processus de test pour valider les combinaisons de comportements. Nous travaillons sur des modèles d’automates étendus avec des paramètres et des prédicats, mais sans variables internes.

Résumé : Le but de nos études est d’améliorer la déclinaison des exigences de sécurité du niveau système vers le niveau logiciel, en utilisant des modèles formels (AltaRica / OCAS pour représenter le système et Lustre / SCADE pour le logiciel). Cet article présente une démarche traditionnelle d’évaluation de la sécurité d’une architecture système préliminaire. Puis nous proposons une amélioration de cette démarche pour les systèmes incluant une partie logicielle. Nous l’illustrons par un exemple de modèle système à haut niveau en langage AltaRica, dans le but d’étudier les propagations de pannes, et plus précisément d’étudier les interactions entre le système et le logiciel. Cet article expose également différentes façons d’exploiter le modèle système, et en particulier, l’intérêt de la génération des scénarios qui conduisent aux événements redoutés, afin d’en déduire la criticité de chaque fonction logicielle. Pour finir, nous nous intéressons à la déclinaison des exigences de sécurité du système vers le logiciel, et aux moyens envisagés de vérifier que le modèle logiciel satisfait bien les exigences déclinées (par preuves formelles).

Résumé : Sociable interfaces are a game-based model with rich communication primitives that facilitate the modeling of software and distributed systems. The first model of sociable interfaces has been introduced in [1], and then implemented in a tool called TICC [2]. While the primary goal of TICC was to perform the composition of two or more sociable interfaces, it has now evolved into a complete specification and verification tool. This paper presents the current status of the sociable interfaces model and of TICC. It discusses the improvements that have been brought to previous versions of the model and the tool, and investigates future directions of research.
[1] Sociable Interfaces, L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, P. Roy and M. Sorea, Proc. of the 5th International Workshop on Frontiers of Combining Systems, Springer, 2005
[2] TICC, a Tool for Interface Compatibility and Composition, B. Adler, L. de Alfaro, L. D. da Silva, M. Faella, A. Legay, V. Raman and P. Roy, Proc. of the 18th International Conference on Computer Aided Verification (CAV), Springer, 2006

Résumé : Dans une approche composants pour le développement de logiciels, les composants sont considérés comme des boîtes noires qui communiquent via leurs interfaces. L’interface fournie d’un composant peut être connectée à l’interface requise d’un autre composant, si l’interface du premier composant implante les fonctionnalités requises par le second composant. Une description formelle de ces interfaces est nécessaire pour s’assurer de leur compatibilité. En général, les interfaces ne sont pas directement compatibles et un adaptateur doit être introduit. Nous proposons des schémas pour développer des adaptateurs et vérifier l’interopérabilité des composants.

Résumé : Dans ce papier, nous décrivons une technique pour intégrer dans des composants logiciels traditionnels des propriétés temporelles. Nous appliquons le principe de la séparation des préoccupations afin de permettre la spécification du temps de manière indépendante de la spécification fonctionnelle traditionnelle afin de faciliter l’intégration des outils de vérification temporelle dans le développement de logiciels. L’objectif de ces travaux est d’aider l’architecte à spécifier les contrats de temps entre composants et à simplifier l’introduction des propriétés temporelles dans le comportement du composant. Nous proposons de gérer les préoccupations de temps dans une branche de développement séparée et spécifique afin de fournir des méthodes formelles de temps lors de l’assemblage de composants sans modifier le processus de conception existant.

Résumé : Les applications interactives sont incluses dans plusieurs domaines critiques comme le contrôle de vol ou le contrôle de processus industriels dangereux. Elles assurent également l’accès à des services commerciaux divers comme les téléphones mobiles, les systèmes de réservation ou les services de télécommunication. C’est pourquoi, leur correction devient un très important problème et leur développement requiert une validation poussée. Plusieurs méthodes automatiques basées sur des spécifications formelles ont été proposées pour la vérification et la validation de systèmes interactifs. Dans la plupart de ces méthodes, l’application interactive est spécifiée formellement comme un modèle abstrait. Les propriétés sont vérifiées sur ce modèle par les techniques traditionnelles de vérification formelle comme le modèle checking. L’utilisation de la méthode B est également suggérée. Avec cette méthode, un modèle abstrait de l’application interactive et les propriétés à vérifier sont spécifiés. Des techniques de preuves sont appliquées afin d’assurer que les propriétés sont préservées pendant le processus du raffinement. Dans tous les cas, la vérification requiert une démarche lourde de spécification que la plupart de concepteurs des applications interactives ne peuvent pas normalement effectuer. Récemment, nous avons proposé une technique pour tester les systèmes interactifs basés sur l’approche synchrone. Contrairement aux méthodes ci-dessus, cette technique requiert une spécification partielle du comportement de l’utilisateur de l’application. Cette spécification est fournie comme un ensemble d’expressions Lustre et peut être renforcée par des probabilités d’occurrences ou des spécifications de scénarios. Ensuite, plusieurs stratégies de génération peuvent être appliquées pour automatiquement engendrer les entrées du système à tester. La génération des entrées est effectuée "à la volée" (les entrées sont calculées en fonction des entrées et des sorties précédentes). Cependant, ce model synchrone du comportement de l’utilisateur n’est pas facile à construire pour les concepteurs des applications interactives qui ne sont pas habitués avec les langages synchrones. Pour cette raison, nous avons étudié des méthodes de génération de données de test basées sur des modèles qui sont plus habituels dans le processus de développement des applications interactives. Ces modèles sont fournis par les arbres de tâches. Ces derniers décrivent les interactions entre l’application et l’utilisateur. La contribution principale de ce papier est la définition formelle de la transformation de l’arbre de tâche dans un modèle comportemental de l’utilisateur, qui peut être utilisé pour la génération de données de test. Ce modèle est une machine d’états finis à entrées-sorties, qui peut être parcourue selon plusieurs stratégies pour simuler les entrées de l’utilisateur, afin de tester l’application.

Résumé : Les travaux sur le test des logiciels synchrones ayant abouti au développement de l’environnement Lutess avaient pour principale motivation la volonté d’apporter un moyen de vérification complémentaire à la preuve formelle par "model-checking". Cette dernière se limitant essentiellement à la vérification de propriétés définies sur des signaux booléens du programme, cette même limitation s’est retrouvée dans les outils de test développés. Les logiciels synchrones ne se limitant pas uniquement à des entrées sorties booléennes, il était indispensable de prendre en compte des spécifications incluant des relations entre valeurs et expressions numériques. Nous présentons ici une approche basée sur la programmation par contraintes, visant à générer des données de test pour les logiciels synchrones avec des entrées-sorties numériques. La Programmation Logique avec Contraintes (PLC) offre un environnement qui permet d’envisager cette extension de manière simple et efficace sans avoir à développer une solution ad hoc. De plus, il est intéressant d’étudier les moyens d’exploiter cette nouvelle représentation du problème de la génération de test et des avantages que la PLC peut apporter, en particulier pour l’adaptation à ce nouveau contexte des nombreuses stratégies de test que Lutess propose. Plusieurs méthodes de génération ont été étudiées dans ce cadre: la génération aléatoire, guidage par les probabilités et par les propriétés de sûreté. Un autre objectif de notre travail est d’étendre Lutess de sorte à prendre en compte des hypothèses ou des connaissances sur le fonctionnement du programme et de rendre le guidage plus efficace.

Résumé : Les travaux présentés dans cet article s’articulent autour de la validation du contrôle d’accès défini par des politiques de sécurité. Nous nous intéressons à la validation par génération de tests à partir d’un modèle fonctionnel écrit en B. Nous utilisons l’outil Meca, qui prend en entrée un modèle fonctionnel et une description d’une politique de sécurité sous la forme de machines abstraites B, et qui génère un noyau de sécurité pour le modèle fonctionnel. Ce noyau de sécurité est en charge d’intercepter tous les accès des sujets aux objets, et restreint les comportements à ceux satisfaisant les exigences de sécurité. Nous proposons une approche définissant des objectifs de tests de conformité vis-à-vis d’une politique de contrôle d’accès. L’objectif est de s’assurer que les appels à des opérations dans un contexte licite (resp. illicite) sont bien autorisés (resp. sont bien bloquées) sur l’implantation sous test. Nous présentons une étude de cas complète, sur une application de type porte-monnaie électronique, modélisée en B et implantée en Java, et agrémentée d’une politique de sécurité discrétionnaire.

Le projet EICOSE (European Institute for Complex & Safety Critical Embedded Systems Engineering) devient officiellement le premier pôle d'innovation d'ARTEMIS (Advanced Research & Technology for EMbedded Intelligence and Systems), la plate-forme technologique européenne spécialisée dans le domaine des systèmes embarqués. Il inclut les pôles de compétitivité System@tic Paris-Region, Aerospace Valley, ainsi que le cluster allemand SafeTrans. Quatre des cinq groupes de travail du pôle Eicose sont particulièrement intéressants pour les chercheurs AFADL. A savoir : les Environnements de développement des systèmes embarqués critiques ; la réduction des coûts de développement de systèmes certifiables ; la conception pour la robustesse et la fiabilité ; l'interaction système pour les assistances homme-machine.

Le B événementiel a maintenant atteint sa maturité. L'exposé présente donc les principes et concepts de ce formalisme utilisé pour la modélisation de programmes séquentiels, distribués, concurrents ou parallèles ainsi que celle de systèmes complets incluant aussi bien un logiciel que son environnement. L'usage de ce formalisme est toujours basé, comme l'était le B "classique", sur la pratique du raffinement et de la preuve. Les outils de la plateforme Rodin permettent maintenant d'utiliser le B événementiel dans de bonnes conditions. On présentera donc aussi succintement cette plateforme ouverte et d'accès totalement libre.

Résumé : Cet article expose une méthode de modélisation de circuits électroniques synchrones basée sur la méthode B événementielle. Dans ce formalisme adapté à la modélisation de systèmes, un circuit est modélisé par un ensemble d’événements. Certains principes de modélisation ont été dégagés pour l’application de la méthode à la modélisation de circuits synchrones. Un ensemble d’outils permet de valider par la preuve le modèle et ensuite d’obtenir le code simulable et synthétisable VHDL ou SystemC du circuit. Les différentes phases de modélisation sont illustrées à l’aide d’un exemple de protocole d’accès à un bus géré par un arbitre.

Résumé : The B-method, as well as its offspring Event-B, are both tool-supported formal methods used for the development of computer systems whose correctness is formally proven. However, the more complex the specification becomes, the more proof obligations need to be discharged. While many proof obligations can be discharged automatically by recent tools such as the RODIN platform, a considerable number still have to be proven interactively. This can be either because the required proof is too complicated or because the B model is erroneous. In this paper we describe a disprover plugin for RODIN that utilizes the ProB animator and model checker to automatically find counterexamples for a given problematic proof obligation. In case the disprover finds a counterexample, the user can directly investigate the source of the problem (as pinpointed by the counterexample) and she should not attempt to prove the proof obligation. We also discuss under which circumstances our plug-in can be used as a prover, i.e., when the absence of a counterexample actually is a proof of the proof obligation.

Résumé : Pour gérer les accès aux données partagées, on trouve souvent un verrou global. Ici nous nous intéressons aux algorithmes sans verrou qui permettent un accès simultané en lecture et écriture. Malgré une littérature récente abondante, il n’y a pas de preuves de ces algorithmes faites avec des assistants à la preuve. Nous décrivons une méthode qui permet de dériver un algorithme sans verrou à partir d’une spécification atomique. Les dérivations permettent soit de raffiner les structures utilisées par l’algorithme précédent « à la B » (approche top-down), soit de raffiner l’algorithme en rajoutant des points de concurrence. Afin d’avoir une méthode modulaire on travaille plus précisément sur un ensemble d’algorithmes, par exemple celui de la lecture et celui pour la modification. Ceci permet d’adapter le style de la méthode « assume-guarantee ». Dans un deuxième temps, on propose une formalisation de la méthode et de son utilisation. Enfin les algorithmes sans verrou utilisant souvent des solutions types, la méthode permet de disposer d’une bibliothèque de solutions qui seront utilisées comme une dérivation dans la méthode. Pour finir nous faisons une comparaison de cette méthode aux méthodes plus classiques telles que B et TLA+.

Résumé : Un des aspects de la sécurité en informatique concerne le contrôle des accès aux données d’un système pour lequel différentes politiques de sécurité peuvent être mises en oeuvre. Toutefois, rien ne sert de mettre en place une politique de sécurité pour gérer un système si les programmes chargés de garantir le bon fonctionnement de cette politique ne sont pas fiables. Ne pas apporter de garanties fortes sur la correction de tels programmes reviendrait à construire un château fort avec une porte en papier. Dans cet article nous présentons différents développements formels de politiques de contrôle d’accès. Ces développements nous conduisent à introduire un "cadre sémantique" dans lequel il est possible de spécifier, implanter et comparer des politiques de contrôle d’accès.

Dans le cadre de la vérification de systèmes à espace d'états infini, les automates finis s'avèrent être une représentation for commode des ensembles d'états. En particulier, les ensembles de vecteurs d'entiers ou de réels se représentent très naturellement par des automates sur lesquels on peut directement appliquer des procédures de calcul. Dans ce contexte, nous considérons le problème de calculer l'enveloppe convexe d'un ensemble fini de vecteurs d'entiers à n dimensions représenté par une automate fini. La méthode consiste à calculer une séquence d'approximations de l'enveloppe convexe et à utiliser des techniques d'extrapolation pour obtenir la limite de cette séquence. La fermeture convexe peut alors être directement calculée à partir de cette limite sous la forme d'une représentation par automate de l'ensemble correspondant de vecteurs de réels. La technique est fort générale et a été implémentée avec succès.

Résumé : An implemented static analyser of logic programs is presented. The system is based on a unified abstract interpretation framework, which allows the integration of several analyses devoted to verification and optimisation. The analyser is able to verify many desirable properties of logic programs executed with the search-rule and other specific features of Prolog. Such operational properties include verifying type, mode, sharing, and linearity of terms, proving termination, occur-check freeness, sure success or failure, and determinacy of logic procedures, as well as linear relations between the size of input/output terms and the number of solutions to a call. It is emphasized how each analysis may contribute to each other.

Résumé : Des travaux récents sur l’analyse statique de programmes numériques ont montré que les techniques d’interprétation abstraite étaient adaptées à la validation de la précision des calculs en arithmétique flottante. L’utilisation des intervalles comme domaine numérique, même avec des méthodes de subdivision, induit une sur-approximation des résultats en particulier par l’existence de l’effet enveloppant (wrapping effect). Une solution utilisée pour éviter ce problème est la définition de domaines relationnels étroitement liés aux propriétés à valider. Nous allons montrer dans cet article, comment l’utilisation les techniques de différentiation automatique peuvent être utilisées pour définir des formes de Taylor. Ces formes sont à la base d’une nouvelle arithmétique relationnelle implicite qui limite l’effet enveloppant dans le calcul des erreurs tout en garantissant les résultats.