Ci-dessous, les différences entre deux révisions de la page.
Les deux révisions précédentes Révision précédente Prochaine révision | Révision précédente | ||
collaborations_recherche:univ_corte:minutes_161014 [2014/11/07 11:53] tigli [Minutes Meeting du 16/09/14] |
collaborations_recherche:univ_corte:minutes_161014 [2014/11/07 16:52] tigli [Minutes Meeting du 16/09/14] |
||
---|---|---|---|
Ligne 8: | Ligne 8: | ||
Problématique Générale : modéliser, simuler grâce à DEVS (Discrete Event System Specification) différentes stratégies de machine d'exécution d'automates synchrones (issus d'une modélisation synchrone du comportement) au coeur d'un composant logiciel type composant léger dans un environnement asynchrone d'exécution. | Problématique Générale : modéliser, simuler grâce à DEVS (Discrete Event System Specification) différentes stratégies de machine d'exécution d'automates synchrones (issus d'une modélisation synchrone du comportement) au coeur d'un composant logiciel type composant léger dans un environnement asynchrone d'exécution. | ||
- | Pb 1 : Modéliser / Simuler des stratégies de machine d'exécution quelque soit l'automate. (langage) | + | ** Pb 1 ** : Modéliser / Simuler des stratégies de machine d'exécution quelque soit l'automate. |
- | Défi 1 : Valider l'implémentation asynchrone du modèle synchrone de comportement dans un composant asynchrone | + | |
+ | ** Défi 1 ** : Valider l'implémentation asynchrone du modèle synchrone de comportement dans un composant asynchrone. Faut-il un langage d'expression des con | ||
Les stratégies modélisées / simulées ne dépendent pas de l'automate et son modèle (pas de connaissance sur la sémantique de l'application) | Les stratégies modélisées / simulées ne dépendent pas de l'automate et son modèle (pas de connaissance sur la sémantique de l'application) | ||
Ligne 15: | Ligne 16: | ||
- | Pb 2: Gérer la composition/ fusion de deux composants asynchrones dont le comportement est modélisé par deux automates synchrones. | + | ** Pb 2 **: Gérer la composition/ fusion de deux composants asynchrones dont le comportement est modélisé par deux automates synchrones. |
- | Défi 2 : Validé et Généré le composant résultat | + | |
+ | ** Défi 2 **: Validé et Généré le composant résultat | ||
Deux pistes : | Deux pistes : | ||
* La composition est faite au niveau des modèles synchrones : le modèle synchrone du composant résultat est le produit des automates des composants à composer/fusionner x automate des contraintes à la fusion | * La composition est faite au niveau des modèles synchrones : le modèle synchrone du composant résultat est le produit des automates des composants à composer/fusionner x automate des contraintes à la fusion | ||
+ | * Exemple : un automate de modélisation d'un lampe est à 2 états et deux entrées : on / off, le produit en cas de modélisation de deux accès concurrents, on le modélise par le produit des 2 automates : | ||
* Le problème pour la partie asynchrones est seulement celle du Pb1 | * Le problème pour la partie asynchrones est seulement celle du Pb1 | ||
* La composition est gérée dans les accès concurrents dans la machine d'exécution, multi-automates, sans en tenir compte dans l'automate | * La composition est gérée dans les accès concurrents dans la machine d'exécution, multi-automates, sans en tenir compte dans l'automate | ||
Ligne 28: | Ligne 31: | ||
- | +++++++++++++++++ | ||
- | |||
- | Ex. | ||
- | mes entrées sont on1 / on2 / off 1 / offé pour 2 accès | ||
- | |||
- | ces mon produit d'automate avec ses contraitnes ajoutées : ex : on1-off2 | ||
- | => on et on2-oof1 => on | ||
- | qui va résoudre la compostion | ||
- | validatation par model checking sur l'automate résultatnt | ||
- | |||
- | |||
- | B> résoudre les contraintes de la coposition liées aux accés concurrents | ||
- | dans la mahcine d'exécution sans en tenir copte dans l'automate | ||
- | Je dépose dans la stratégie de la machine d'exécution, en plus des | ||
- | asppects génréqes (ex. DT entre deux décleanchment ... , donc tout | ||
- | quelque soit le dispotif), des contraintes sur la génération des | ||
- | événmrents d'entrée de l'automate liées à la sémnatinwque du dispostif | ||
- | : on1 - off2 => on | ||
- | on2 - off1 => on |