Résumé de la discussion téléphonique avec JY

Pour JY : 
un automate synchrone et dissocié de sa machine d'exécution asynchrone qui gère ses entrées/sorties en fonction de stratégies.

{{:collaborations_recherche:univ_corte:automate_machine_exe_jy.jpg?200|}}

problème fondamentale de base 1: un automate synchrone ne s’exécute pas. C’est un modèle. C’est la machine d'exécution qui encapsule l’automate et qui va gérer les entrées/sorties asynchrones de celui. La machine d'exécution a donc des communications asynchrone avec son environnement. Cette encapsulation entraîne une explosion combinatoire qui amène à des systèmes complexe. Le problème est de savoir si le comportement de la machine d'exécution va rester conforme à ce que modélise l’automate encapsulé voir à des contraintes supplémentaires (propriétés).

position / existant: Il n’existe pas de travaux sur la machine d'exécution exhibée dans un certain nombre de stratégies différentes. Le problème de la gestion de l’automate synchrone et la gestion du déclenchement de son cycle d'exécution qui normalement ne doit pas être préempté (modèle atomique utilisé par les modèles checking). Il existe plusieurs stratégies possible pouvant être classées par famille comme :
déclenchement d’un cycle dès qu’un événement arrive sur l’automate;
déclenchement d’un cycle sur un certain type d’évènement;
etc...
Donner la possibilité de générer un composant asynchrone avec le choix de l’automate et de la stratégies de la machine d'exécution est un progrès en soit.
Il faut ensuite être en capacité de dire à l’utilisateur qu’avec tel stratégie on il peut avoir tel propriété.

proposition: L’idée est d’utiliser un formalisme pour éviter de faire à la main l’encapsulation pour vérifier des propriétés comportementales supplémentaires. A coté de la stratégies il faudra “un langage” pour exprimer les propriétés (à définir comme temporelle, intervalle, max, min) que l’on veut avoir. Le formalisme va nous aider à définir ces propriétés. Ces propriétés seront simuler pour valider les stratégies proposées plus tard au designer. Les stratégies devront être non application dépendantes (générique). 

qui choisi la stratégies: c’est le designer. C’est lui qui génère les composant et lorsqu’il choisi une stratégie il aura un ensemble de propriétés toujours valides. Dans N stratégies il y aura que n stratégies qui valide les propriétés.

la stratégie de machine d'exécution ne dépend pas de la sémantique de l’automate. 

problème fondamental 2: à partir de la connaissance de la sémantique de l’application (je sais que j’attaque une lampe, un chauffage, etc). Nous sommes dans la composition/fusion consistant à faire le produit d’automate synchrone qui amène à exprimer à définir les contraintes sous forme d’un nième automate (exemple de l’automate de la lampe avec un accès concurrent). Le résultat de la fusion est un automate synchrone qui possède à présent plusieurs entrées avec des accès concurrents. Le problème est le même que tout à l’heure. 

**Réflexion avec Souhila**

Une modèle atomique DEVS repose sur une description formel d’un automate à états finis. Cet automate représente à la fois l’automate synchrone et la machine d'exécution asynchrone. Une stratégie d’un modèle atomique DEVS est donc une expression particulière de ces fonctions de transition et de sa fonction de sortie. Dans le cas du problème 1 exprimé par JY consistant à proposé des propriétés permettant de sélectionner des stratégies générique, on peut penser à définir des propriétés basées sur les états et les événements en entrée du modèle DEVS. On peut par exemple proposer la stratégie “safe” qui consiste à exécuter l’automate du modèle DEVS de manière fidèle.  La stratégie ‘inverse’ à inverser l’automate du modèle DEVS. La stratégie ‘delayed’ à décaler dans le temps la transition des états. Pour l’exemple de la lampe:

stratégie ‘safe’ :
	if state=’on’ and ev=’off’ : state=’off’
	if state=’off’ and ev=’on’ : state=’on’
	if state=’on’ and ev=’on’ : state=’on’
	if state=’off’ and ev=’off’ : state=’off’

stratégie ‘inverse’ :
	if state=’on’ and ev=’off’ : state=’on’
	if state=’off’ and ev=’on’ : state=’off’
        if state=’on’ and ev=’on’ : state=’off’
	if state=’off’ and ev=’off’ : state=’on’

stratégie ‘delayed’ :
	if state=’on’ and ev=’off’ : state=’off after 2
	if state=’off’ and ev=’on’ : state=’on’ after 2
	if state=’on’ and ev=’on’ : state=’on’ after 2
	if state=’off’ and ev=’off’ : state=’off’ after 2

Ces stratégies peuvent être considérées comme génériques et de non composition. 
DEVS permet une représentation du temps de manière formel dans l’automate et permet donc de considéré cette propriété dans les stratégies d’exécution de la machine de l’automate.

Lorsqu’un modèle atomique DEVS est couplé à d’autre modèle  atomique ou couplé, nous avons affaire à une stratégie de composition de l’automate. Les collaborateurs de JY travaillent sur la fusion des automates sous contraintes. L’automate résultant peut donc être représenté par un modèle atomique et donc peut présenter les mêmes stratégies génériques.
Lorsque une stratégie particulière qui sort du cadre générique doit être implémentée, il faudra présenter les propriétés correspondantes au designer. Ce cas est présenter dans l’exemple de la lampe connecté avec l’interrupteur, le motion et le light sensor. 
Dans tout les cas, la simulation DEVS permettra de valider les stratégies correspondantes au propriétés attendue par le designer.

D’un point de vue de la conception : le concepteur utilise la modélisation et la simulation DEVS pour décrire et simuler le comportement de son composant. La simulation permet de valider les stratégies mises en place dans des fonctions séparées des fonctions de transition.

{{:collaborations_recherche:univ_corte:generation_strategies_par_sim_devsimpy.jpg?200|}}

D’un point de vue l’utilisation : le designer choisi les propriétés qu’il désire voir respecter par son composant connecté. Ensuite, un ensemble de stratégies correspondant aux propriétés son proposé au designer.