Projet TOAST
Réunion du 3 mai 2007
Deuxième réunion :
Cette réunion informelle a eu lieu à la bibliothèque du LSV le jeudi 3 mai 2007 de 11h à 11h30.Participants :
|
|
Compte-rendu de la réunion :
- L'objectif de cette réunion intermédiaire était que Thomas et Nicolas
présentent à Marc un modèle construit avec l'outil UppAal TiGa.
Ce modèle, un peu amélioré entre temps, est décrit ci-dessous.
Le modèle représente un système de deux émetteurs. Chaque émetteur est composé
d'un module représentant l'état, éteint ou allumé, du module, ainsi que d'un
module gérant la puissance d'émission. Lorsqu'il s'allume, l'émetteur
l'indique aux autres émetteurs (via le message e[id]! où id
est l'identifiant de l'émetteur) ainsi qu'à son module de puissance (via
d[id]!). Lorsqu'il s'éteint, il ne l'indique qu'à son module de
puissance (via c[id]!). On impose que le système n'oscille pas trop
entre les états éteint et allumé avec les conditions sur l'horloge x (qui mesure le temps écoulé dans chaque état).
Le module de puissance est lui aussi composé de deux états (du moins dans la
représentation graphique).
L'état initial correspond à l'état éteint, et l'autre état représente l'état
allumé. Dans ce deuxième état, la puissance peut varier de manière discrète,
en prenant des valeurs entières entre 0 et 50.
Lorsque ce module reçoit le signal lui indiquant de
s'allumer, il fixe la puissance à une valeur I donnée, et arrive dans le deuxième état, où plusieurs actions sont possibles :- il peut augmenter sa puissance d'émission : cela n'est possible que si un temps suffisant (delay) s'est écoulé, et si cette augmentation se justifie par un rapport signal sur bruit trop faible.
- de la même façon, il peut diminuer la puissance si le rapport signal sur bruit est trop élevé. De cette façon, l'émetteur essaye de rester avec des valeurs raisonnables de ce rapport signal sur bruit, entre deux bornes données.
- enfin, si un autre émetteur se met en marche, l'émetteur courant
doit baisser sa puissance
(à une valeur
J fixée) afin de laisser la nouvelle communication s'établir.
Chacune des valeurs des paramètres peut être modifiée facilement.
L'outil Uppaal TiGa permet ensuite de faire une simulation interactive du système ainsi construit. On peut ainsi constater informellement que le système se comporte de manière correcte, que la puissance d'émission se stabilise, ...
Enfin, l'outil de vérification permet de s'assurer de manière formelle que le comportement est correct. On vérifie ainsi les propriétés suivantes :
- le long de toute exécution, la puissance d'émission reste bornée : elle ne dépasse jamais la valeur 21. Lorsque les deux émetteurs sont en marche, la différence de puissance reste assez faible (ce qui indique qu'aucun des émetteurs ne prend le dessus sur l'autre).
- il est possible, pour l'un des modules, de se mettre en marche, quoi que
fasse l'autre module. Cette propriété est évidente, mais pourrait ne pas être
vérifiée si le modèle n'est pas construit correctement (problèmes de
synchronisation des différents modules).
- on peut vérifier qu'un émetteur peut s'arranger pour avoir un rapport signal sur bruit supérieur à une valeur donnée, et ce, quoi que fasse l'« adversaire ».
- enfin, on peut vérifier qu'il existe une stratégie pour que, quoi que fasse l'adversaire, lorsqu'un émetteur est en marche, le rapport signal sur bruit est toujours supérieur à une valeur seuil.
On a donc obtenu un modèle très simplifié, mais réaliste, dans lequel deux émetteurs équivalents peuvent cohabiter sans problème. On peut envisager plusieurs extensions de cette modélisation :- donner plus de pouvoir à l'adversaire : on pourrait lui donner la possibilité de moduler sa puissance indépendamment de celle des autres, de s'allumer et s'éteindre quand il le veut, et éventuellement sans en informer les autres émetteurs...
- ...
