====== CR rapide du 26/02/09 ======
 
//(rédigé par PA)//

Présents : PA, GA, AL, MM

===== Kmelia =====

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

  * voir notes MM

=== Axiomes ===

  * **Composant séquentiel**: une seule action d'un service s'exécute à la fois dans un composant (et dans le système) - Atomicité
  * **Concurrence locale**: plusieurs instances de un ou plusieurs services d'un composant s'exécutent en parallèle dans le composant
  * **Concurrence globale**: plusieurs instances de un ou plusieurs services de composants différents s'exécutent en parallèle dans le système

=== Sémantique opérationnelle ===

Sur une machine monoprocesseur, on a une seule action à la fois.

Non-déterminisme complet sur les instances de services.

=== Gestion de l'entrelacement pour les Pre/post ===

Pour limiter le non-déterminisme complet et permettre des vérifications statique, on doit mettre en place des mécanismes de séquences.

   * ininterruptible
     * niveau services : trop contraignant + vérifications statiques fortes
     * groupes d'actions : sections critiques
       * assertions
       * verrous
       * ...
   * service property : query/modify
   * protocole "fin" (découper le services en sections explicites). les sections sont des services.

   A décider



==== discussions sur Kml2B ====

  * mapping des types Kml en B
    * enum : SET ou not SET ?
    * struct : fonctions B d'accès 
   POINT -/-> int
   ou Point subseteq POINT
   +
   accès en modifications
   solution merge var_field : pb des variables en retour
    *

==== discussions sur COSTO ====

  * mapping des types déclarés : ATM_CORE.CashCard et USER_INTERFACE.CashCard