(rédigé par PA)

Présents : PA, GA, AL, MM

• voir notes MM

• 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

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

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

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

• 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 : ATMCORE.CashCard et USERINTERFACE.CashCard