Velo - Vérification pour l'Environnement et le LOgiciel

Cette page est en lecture seule. Vous pouvez afficher le texte source, mais ne pourrez pas le modifier. Contactez votre administrateur si vous pensez qu'il s'agit d'une erreur.

====== 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

Velo - Vérification pour l'Environnement et le LOgiciel

Outils pour utilisateurs

Outils du site

Outils de la page