(rédigé par PA)

Présents : PA, CA, GA, AL, MM

• étude des propositions sur graphes de contrôles
• articles de p. Sotin, thèse de LEDANG phd_ledang.ps.gz
• trouver les bonnes constructions B

• trouver tous les chemins
• graphe de dépendance de services à établir
• étude des propositions sur graphes de contrôles

• machcomponent includes machstate promote machservices uses machstate
• patterns dans le LTS
• codage à la UMLToB : pas intéressant du côté preuve

• traiter en même temps pre/post et eLTS : le raffinement du eLTS se ramène à la pre/post
• requis/fourni : raffinement

• un composant Kml = une machine B + INVT

  traduction KmlToB des variables d'état + prédicat

• un service Kml = une opération B + Pre/Post

  traduction KmlToB des prédicats + extraction des variables

  opserv = Pre trad(Pserv) THEN ANY x WHERE trad(Qserv) THEN var := x END END

• lire papiers cités par AL

• cohérence requis offert

  traduction KmlToB des variables d'état + prédicat raffinement requis/offert

  Machine Refinement C1-prov refine C2-req masquer les autres opérations

  Machine C1-prov v11 : T11 s1 s2 s3

  Machine C2-req v11 : T11 s4 requis + contexte : v1:T1 s5 masqué s5 masqué

  Refinement refines C2' (masquage des opérations inutiles) includes C1 invariant : V1 ↔ v11 operation s4 ^= S1

• cas des sous-services à voir plus tard
• cas des types et signatures (contexte, paramètres)

• enchaînement de services, protocoles

  traduction KmlToB des actions de base, des prédicast

  cohérence de plusieurs pre/post cas simplifié de LTS

• eLTS est un raffinement des pre/post

  traduction KmlToB des actions et eLTS

• à creuser