(rédigé par PA)

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

inclusion des expressions

possibilité de factoriser

 * appel de service : pas de factorisation
 
channel[:<RoleId>}[<selector>](!|?|!!|??)message(param*)}
selector : '['i|:i|ALL']'

 * sous-services opt :

 channel[:<RoleId>}[<selector>] {servName1, servName2, ...}

• sous-services mandatory: pas de factorisation : un seul par transition
  

pre/post 

• obs/non-obs
• listes de prédicats nommés

contexte virtuel + nommage des variables présumées

• tous les offerts sont corrects
  • Pre / Post de l'offert préserve Invariant
  • Sous-Services : enchaînements corrects de Pre / Post
    • protocoles
    • eLTS restreint à opt/mandatory (subprovides)
  • Pre + eLST ⇒ Post : étude de l'effet des actions
• tous les requis sont corrects
  • Pre / Post du requis cohérent dans le contexte d'appel du service offert appelant
• Invariant ?
• Obs/nObs : discussion sur incohérence entre les deux ⇒ lever des erreurs de spécification. Ex: Obs correct mais nObs non correct – sans doute plus facile de vérifier uniquement Obs

Règles

• 1.a assertions

  Invt + Pre + Post ⇒ Invt

• 1.b enchaînements de deux services 1 et 2

  Invt + Pre1 + Post1 ⇒ pre2 & Invt

• 1.c actions

  Invt + Pre + Actions ⇒ post & Invt

• 2 Pour chaque appel d'un requis Sr on a la cohérence des “assertions” (état du service sous forme de prédicat Pei)

  Pei |- pre(Sr) post(Sr) + Pei |- Pej

• 3 Invariant et initialisation

  Invt <> false Init ⇒ Invt

• voir les travaux discutés précédemment