====== CR rapide du 19/02/09 ====== //(rédigé par PA)// Présents : PA, CA, GA, AL, MM ===== Kmelia ===== ==== discussions sur Kml2B ==== * étude des propositions sur graphes de contrôles * articles de p. Sotin, thèse de LEDANG {{kmelia:phd_ledang.ps.gz|}} * trouver les bonnes constructions B === Graphe acyclique === * trouver tous les chemins * graphe de dépendance de services à établir * étude des propositions sur graphes de contrôles === Machines === * mach_component includes mach_state promote mach_services uses mach_state * patterns dans le LTS * codage //à la UMLToB// : pas intéressant du côté preuve === Niveaux === * traiter en même temps pre/post et eLTS : le raffinement du eLTS se ramène à la pre/post * requis/fourni : raffinement ===== Relevé de décisions ===== ==== Niveau 1 ==== * 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 ==== Niveau 2 ==== * 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) ==== Niveau 3 ==== * enchaînement de services, protocoles traduction KmlToB des actions de base, des prédicast cohérence de plusieurs pre/post cas simplifié de LTS ==== Niveau 4 ==== * eLTS est un raffinement des pre/post traduction KmlToB des actions et eLTS * à creuser