Programme de la journée MFDL 2012


09h30
  • Accueil

10h00
  • ANDRIAMIARINA Manamiary Bruno (LORIA-Nancy)

    Titre : Formal verification of Fault Tolerant Noc-based architecture

    Résumé : Approaches to design fault tolerant Network-on-Chip (NoC) for System-on-Chip(SoC)-based reconfigurable Field-Programmable Gate Array (FPGA) technology are challenges on the conceptualisation of the Multiprocessor System-on-Chip (MPSoC) design. For this purpose, the use of rigorous formal approaches, based on incremental design and proof theory, has become an essential step in a validation architecture. The Event-B formal method is a promising formal approach that can be used to develop, model and prove accurately the domain of SoCs and MPSoCs. This paper gives a formal verification of a NoC architecture, using the Event-B methodology. The formalisation process is based on an incremental and validated correct-by-construction development of the NoC architecture.


10h45
  • Christophe Chareton (ONERA DTIM)

    Titre : Strategic Reasoning for the Resolution of Assignment Problems in Goal- and Actor-Oriented Requirements Engineering

    Résumé : The aim of this talk is to preset a formal framework for actor- and goal-oriented requirements engineering modelling. To do so, we define Khi, a core modelling language, as well as its semantics in terms of a strategy logic we call SLsc. Actors, concrete active entities, are defined by their capabilities. They also pursue behavioural goals that are realised by operations. Then a relation of assignment, between (coalitions of) actors and roles (sets of operation specifications) is defined. We highlight the importance of this relation by exhibiting three "assignment problems" and we define criteria for their correctness. They are modalities about the effective ability of (coalitions of) actors to play their assigned roles. The assignment problems reduce to the satisfaction of Slsc formulas in a structure derived from the capabilities of actors. Thanks to the properties of SLsc, we end up with a decidable procedure for the assignment problems. We illustrate our approach using a toy example featuring a satellite-based Earth observation mission.


11h30
  • Picard Celia (IRIT-Toulouse)

    Titre : Coinductive Graph Representation

    Résumé : This presentation stands at the interface between Model Driven Engineering (MDE) and type theory. We aim at certifying model representation and transformation, using the interactive theorem prover Coq for certification matters. This talk only deals with representation and manipulation of graphs using coinductive types. First we present our coinductive representation of graphs. The use of coinductive types allows, among other things, to ensure navigability by construction. While defining this representation, we have to overcome Coq's guardedness condition using a non-inductive type to represent lists. We also define various tools to manipulate those lists and graphs, among which the canonical relation on graphs. Then, we define a wider (parameterized) relation on graphs. This new relation is close to the notion of equivalence on the classical representation of graphs (set of nodes/set of edges), but keeps the advantages offered by coinduction. Indeed, our definit ion of graph induces an implicit order (both horizontally and vertically) between the nodes. The new relation allows us to abstract from this order. We also show that this relation is equivalent to another one based on finite observations of graphs, which requires a non-constructive principle to be added to Coq's logic.


14h00
  • Présentation industrielle invitée : Yannick Moy (ADACORE)

    - Stratégie d'intégration du test et de la preuve formelle


15h00
  • Sanogo Alfred (LIPN)

    Titre : Méthodologie de Conception des Modèles exprimés en réseaux de Petri :Raffinement des réseaux de Petri colorés

    Résumé : Les réseaux de Petri colorés sont très utilisés comme langage de spécification des systèmes complexes caractérisés par la concurrence. La spécification d'un système complexe (réel) nécessite généralement la prise en compte de nombreux détails. Des difficultés apparaissent lorsque l'on essaye de prendre en compte tous ces détails dans le modèle en une seule étape. L'une des solutions consiste à construire un modèle plus abstrait (avec moins de détails) et modifier ce modèle étape par étape en apportant plus de détails à chaque étape. Cette démarche appelée raffinement prend fin lorsque tous les détails sont pris en compte. Plusieurs chercheurs ont travaillé sur le raffinement des modèles exprimés en réseaux de Petri colorés et proposé le raffinement des places, le raffinement des transitions, le raffinement par sous-réseau et le raffinement de type. Nous avons dans notre travail proposé de nouvelles règles de raffinement de type et de! transition. Nous essayons d'élargir le raffinement de type proposé par C. Lakos. Cet élargissement concerne la relation qui doit exister entre le type raffiné et le type abstrait et les modifications sur le type. En plus du principe de raffinement de C. Lakos, la relation de sous-typage définie par B. Liskov et J. Wing. La règle de raffinement de transition consiste à remplacer la transition abstraite par un sous-réseau qui comprend des transitions dites alternatives. Nous avons mené des études de cas pour illustrer ces règles de raffinement et développé un outil d'aide à la conception des modèles exprimés en réseaux de Petri colorés.


15h45
  • Diagne Fama (Télécom Sud Paris / Simbad)

    Titre : Utilisation de raffinement B pour la preuve de propriétés d'atteignabilité

    Résumé : Nous présentons dans cet exposé une approche de vérification de propriétés d’atteignabilité, de la forme AG (ψ⇒ EF ϕ), en utilisant le raffinement de substitutions de la méthode B. De telles propriétés assurent l’existence d’un chemin à partir de chaque état qui satisfait ψ à état qui satisfait ϕ. Ce type de propriétés est très fréquent dans le domaine des systèmes d’information par exemple. On montre comment il est possible d’utiliser les spécifications de Morgan pour représenter une propriété et les règles de raffinement pour la prouver. L’idée clé est de définir, par raffinement successif, un programme dont l’exécution satisfait AG (ψ⇒ EF ϕ). Pour prouver un tel raffinement, des obligations de preuve sont générées et prouvées comme des assertions en utilisant l’AtelierB.


16h30
  • Conclusion