Site ELEC344/ELEC381

Partie interactive du site pédagogique ELEC344/ELEC381 de Télécom ParisTech (occurrence 2010).

Catégories

modèles et vérification

Non, ce n’est pas le titre d’un cours super intéressant (:D), mais bien ce que j’ai commencé cet après midi. Je me suis attelé à la tâche d’intégration des autres tâches qui tourneront sur la carte.

Il y a plusieurs sources de controle de la carte : entrée DMX, multiples boutons poussoirs. Il y a de même plusieurs facteurs qui peuvent nécessiter l’extinction immédiate du laser : surchauffe de l’un des galvanomètres, déconnection du cable ethernet pendant l’affichage d’une vidéo en streaming.
Le but est donc d’identifier et de centraliser les changements d’état courant dans une machine à états afin de faciliter la programmation dans les autres tâches, et de fournir des fonctions « sécurisées » comme enableLaser(), qui garantissent que l’état courant dans lequel se trouve le système autorise l’exécution d’une telle fonction.

Les états du système sont représentés comme l’ensemble des combinaisons des états suivants (extrait du code source):
typedef enum {DMXControl, localControl} controlInputMode;
typedef enum {ethernet, SDCard} dataInputMode;
typedef enum {present, absent} SDPresenceMode;
typedef enum {connected, unconnected} ethernetPresenceMode;
typedef enum {hot, cold} overheatMode;
typedef enum {idle, image, video, etc} runMode;
typedef enum {read, write, both} controlSDMode;
typedef enum {on, off} updateMode;
typedef enum {allowed, forbidden} enableLaserMode;
typedef enum {enabled, disabled} laserStateMode;

Un certain nombre de combinaisons de ces états sont incompatibles. Il faut donc développer un système de transitions qui garantisse qu’ils ne seront jamais atteints. Si j’ai le temps (dans une autre vie :) ) je pense valider le système de transitions en le codant en lustre et en utilisant un model checker (lesar je pense), mais ce n’est pas la priorité. Je pense que d’ici vendredi matin ca sera codé, en étant pas très efficace j’y ai passé 3h cet aprem et j’ai pas mal avancé.

Sinon j’ai regardé comment envoyer des fichiers ILDA en TCP vers la carte une fois qu’Etienne aura réglé l’ethernet, et j’ai trouvé un code client/serveur en C sur internet. Il faudra adapter le serveur pour qu’il utilise les fonctions de uip et ca sera bon.

1 comment to Modèles et vérification

  • Samuel Tardieu

    Sinon j’ai regardé comment envoyer des fichiers ILDA en TCP vers la carte une fois qu’Etienne aura réglé l’ethernet, et j’ai trouvé un code client/serveur en C sur internet. Il faudra adapter le serveur pour qu’il utilise les fonctions de uip et ca sera bon.

    Maintenant, faire un client-serveur TCP en C n’est pas bien difficile hein. N’oubliez pas que vous serez interrogés sur tout ce que vous utilisez, et qu’il faut faire attention aux licences des logiciels utilisés.