(rédigé par PA)

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

• voir notes PS cas simple
• cas NONINTERRUPTIBLE :
  • aucun autre service s'exécute en parallèle dans le composants (tous suspendus)
  • appel service interne : uniquement synchrone sinon PB
• plusieurs (instances de) services s'exécutent avec un espace d'état partagé
• plusieurs instances d'un même service pas possible (pour l'instant) : un seul canal (bipoint)
• clause initialisation dans un service (même chose que pour un composant)

  var := expr sans com : ElementaryAction expr : portée : var comp, constantes, param, autres var locales (si def avant)

• pre/post : pas sur les variables locales post : accès variable de retour
• ajouter une variable prédef “result” pour nommer le résultat
• val après d'une var du composant : before(var)
• Pas de variables locales dans les postconditions
  Usage
  • abstraction : vérif stat
  • assertion : vérif dyn
• pas d'effets de bord sur des fonctions
• code = actions (elem + com) 1 seule comm par transition de base

plus tard

 rapport MM en cours 

ici

plus tard

retrouver la dernière discussion sur le sujet