====== CR rapide du 05/03/09 ======
 
//(rédigé par PA)//

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

===== Kmelia =====

==== discussions sur la sémantique de Kmelia ====

  * voir notes PS {{kmelia:simplest.pdf|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














==== discussions sur Kmelia/B et vérification ====

plus tard
   rapport MM en cours 
{{kmelia:rr_xx_yy.ps|ici}}

==== discussions sur shared services et vérification ====

plus tard
  retrouver la dernière discussion sur le sujet