Séminaire au vert du Département Langage et Génie Logiciel de l'IRISA

In this talk we present the meaning given to the "interface" word within several activities led by the Triskell team. After recalling the sister "contract" notion in object-oriented and component-oriented domains, we highlight ongoing work relating to models at runtime and model composition.

Les méthodes d'ingénierie des systèmes employées dans l'industrie ont connu ces dernières années des évolutions sensibles, notamment en adaptant des techniques de conception par composants issues de l'ingénierie du logiciel. Ces méthodes offrent d'une part une plus grande flexibilité du processus de conception, et permettent d'autre part des activités de conception parallèles. Les concepteurs sont alors amenés à modéliser, en cours de conception, les hypothèses faites sur l'environnement d'un composant et par la suite, à vérifier le bienfondé de ces hypothèses. Il est donc primordial de pouvoir modéliser non seulement les propriétés comportementales du systèmes à réaliser, mais aussi les hypothèses sous lesquelles ces propriétés sont énoncées. Ceci permet de repousser ultérieurement la réalisation des composants, pour permettre une analyse de la composition de ces composants, reposant uniquement sur la manipulation d'abstractions de composants, appelées interfaces.

Les concepteurs sont donc amenés à manipuler deux sortes d'objets, (i) des réalisations (de composants) et (ii) leurs interfaces. Réalisations et interfaces sont reliées par une relation de satisfaction, qui définit quelles sont les réalisations correctes d'une interface. La relation de satisfaction permet de définir une relation de pré-ordre sur les interfaces, dite relation de raffinement. La nécessité de pouvoir composer les modèles de conception implique que les interfaces doivent pouvoir être combinées selon plusieurs opérateurs de composition: la conjonction des interfaces est requise pour pouvoir combiner les différents points de vues d'un même composant. La composition parallèle et la définition des architectures requiert que les interfaces puissent être composées à l'aide d'une opération de produit. Enfin, une opération de résiduation des interfaces est requise pour pouvoir (i) définir des contrats hypothèses/garanties et (ii) recourir à des méthodes de conception incrémentale, où il s'agit de réduire par étapes successives un problème de conception en une suite de problèmes de moindre difficulté.

Il existe de nombreuses instances de théories d'interfaces. L'une d'entre elle sera présentée, les interfaces modales, qui généralisent à la fois les spécifications modales, les contrats hypothèse/garantie et les automates d'interfaces. Nous aborderons de manière approfondie les propriétés algébriques générales des théories d'interfaces , celles des interfaces modales, les relations avec d'autres formalismes apparentés (contrats et automates d'interfaces) et les implications quant à leur utilisation comme outil support d'une méthode de conception en ingénierie des systèmes.

The distribcom team is involved since 2006 in research around web services and their composition. This implies considering techniques to address distribution, consistency between needs expressed by a module, and the services provided by the other. These needs are not purely functionnal, and may involve data consistency, QoS, etc.

In this talk, we will give an overview of the following activities: - composition and analysis of distributed active documents : how can we distribute data over the web, expect some services from the environment, and prove that two composed systems meets some safety requirements, and exchange the data they expect.

• QoS contracts definition, computation and monitoring : how can we design "soft contract" that are not just a simple threshold of a QoS value, but rather a commitment to meet a QoS from a statistical point of view. How can we monitor a system to detect failure of a soft contract.
• monotonicity in Web services : we will show on easy examples that improving the QoS of a service does not necessarily improve the overall QoS of an orchestration that uses this service. Studying monotonicity is then a central issue to QoS improvement.

We will then discuss the future directions around this line of research.

The talk gives an overview of existing simulation/refinement notions for timed systems and their use in formal methods. In the end we introduce an input-output refinement relation for timed transition systems with inputs/outputs, and its application in model-based testing for real-time systems.

Dans les langages orientés objets, l'échange de données mutables avec du code inconnu est un sujet délicat, en raison du risque de création d'un espace de données accessible à un attaquant. Pour parer à cette éventualité, plusieurs normes de programmation recommandent d'effectuer des copies défensives avant d'accepter ou de renvoyer des références à un objet mutable interne.

En revanche, l'implémentation de méthodes de copie telles que clone() est laissé à la charge du développeur. Celle-ci risque alors de ne pas fournir de copie assez profonde, et est sujette à redéfinition par une sous-classe malveillante. Actuellement aucun mécanisme ne permet de sécuriser la copie d'objet.

Notre travail propose un système d'annotation de types permettant la définition modulaire de politiques de copie pour des programmes orientés objet. Ces politiques définissent le niveau maximal de partage autorisé entre un objet et son clone. Nous présentons un mécanisme de vérification statique qui garantit que toutes les classes respectent leur politique de copie, y compris dans le cas où des méthodes de copie sont redéfinies, et dont nous établissons la correction sémantique en Coq. Ce mécanisme est implémenté et validé expérimentalement sur les méthodes de clone de plusieurs librairies Java.

Quiconque a fait l'expérience de concevoir un programme multitâche, en Java par exemple, reconnaitra la difficulté de l'exercice. Comprendre, mettre en évidence et résoudre les problèmes de concurrence, de synchronisation, de coordination, est une tâche particulièrement difficile et leur mise en œuvre ardue. Aussi, concevoir d'abord un modèle mathématique de l'application pour ensuite synthétiser le programme automatiquement et enfin prouver, une fois pour toutes, la correction de l'algorithme de synthèse, est une approche qui garantie plus facilement et plus rapidement une exécution sûre: plutôt que de programmer directement un logiciel multitâches, il est préférable d'en donner une spécification mathématique simple et facile à prouver, et d'ensuite synthétiser le programme correspondant d'une manière ``correcte par construction''. C'est de cette manière, qu'en Europe et en France, les fonctions ``fly-by-wire'' des avions modernes ont été spécifiées et automatiquement synthétisées au moyen de modèles de programmation synchrone, conceptuellement bien plus simples que les les support de programmation de leurs architectures (AFDX, ARINC) et modèles d'exécution cibles (L)TTA ((Loosely) time-triggered architecture). Aujourd'hui, cependant, des architectures bien plus performantes sont maintenant présentes partout à la maison: des processeurs multi-cœurs aux réseaux sans fil; et les modèles d'exécution de type TTA semblent inadaptés pour exploiter les performances considérables et la parfaite concurrence des calculs qu'offrent ces technologies. Les modèles de calcul synchrone facilitent grandement la génération de code pour la mise en oeuvre de logiciels embarqués sur des architectures relativement simples. Pour effectuer le passage à l'échelle de ces technologies au cadre d'architectures multi-coeurs et concurrentes, il semble évident que des modèles de calculs multi-pas, multi-horloges, polychrones, sont, mêmes si conceptuellement un peu plus complexes, en pratique bien mieux adaptés pour comprendre et maîtriser la mise en oeuvre de logiciels de contrôle. La synthèse de programmes concurrents au moyen de techniques de génération automatique de code multitâche est un outil indispensable pour exploiter les performances des architectures multi-cœurs d'aujourd'hui. Pour développer ces outils, la conceptualisation, la modélisation mathématique, l'analyse, la vérification, la synthèse de programmes doivent être étudiées le plus complètement possible. Aussi, nous proposer de développer des modèles de calcul formel, des méthodes et algorithmes de vérification et de synthèse, pour l'ingénierie de systèmes multitâches, temps-réel, réactifs. Cela permettra de proposer des outils de programmation permettant une modélisation hiérarchique et compositionnelle de systèmes, afin de faciliter le travail de l'ingénieur. Avec ces outils, il sera possible de garantir la correction par construction de ces systèmes, en développant une algorithmique de vérification itérative et une algorithmique de synthèse adaptée. Ce travail repose sur l'étude d'un modèle de calcul polychrone (synchrone multi-horloge), son adaptation ou son extension, pour comprendre et maîtriser la concurrence dans les architectures multi-coeurs. Nous proposons d'étayer cette étude en définissant tout d'abord un outillage algébrique définissant des relations entre un modèle mathématique et sa mise en œuvre GALS (globalement asynchrone localement synchrone), des modèles de calcul causaux et ordonnancés, des modèles de temps discrets et temps-réel, adaptés aux architectures multi-coeur. De ces relations découlent un cadre mathématique simple qui permet de représenter formellement le fonctionnement d'architectures logicielles multitâches et de synthétiser les programmes qui exécutent ces fonctions. Ces études supportent la définition d'une méthodologie de conception formellement bien fondée. L'objectif de cette méthodologie est d'aider l'architecte logiciel à mettre en oeuvre un programme concurrent sur une architecture complexe. Elle considère un modèle mathématique abstrait des composants du logiciel et de son support d'exécution. Elle met en oeuvre des méthodes formelles d'analyse, de vérification, de synthèse, de transformation, qui vont aider l'architecte de synthétiser un logiciel multitâche pour une architecture multi-coeur à partir de ce modèle, tout en assurant que les propriétés qui avaient initialement été spécifiées soient toujours préservées. Une application majeure de ces techniques est l'exploration d'architecture L'exploration d'architecture est une activité qui intervient très tôt dans le flot de conception d'un logiciel afin d'aider l'architecte logiciel à prendre des décisions importantes sur le logiciel en termes de coût et en performance. Il s'agit de combiner des spécifications hétérogènes comme celle de l'architecture logicielle et matérielle du système, de ses fonctions de contrôles discrètes et continues au moyen d'un même modèle de calcul médian, afin de pouvoir valider le plus tôt possibles des exigences fonctionnelles ou temps-réel, mais encore de conduire une activité de co-modélisation pour simuler, tester, vérifier, son comportement, voir même générer du code pour celui ci.