# Comment choisir son outil d'analyse de systèmes à événements discrets ?

Pascal Andre, Aurélien Pageot, Orlann Cailleau, Charbel Bedran

► To cite this version:

Pascal Andre, Aurélien Pageot, Orlann Cailleau, Charbel Bedran. Comment choisir son outil d'analyse de systèmes à événements discrets?. Modélisation des Systèmes Réactifs (MSR'25), CReSTIC et LICIIS, Nov 2025, Reims (51), France. hal-05384903

HAL Id: hal-05384903

https://hal.science/hal-05384903v1

Submitted on 27 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Comment choisir son outil d'analyse de systèmes à événements discrets ?

Pascal André<fnref n="1" />, Aurélien Pageot<fnref n="2" />, Orlann Cailleau<fnref n="2" />, and Charbel Bedran<fnref n="2" />

## Résumé

Lorsqu'on veut étudier la dynamique d'un système de manière méthodique, la première étape est de choisir le formalisme et l'outil qui permettront de modéliser le système, vérifier ses propriétés et/ou le simuler et examinant les traces d'exécution. Ce papier contribue à répondre à cette question en proposant une grille d'évaluation des outils sur quatre thèmes. Le comparatif réalisé sur quelques études de cas, ne se veut pas exhaustif mais représentatif des approches pour illustrer la démarche. Il pourra être enrichi collaborativement à la fois sur les outils et les études de cas.

# 1 Introduction

En ingénierie des systèmes, on s'appuie sur des modèles pour comprendre et mettre en œuvre des systèmes complexes (concurrents, distribués, temps-réels, embarqués). On s'intéresse ici, en particulier, à des systèmes de contrôle (contrôle/commande comme des feux de circulation, processus de production, domotique...) sous l'angle particulier des systèmes à événements discrets (SED). La question essentielle devient alors quelle approche/outil faut-il utiliser pour étudier (modéliser, analyser, tester) le système cible ? C'est celle que nous nous posons tous face au problème. Pour y répondre, il est nécessaire alors de (i) faire un état de l'art des formalismes et outils permettant de modéliser efficacement des modèles de systèmes dynamiques et pour le valider, (ii) de créer un benchmark comparatif des outils et formalismes pour identifier chaque avantages et inconvénients de chacun en fonction des besoins d'ingénierie.

Nous contribuons modestement à ce travail de synthèse en posant une première brique. Ce papier traite d'outils permettant de traiter des systèmes de contrôle à événements discrets tels que des simulateurs, des Réseaux de Pétri (RDP), des automates ou des algèbres de processus, en mettant en lumière leurs caractéristiques. À travers des études de cas concrètes, nous évaluerons la capacité de ces outils à simuler des systèmes de contrôle et à vérifier leurs propriétés. L'objectif est de fournir une comparaison étayée des outils testés sur leur expressivité, la vérification de propriétés et la simulation. Ayant une vision empirique, nous n'avons pas la prétention d'être exhaustifs ni en largeur sur la variété des outils ni en profondeurs sur la finesse des caractéristiques prises en compte. Par exemple, le temps peut s'interpréter différemment d'une approche à l'autre. De même, le benchmark s'appuie sur trois cas, il n'est pas suffisamment représentatif. Notre idée est que ce travail soit enrichi par d'autres contributeurs.

L'article est organisé comme suit. Nous commençons par introduire les éléments de la méthodologie dans la section 2. Nous détaillons les études de cas support d'expérimentation (section 2.1), les formalismes et outils (section 2.2), la vérification de propriétés (section 2.3), et les outils sélectionnés (section 2.4) pour les expérimentations. Les expérimentations sont décrites dans la section 3 : l'application des outils au cas (section C) et les résultats du benchmark (section 4). Nous discutons de ces résultats en section 5 avant de conclure. Ces travaux étant empiriques, nous proposons une annexe en ligne <fnref n="1" /> pour plus de détails.

<footnote n="1">¹ LS2N CNRS UMR 6004 - Nantes Université- pascal.andre@ls2n.fr</footnote>

<footnote n="2">² Master ALMA - LS2N - Nantes Université- {firstname.lastname}@etu.univ-nantes.fr</footnote>

<footnote n="1">1. https://uncloud.univ-nantes.fr/index.php/s/KjgZJx2BeXwXNZq</footnote>
# 2 Méthodologie

La méthodologie utilisée pour construire un benchmark comparatif est la suivante : (i) définition des études de cas (exemples de systèmes de contrôle) (ii) sélection des approches et outils candidats (critères de sélection), (iii) sélection des caractéristiques retenues pour chaque approche (critères de comparaison), (iv) application aux études de cas. Les études de cas décrivent l'espace du besoin tandis que les approches décrivent l'espace de la solution. Nous aurions pu choisir une approche plus rationnelle visant à définir les caractéristiques du besoin et les caractéristiques des solutions puis définir une relation entre les deux. Cela semble bien complexe et au delà des motivations initiales.

## 2.1 Etudes de cas

Les outils ont été testés sur trois cas d'études avec des besoins de modélisation, vérification et simulation variables qui illustrent les besoins que l'utilisateur (ingénieur) peut avoir. (1) Le premier cas est le contrôle des feux de circulation à un carrefour avec des propriétés de sûreté de fonctionnement et de vivacité (safety & liveness). (2) Un cas de processus de production simplifié organisé en Kanban. (3) Le troisième cas d'étude consiste en une boucle de convoyeurs qui bloquent des palettes à chaque poste pour un traitement ou pas des produits dans un système de production fictif (performance). Le premier cas est typique d'une organisation par flot de contrôle tandis que les deux autres sont de type flots de données.

Nous aurions pu prendre des cas classiques de contrôle distribué comme le 'producteur/con sommateur', rendez-vous, 'lecteurs/écrivain'. Nous avons souhaité des cas concrets, et les feux tricolores ou le cas Kanban sont simples et compréhensibles par tous. Nous disposons d'une base de modèles (automates synchronisé, RDP, UML...) pour nos enseignements qui ont permis de nous focaliser sur les outils et non les modèles. Ces deux cas sont des cas simplifié d'automate qui possèdes très peu de places/états ainsi que des arcs/transitions. Concernant le cas n°3, c'est un cas pour lequel nous disposons d'un modèle FlexSim réalisé par un collègue spécialiste, qui nous permet de comparer avec les autres approches. Pour des raisons de place, ces cas et leur motivation sont détaillés dans la Section A de l'annexe web¹. Nous n'avons pas considéré ici la vérification de logiciels ou d'architecture matérielles, domaines d'application d'une partie des outils de vérification formelle mentionnées dans la section suivante.

## 2.2 Approches SED et outils candidats

Deux approches semblent pertinentes, (1) les outils de vérification formelle et (2) les simu-lateurs à événements discrets. Des détails sont apportés en Section B de l'annexe ¹.

Les outils de **vérification formelle** de formalismes classiques comme les automates (ou systèmes de transitions) [BBL+99], réseaux de Petri [GV03] et algèbres de processus [CRS18]. Ces formalismes sont très abstraits, vis-à-vis des concepts des cas d'étude (contrairement à l'autre catégorie) mais bénéficient de nombreux travaux théoriques et des outils Les réseaux de Petri (RDP) et certains types d'automates sont visuels et donc plus conviviaux. Les algèbres de processus sont plus algorithmiques et familières pour les informaticiens. Il existe de nombreuses variantes (et théories sous-jacents) e.g. avec ou pas de types de données, de temps, des gardes, d'actions, de non-déterminismes, de probabilités... L'expressivité du langage de modélisation en dépend. Bérard et al. [BBL+99] proposent un éventail de langages et outils pour la modélisation et la vérification par *model-checking* de la dynamique des systèmes réactifs tels que SMV — Symbolic Model Checking, SPIN — Communicating Automata, DESIGN/CPN — Coloured
Petri Nets, UPPAAL — Timed Systems, KRONOS — Model Checking of Real-time Systems, HYTECH — Linear Hybrid Systems. On trouve aussi nuSMV ou DEVS.

Les outils de **simulation de flux** comme AnyLogic ou FlexSim [Nor03] sont pratiques dans le domaine de la modélisation de processus de production industrielle, mais sont aussi lourds à appréhender. La création d'un nouveau modèle de chaîne de production demande beaucoup de ressources tant pour la structure détaillée que la description du comportement dynamique. Ces outils sont puissants et permettent de définir des scénarios de simulation, les étalonner et comparer les performances aussi chronophage et nécessite de l'expérience, qu'on ne trouve pas forcément sur les lieux de production notamment les PME-PMI. Un inconvénient crucial est le manque d'outils de vérification formelle. Enfin, et ce n'est pas négligeable, ils ne s'adaptent pas simplement à d'autres contextes comme le contrôle de processus réels-réel ou de systèmes embarqués. De ce fait nous ne les avons pas inclus à ce stade dans le comparatif.

## 2.3 Analyse des Propriétés

Les modèles dont nous traitons ici sont des spécifications formelles [GMBS96] dont l'intérêt est de pouvoir démontrer formellement des propriétés. Trois approches sont possibles : l'analyse statique qui consiste à explorer le modèle (structure et caractéristiques, types et espace d'état...), la preuve par théorèmes (il faut une structure logique sous-jascente au modèle) et l'analyse dynamique qui explore ses comportements dans le temps (évolution dans le temps, analyse de traces par exemple, simulation sous certaines hypothèses). Le model checking [BBL+99] est ainsi une technique de preuve formelle automatique<fnref n="2" /> qui explore un espace d'état pour démontrer une propriété donnée. Elle est adaptée à l'étude (des propriétés) de la dynamique des systèmes.

Plus le formalisme est expressif, plus il est difficile à vérifier formellement et statiquement des propriétés, on se tourne alors vers le test et la simulation, qui fonctionnent sous certaines conditions. Noter, et c'est fondamental, qu'on doit spécifier formellement on seulement le modèle du système mais aussi les propriétés attendues et il y a des langages pour cela, notamment les logiques temporelles [BBL+99] qu'on utilise pour explorer les traces d'exécution. Nous détaillons notre approche de la vérification dans la Section B.5 de l'annexe web¹.

## 2.4 Approches et outils sélectionnés

Pour sélectionner les outils du comparatif, les critères suivants sont retenus : (i) outils gratuit disponible, (ii) notoriété, (iii) ergonomie, (iv) représentativité (couverture), (v) modularité des spécifications, (vi) techniques de vérification, (vii) documentation... Nous avons commencé par des outils conviviaux comme Tina ou Romeo avant de nous attaquer aux autres. Nous avons sélection au moins un outil dans chaque sous-catégorie RdP (Romeo [GLMR05], Tina [BRV04], CPN Tools [RWL+03]), Automate (UPPAAL [BLL+96]), Algèbres de processus (SPIN [Hol04]). Nous avons aussi fait des tests avec Renew, Imitator, Itemis et JFLAP. Nous détaillons les outils dans la Section B.6 de l'annexe web¹.

# 3 Expérimentations

Nous avons expérimenté les études de cas avec différents outils de modélisation et de vérification dédiés à la vérification formelle de la dynamique des systèmes. Entre autres, nous avons

<footnote n="2">2. La preuve est aussi partiellement automatisée par des *theorem provers*, mais l'humain doit généralement intervenir dans la construction de la preuve.</footnote>
expérimenté avec des outils de réseaux de Petri (Tina, Romeo, CPN tools), des automates communs (UPPAAL), ou des processus (SPIN). Pour des raisons de places nous nous illustrons nos expériences sur le cas d'étude n°3 avec Tina pour les RdP et UPPAAL pour les automates. Tina a été choisi car il met en oeuvre simplement la vérification et la simulation avec horloge centralisée. Le reste est disponible dans la Section C de l'annexe web¹. Dans ce qui suit, nous illustrons nos expériences avec le cas n°3 et un outil de chaque catégorie.

## 3.1 Cas d'étude A.3 avec un RDP sur Tina 3.4.4

Le cas est décrit plus précisément dans la Section A.3 de l'annexe web¹. Une boucle de plusieurs convoyeurs alimente chaque poste. Le poste 1 place deux produits sur la palette. Le poste 2 (resp. 3) en prend 1 et le replace ailleurs sur le convoyeur. Une fois les deux produits déposés, la palette avance au poste 4 qui les stocke.

Le RDP temporisé de la Figure 1 modélise chaque élément décrit dans le cas d'étude. Bien que le système soit représenté comme un réseau unique, nous l'avons conçu par parties que nous avons ensuite assemblé par fusion/ajout de places ou de transitions <fnref n="3" />. Sur la Figure 1 nous avons ajouté des commentaires graphiques pour identifier les parties. On y voit plus distinctement les 4 postes ainsi que les 5 convoyeurs qui forment le convoyeur circulaire <fnref n="4" />.

<figure><img src="image_2.png" /><figcaption>FIGURE 1 – Troisième cas d'étude modélisé sur Tina</figcaption></figure>

Chaque convoyeur est composé de 5 places pour 5 emplacements de palettes, chaque place d'un convoyeur dispose d'une place de garde supplémentaire permettant de limiter le passage des palettes. Cette garde empêche les palettes de se superposer dans le système en créant une file de palettes. Le temps est ajouté à chaque transition indiquant la durée de chaque

<footnote n="3">3. C'est une technique de base commune aux RdP. D'autres outils permettent de représenter différemment cet assemblage : par exemple on utilise des variables partagées de marquage dans Romeo (cf. Section C.9 de l'annexe web¹) alors que dans CPN Tools (cf. Section C.6 de l'annexe web¹) le réseau est hiérarchique comme un arbre et on peut en développer les branches. Ainsi, une "substitution transition" est une transition définie par un sous-réseau (subpage) on a aussi des "fusion sets" pour éviter la multitude d'arcs dans un graphe planaire.</footnote>

<footnote n="4">4. Dans un système industriel, une boucle de convoyage automatisée n'est pas faite d'un seul tenant, elle est modulaire et donc extensible ; des connecteurs permettent de brancher les sections pour faire circuler les fluides (électricité, huile, gaz...).</footnote>
étape. Tina n'utilisant que le formalisme des jetons simples le flux des palettes sans objets se déroule avec un seul jeton et une fois que deux objets sont sur les palettes ce sont deux jetons qui se déplacent simultanément de place en place. Chaque poste nécessite une garde pour simuler un bloqueur et permettre le blocage des palettes. (i) Au premier bloqueur, la palette attend que deux objets soient déposés dessus avant de pouvoir passer au convoyer suivant. (ii) Au deuxième bloqueur, l'opérateur 1 prend un objet, puis la palette est libérée (iii) Au troisième bloqueur, l'opérateur 2 prend un objet, puis la palette attend que les objets traités par les opérateurs 1 et 2 soient replacés sur la palette. (iv) Au quatrième bloqueur, la palette est vidée grâce au transporteur, puis elle retourne dans le cycle. Le RDP dispose également de deux emplacements supplémentaires : l'un pour choisir le nombre de palettes dans le système (source1), et l'autre pour choisir le nombre d'objets à traiter (source2).

Une fois le système modélisé avec Tina, il est possible d’en vérifier des propriétés grâce au
outils (structural analysis, reachability analysis, checker). Par exemple, la Figure 2 montre
l’analyse de la structure d’un RDP par Tina avec le nombre de places, transitions, arcs ainsi
pour chaque transitions du modèle est indiqué ces places d’entrées et de sorties associés.

<figure><img src="image_3.png" /><figcaption>FIGURE 2 – Analyse de la structure du RDP du troisième cas d'étude modélisé sur Tina</figcaption></figure>

La figure 3 indique quant à elle un des résultats d'une vérification des état du RDP. Cette vérification diffère en fonction de beaucoup de paramètres. Ici, il est possible d'identifier plusieurs propriétés comme la vivacité. Lorsqu'on calcule le graphe de marquage, on dispose explicitement de l'espace d'état sous forme d'un automate, on obtient ici 299 états sur cette versions (et 466 sur la version dont le graphe est représenté en Figure 14 de l'annexe web¹).

<figure><img src="image_4.png" /><figcaption>FIGURE 3 – Analyse de l'espace d'état (graphe de marquage) du cas d'étude avec Tina</figcaption></figure>

Concernant la simulation (cf. Figure 4), l'intérêt de Tina par rapport aux autres outils testés est qu'il conserve une horloge globale de simulation pour le temps. Il permet de plus de simuler pas à pas ou globalement. En tenant compte d'une règle aléatoire pour les intervalles de temps, on obtient un temps de simulation, ici on obtient 342 avec 3 palettes et 10 produits.
<figure><img src="image_5.png" /><figcaption>FIGURE 4 – Cas d'étude simplifié traité avec Tina</figcaption></figure>

## 3.2 Cas d'étude A.3 avec un automate sur UPPAAL

Par nature, les automates (ou *finite state machines*) suivent une approche modulaire et distribuée. Deux modes d'interactions sont courants^5 : (i) *implicite* par variables partagées. Les automates n'échangent pas directement, c'est leur contexte qui varie. On retrouve les problèmes classiques de condition de verrouillage d'accès en lecture/écriture pour conserver la cohérence des valeurs. L'horloge globale dans une simulation ou une exécution peut-être considérée ainsi. (ii) *explicite*, les automates interagissent par synchronisation seule ou par communication (asynchrone par envoi de message dans une boite aux lettres, synchrone par des canaux de communication). Dans les deux cas, l'interaction peut être pair-à-pair ou généralisée (*broad-casting* pour les messages). Par exemple, MEC [Arn90] est un *model-checker* pour automate synchronisés sur les étiquettes de transitions par des vecteurs de synchronisation et le produit synchronisé des automates. Dans les Statecharts, les messages sont envoyés en synchrone et les événements en asynchrone. En UPPAAL, deux automates communiquent (et se synchronisent) par des messages sur un canal. Les variables globales sont partagées.

Comme illustré par la Figure 5, le système est structuré en 15 automates : 4 forment le convoyeur et 5 bloquent les palettes entre le convoyeur et le poste de travail permettant d'attendre que le poste est fini sont action avant de laisser la palette avancée. Les 4 derniers sont dédiés aux postes de travail : (i) Poste 1 : Un robot charge deux objets un par un sur la palette

<footnote n="5">5. Noter que les approches par processus communicants *e.g.* avec SPIN ou CADP fonctionnent sur les mêmes principes.</footnote>
<figure><img src="image_6.png" /><figcaption>FIGURE 5 – Troisième cas d'étude modélisé sur UPPAAL</figcaption></figure>

bloquer en attendent les objets (encadré en rouge). (ii) Poste 2 : Un opérateur récupère un objet d'un premier bloqueur, le dépose dans une machine pour traitement, puis le replace sur la palette bloquer au seconde bloqueur (encadré vert). (iii) Poste 3 : Un opérateur récupère un objet du bloqueur, le dépose dans une machine pour traitement, puis le replace sur la palette (encadré vert). (iv) Poste 4 : Un transporteur récupère les objets de la palette bloquer pour les déposer dans un dépôt (encadré en jaune). Enfin, les deux derniers automates permettent de sélectionner le nombre de palettes et d'objets à faire circuler dans la chaîne de production, assurant ainsi l'arrêt de l'automate lorsqu'il n'y a plus d'objets à traiter (encadré en violet).

Une fois modélisé, on vérifier des propriétés du système comme la sûreté et la vivacité dans l'onglet vérification d'UPPAAL. On peut observer sur la Figure 28 de l'annexe web¹) que les propriétés vérifié sont signalées en vert et en rouge celles dont la vérification a échoué. Pour la simulation, nous avons obtenu la trace d'exécution de la Section C.12 de l'annexe web¹).

## 4 Synthèse des résultats préliminaires

Pour évaluer les différents outils de modélisation et de vérification formelle, un ensemble de critères de comparaison a été défini et regroupé en quatre grandes parties : 1. généralités, 2. expressivité du langage, 3. potentiel de vérification, 4. potentiel de simulation. Notre proposition de benchmark est détaillée dans les sections suivantes. Nous utilisons des codes pour visualiser le résultat : — **vert** (caractéristique présente, facilité d'accès), — **orange** (fonctionnalité réduite ou accès délicat), — **rouge** (caractéristique absente, difficulté d'accès).
## 4.1 Généralités

Cette partie s'intéresse au caractéristiques générales des outils et leur *accessibilité*. Nous vérifions les accès, droits et licences. L'interaction *homme-machine* est ensuite évaluée en terme d'ergonomie et de convivialité. L'aide en ligne et la documentation sont indispensables pour mener une analyse SED. La capacité à ajouter des *plugins ou extensions* est également prise en compte pour étendre les fonctionnalités de base. L'analyse inclut la possibilité d'importer ou d'exporter des modèles pour les réutiliser ou les exploiter dans d'autres outils. Enfin, la génération automatique de code est examinée pour voir si l'outil peut produire des programmes exécutables directement à partir des modèles. La Table 1 compare l'échantillon d'outils de modélisation et vérification formelles selon plusieurs critères. Les outils sont classés par formalisme. Nous avons retenus les outils gratuits téléchargeables. Il se distinguent par leur interface homme-

<table><caption>TABLE 1 - Liste des outils envisagés</caption><thead><tr><th rowspan="2"></th><th colspan="5">Composants/Environnements</th></tr><tr><th>Téléchargement</th><th>Ergonomie</th><th>Extensions</th><th>Imports/Exports</th><th>Génération de code</th></tr></thead><tbody><tr><td><strong>RDP</strong></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>Tina</td><td>Facile, Gratuit, sur leur site web</td><td>Facile, Éditeur graphique et éditeur textuel</td><td>Moyen, Vous pouvez ajouter votre code de vérification de modèle</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Vous ne pouvez pas générer de code à partir de cet outil</td></tr><tr><td>Romeo</td><td>Facile, Gratuit, sur leur site web</td><td>Facile, Éditeur graphique</td><td>Non, Vous ne pouvez pas ajouter d'extensions à l'outil</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Vous ne pouvez pas générer de code à partir de cet outil</td></tr><tr><td>CPN Tools</td><td>Facile, Gratuit, sur leur site web</td><td>Facile, Éditeur graphique</td><td>Non, Vous ne pouvez pas ajouter d'extensions à l'outil</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Vous ne pouvez pas générer de code à partir de cet outil</td></tr><tr><td>Renew (Reference Net Workshop)</td><td>Facile, Gratuit, sur leur site web</td><td>Moyen, Éditeur graphique et textuel</td><td>Oui, Supporte les extensions</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Pas de génération de code</td></tr><tr><td><strong>Processus</strong></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>SPIN promela</td><td>Facile, Gratuit, sur leur site web</td><td>Non, il ne fournit pas de support spécifique pour les interfaces utilisateurs interactives ou l'interaction directe homme-machine</td><td>Moyen, SPIN supporte les extensions via des scripts personnalisés ou des outils supplémentaires, mais ce n'est pas aussi flexible</td><td>Moyen, en utilisant des formats spécifiques, mais ce n'est pas aussi flexible que certains autres outils en termes de capacités générales d'import/export</td><td>Non, il génère du code C pour la vérification, mais pas pour la génération de code général ou au niveau de l'application</td></tr><tr><td><strong>Automate</strong></td><td></td><td></td><td></td><td></td><td></td></tr><tr><td>UPPAAL</td><td>Facile, Gratuit, sur leur site web</td><td>Moyen, L'éditeur graphique est facile mais l'éditeur textuel est complexe à comprendre</td><td>Non, Vous ne pouvez pas ajouter d'extensions à l'outil</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Vous ne pouvez pas générer de code à partir de cet outil</td></tr><tr><td>Imitator</td><td>Moyen, Nécessite Linux pour l'installation</td><td>Facile, Éditeur graphique</td><td>Non, Vous ne pouvez pas ajouter d'extensions à l'outil</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Non, Vous ne pouvez pas générer de code à partir de cet outil</td></tr><tr><td>Itemis Create/Yakindu Statechart Tools</td><td>Facile, licence graphique sur le site web et licence professionnelle avec plus de fonctionnalités</td><td>Facile, Éditeur graphique et textuel</td><td>Oui, Supporte les extensions</td><td>Facile, Les modèles peuvent être importés et exportés</td><td>Oui, Génération de code possible</td></tr><tr><td>JFLAP</td><td>Facile, Gratuit, sur leur site web avec formulaire</td><td>Facile, Interface utilisateur intuitive</td><td>Non, Pas de support pour les extensions</td><td>Facile, Supporte les formats d'import/export</td><td>Non, Pas de génération de code</td></tr></tbody></table>
machine et sa qualité ergonomique. Certains outils proposent des interfaces graphiques facilitant la modélisation et les interactions intuitives, tandis que d'autres privilégient une approche textuelle via l'ajout de scripts ou des prompts. Le Table 1 permet de voir rapidement quels outils étaient faciles à utiliser et assez complets en fonctionnalités. Cette comparaison générale inclut les outils que nous avons testé 6 mais seule une partie est retenue pour les expérimentations plus détaillée qui suivent. Certains outils ont été écartés en raison de leur complexité d'installation, de leur difficulté d'utilisation, ou de leurs limitations fonctionnelles.

## 4.2 Expressivité du langage

L'objectif est d'évaluer jusqu'où les langages utilisés par les outils peuvent aller dans la modélisation. La gestion du temps est essentielle dans les systèmes temps réel : certains outils utilisent des horloges explicites (comme UPPAAL), d'autres intègrent le temps de manière plus limitée. La communication entre processus est également importante, certains outils supportant des canaux de communication ou des échanges de messages. La prise en compte de la probabilité dans les modèles est plus rare, mais importante dans des contextes d'incertitude. Les outils permettent d'imposer des conditions sur les transitions, mais avec des niveaux de complexité différents. La modularité permet de construire des modèles plus grands en assemblant plusieurs petits morceaux. Cela aide à mieux organiser le travail et à réutiliser des parties du modèle. Enfin, la possibilité de définir des couleurs (types complexes pour les jetons) ou d'utiliser des objets enrichit fortement l'expressivité, mais n'est pas systématiquement présente.

<table><caption>TABLE 2 – Comparaison des outils (Modélisation / Expressivité)</caption><thead><tr><th rowspan="2"></th><th colspan="5">Modélisation</th><th rowspan="2">Types</th></tr><tr><th>Temps</th><th>Communications</th><th>Probabilité</th><th>Conditions</th><th>Modularité</th></tr></thead><tbody><tr><td>Tina</td><td>Oui, le temps peut être ajouté sur les transitions et est supporté dans l'outil</td><td>Non, mais cela peut être simulé par des transitions</td><td>Non, il n'y a pas de probabilité</td><td>Non, il n'y a pas de conditions</td><td>Non, il n'y a pas de modularité</td><td>Non, seulement des jetons bâsiques</td></tr><tr><td>Romeo</td><td>Oui, le temps peut être ajouté sur les transitions mais ne sert qu'à prendre toutes les transitions avant d'avancer</td><td>Moyen, les communications peuvent être créées avec l'aide de variables et de bloqueurs</td><td>Non, il n'y a pas de probabilité</td><td>Oui, des conditions peuvent être ajoutées aux transitions</td><td>Oui, il y a de la modularité</td><td>Non, seulement des jetons bâsiques</td></tr><tr><td>CPN Tools</td><td>Moyen, le temps peut être ajouté aux jetons, les transitions, les arcs. Mais seulement en N</td><td>Non, mais cela peut être simulé par des transitions</td><td>Oui, utilisable avec certaines fonctions de distribution aléatoire</td><td>Oui, des conditions peuvent être ajoutées aux transitions</td><td>Non, il n'y a pas de modularité</td><td>Oui, des objets peuvent être définis et utilisés comme jetons</td></tr><tr><td>SPIN promela</td><td>Moyen, le temps peut être simulé, mais il n'est pas intégré nativement</td><td>Oui, communications via des canaux</td><td>Non, il n'y a pas de support natif pour la probabilité, seulement pour le non-déterminisme</td><td>Oui, supporté via des structures de contrôle comme if, for, while, et des gardes</td><td>Oui, il y a de la modularité</td><td>X</td></tr><tr><td>UPPAAL</td><td>Moyen, le temps peut être ajouté par des variables ou par un type d'horloge</td><td>Oui, communications via des canaux peuvent être faites</td><td>Non, il n'y a pas de probabilité</td><td>Oui, des conditions peuvent être ajoutées aux arcs</td><td>Oui, il y a de la modularité</td><td>X</td></tr></tbody></table>

<footnote n="6">6. La sélection n'est ni exhaustive ni représentative des meilleurs outils.</footnote>
La Table 2 permet de voir la couverture par les outils des besoins de modélisation comme la gestion du temps, la possibilité de faire des communications entre les parties concurrentes, l'ajout des conditions sur les transitions, l'utilisation de types plus riches (couleurs ou objets dans les RDP), paramètres. La richesse du langage de calcul fonctionnel (familier aux informaticiens) est un atout de même que l'accessibilité du formalisme à des non spécialistes. Tous les outils n'offrent pas la même expressivité ou la même richesse en termes de concepts. Certains comme UPPAAL, utilisent des horloges pour représenter le temps, tandis que d'autres le gère de manière plus limitée. La communication entre processus est également mieux supportée dans des outils comme Romeo, UPPAAL et SPIN. En revanche, la prise en compte de la probabilité est très rare et elle est intégrée que sur CPN Tools. Enfin, les gardes sur les transitions sont possibles dans de nombreux outils mais leur manière d'être exprimées varie selon environnement.

## 4.3 Vérification

Cette rubrique étudie les capacités (la puissance) des outils à garantir que les modèles satisfont certaines propriétés. Un *aperçu général* permet de voir si une vérification est possible et sous quelle forme. L'analyse structurelle examine la structure du modèle sans exécuter toutes les transitions (par exemple, matrices d'incidences, invariants). L'analyse d'état explore l'espace des états atteignables pour vérifier des propriétés dynamiques (absence de blocage, atteignabilité). Enfin, certains outils offrent la possibilité de vérifier directement des prédicats, en exprimant précisément des propriétés attendues sur le système.

<table><caption>TABLE 3 – Comparaison des outils (vérification de modèles)</caption><thead><tr><th rowspan="2"></th><th colspan="3">Vérification formelle</th></tr><tr><th>Analyse structurelle</th><th>Analyse d'état</th><th>Prédicats</th></tr></thead><tbody><tr><td>Tina</td><td>Oui, mais avec les contraintes temporelles oubliées</td><td>Oui, les RDP peuvent être convertis en automates directement dans Tina.</td><td>Oui, des prédicats peuvent être ajoutés dans l'outil de vérification "vérification de l'accessibilité".</td></tr><tr><td>Romeo</td><td>Oui, l'outil vérifie la structure de chaque RDP</td><td>Oui, l'outil vérifie les places, les transitions, les temps et les variables</td><td>Oui, des prédicats peuvent être ajoutés dans la page de vérification</td></tr><tr><td>CPN Tools</td><td>Oui, mais cela peut être long avec de petits RDP à cause des objets</td><td>Oui, l'outil réalise l'analyse d'état</td><td>Oui, des prédicats peuvent être ajoutés avant de faire le calcul d'état.</td></tr><tr><td>SPIN promela</td><td>Non, l'outil ne vérifie pas la structure de l'automate</td><td>Oui, il analyse tous les états possibles du système pour vérifier les erreurs</td><td>Oui, des prédicats peuvent être définis dans promela pour vérifier des conditions sur l'état ou les actions</td></tr><tr><td>UPPAAL</td><td>Oui, l'outil vérifie la structure de l'automate</td><td>Oui, l'outil vérifie tous les états, les transitions, les variables et si-gnaux</td><td>Oui, des prédicats peuvent être définis dans la page de vérification</td></tr></tbody></table>

La Table 3 compare les capacités de vérification des différents outils de modélisation. Trois aspects sont étudiés : (1) L'analyse structurelle : Tous les outils excepté SPIN/Promela offrent cette fonctionnalité, avec certaines limitations temporelles pour Tina mais une performance moins bonne pour CPN Tools sur les grands réseaux (cf. Figure 2). (2) L'analyse d'état : Tous les outils supportent cette fonctionnalité essentielle, avec SPIN se distinguant par sa capacité à analyser tous les états possibles du système (cf. Figure 3). (3) Les prédicats : La plupart des outils permettent de définir des prédicats dans leur interface de vérification, facilitant ainsi la spécification de propriétés à vérifier 20, 24, 28.
## 4.4 Simulation

La dernière catégorie se concentre sur les outils permettant de simuler le comportement dynamique du système modélisé, ce qui est utile pour détecter des erreurs avant toute phase de vérification exhaustive. La simulation est une exigence sur certains domaines où on veut tester ou comparer des versions de systèmes pour choisir le meilleur. L'analyse de performance (temps d'exécution, utilisation de ressources) est également envisagée pour évaluer l'efficacité du modèle. Enfin, la possibilité d'obtenir des traces d'exécution est un point clé pour comprendre et analyser les séquences d'événements.

<table><caption>TABLE 4 – Comparaison des outils (statique / dynamique)</caption><thead><tr><th rowspan="2"></th><th colspan="3">Vérification formelle</th></tr><tr><th>Simulation</th><th>Analyse de performance</th><th>Traces</th></tr></thead><tbody><tr><td>Tina</td><td>Oui, pas à pas ou automatique aléatoire. Le temps est bien géré</td><td>Non, il n'y a pas d'outils pour calculer la performance. Mais vous pouvez les développer</td><td>Oui, vous pouvez extraire l'historique de la simulation</td></tr><tr><td>Romeo</td><td>Oui, la simulation peut être effectuée mais seulement pas à pas</td><td>Non, il n'y a pas d'outils pour calculer la performance</td><td>Oui, vous pouvez extraire la simulation après qu'elle ait été effectuée</td></tr><tr><td>CPN Tools</td><td>Oui, pas à pas ou automatique aléatoire mais seulement par tranches de 50 itérations</td><td>Oui, il est possible d'obtenir les performances souhaitées</td><td>Oui, vous pouvez extraire l'historique de la simulation</td></tr><tr><td>SPIN promela</td><td>Oui, simulations interactives et aléatoires pour explorer les exécutions du modèle</td><td>Non, il est axé sur la correction, pas sur l'efficacité</td><td>Oui, il génère des traces d'exécution pour montrer la séquence des actions</td></tr><tr><td>UPPAAL</td><td>Oui, la simulation peut être effectuée pas à pas ou de manière aléatoire</td><td>Non, il n'y a pas d'outils pour calculer la performance</td><td>Oui, la trace peut être récupérée depuis la page de simulation concrète</td></tr></tbody></table>

La Table 4 compare les capacités de simulation et d'analyse dynamique des différents outils de modélisation. Cette comparaison montre que les outils varient dans leurs approches avec certains privilégiant l'exploration interactive comme SPIN et d'autres l'analyse quantitative comme CPN Tools, permettant ainsi de choisir l'outil le plus adapté selon le type d'analyse dynamique recherché. Trois aspects sont étudiés : (1) Simulation : Tous les outils offrent des capacités de simulation, mais avec des variations. Les outils RDP permettent généralement une exécution pas à pas ou automatique, tandis que SPIN/Promela se distingue par son approche interactive et aléatoire pour explorer les exécutions du modèle. (2) Analyse de performance : Seul CPN Tools parmi les outils étudiés propose des fonctionnalités natives d'analyse de performance, tandis que UPPAAL offre également une observation des performances dans son interface de simulation. (3) Traces : Tous les outils permettent d'extraire ou de visualiser l'historique des simulations, avec SPIN offrant particulièrement un bon support pour retracer la séquence des actions. Une trace produit une exécution, dont on va pouvoir déterminer les propriétés par exploration, notamment via des logiques temporelles [BBL+99].

## 5 Discussion

Rappelons que l'objectif initial est de proposer un cadre pour aider un analyste à trouver un outil pour modéliser, vérifier et simuler des SED.

La première interrogation est de savoir s'il n'existe pas déjà une méthodologie pour cela et/ou des benchmarks comparatifs d'outils. (i) Nous avons interrogé une IA générative avec le simple prompt "je cherche une classification des systèmes à événements discrets prenant en
compte modélisation, vérification et simulation". Le résultat est disponible dans la Section D.1 de l'annexe web¹. ChatGPT propose une classification des formalismes sur 4 types (RdP, FSM, Timed Automata, langages DEVS/UML), une sur les 3 activités, sur le niveau de formalisme, par domaine d'application et un tableau récapitulatif. C'est finalement un premier niveau qui correspond à la vision générale d'un étudiant de Master. (ii) Nous avons cherché des classification d'approches SED et de *model checkers* dans la littérature. Il existe de nombreux ouvrages sur DES (en anglais) et nombre s'intéressent à la simulation ou en opposition avec les systèmes continus. [CL08] couvre largement les formalismes mais pas les outils, D'autres couvrent une branche particulière, par exemple les SED stochastiques pour [Zim07] ou le contrôle via RdP et automates pour [SSVS13], là aussi sans outillage. L'outil de recherche du site de référence des RDP<sup>7</sup> ne fonctionne pas. Pour la vérification, [BBL<sup>+99</sup>] propose une vision pédagogique, mais l'outillage reste illustratif. (iii) Nous avons cherché des benchmarks. Nous n'en avons pas trouvé pour les outils SED. Pour les *model checkers*, il s'agit souvent de démontrer la performance sur une catégorie particulière de problèmes, par exemple [And18] en propose un pour le temps paramétré, ou des challenges comme le Waters INRIA<sup>8</sup> pour le temps-réel ou le Model Checking Contest<sup>9</sup>.

Dans cette étude menée en initiation à la recherche, le travail de comparaison et d'expérimentation autour des outils de modélisations et de vérifications formelles nous a permis de mieux comprendre leurs usages, leurs limites, et les avantages qu'ils peuvent offrir selon les besoins du système à modéliser. En explorant différentes approches, nous avons pu mieux comprendre dans quels mesure ces outils peuvent être appliqués à des systèmes réels comme ceux décrits dans nos cas d'étude. Nous discutons ici diverses observations de nos expériences.

Une première observation est que le choix de l'outil dépend fortement du contexte et des objectifs du projet. Par exemple, si l'on cherche à simuler le comportement général d'un système de production, certains outils offrent des interfaces graphiques simples et une simulation rapide. D'autres part, certains outils sont basées essentiellement dans le but de prouver rigoureusement les propriétés vérifiables des systèmes modélisés permettant aux outils plus techniques une vérification formelle complète. Dans notre cas, le domaine d'application cible est celui de la gestion de production. En résumé, il est important de déterminer son besoin pour choisir ses outils solutions. Les caractéristiques de nos tableaux peuvent contribuer à le déterminer.

Le cadre est-il une référence dans cet objectif. C'est un benchmark qui permet d'initier la démarche et de voir des exemples mais pas plus à ce stade. Le résultat présenté n'est pas exempt de critiques. Si on représente la démarche par un arbre de décision, on peut affirmer qu'il n'est complet ni en largeur (éventail des outils) ni en profondeur (détail des caractéristiques attendues, profondeur de nos analyses) mais nous avons les premiers nœuds. Si en plus on intègre la dimension du domaine d'application, trois cas d'étude n'est pas significatif. Une façon d'approfondir les travaux est chercher et tester de nouveaux outils en incluant les tests des outils non testé dans la Table 1. Il est aussi possible de tester sur de nouveaux cas d'études pouvant être plus complexe et volumineux afin de vérifié les limites de calcul des outils. Dans certains cas par exemple nous nous sommes heurté à la génération d'automate via les RDP du cas d'exemple A.3 car en fonctions du nombres de palettes et d'objets dans le système le nombre d'état devient rapidement trop élevé à calculer. En résumé, l'analyse doit être approfondie, élargie et mise en perspective avec plus de besoins.

La méthodologie de choix de solution consiste ici assez naïvement déterminer si les caractéristiques attendues pour un besoin sont présentes. La réponse est sans doute plus progressive

<footnote n="7">7. https://www2.informatik.uni-hamburg.de/TGI/PetriNets/tools/search.html</footnote>

<footnote n="8">8. https://waters2017.inria.fr/challenge/</footnote>

<footnote n="9">9. https://mcc.lip6.fr/2025/</footnote>
(on part de grandes catégories pour converger) et plus nuancée (n ne peut tout avoir, il faut
établir des compromis). Par exemple, plus le langage est expressif, plus on augmente le domaine
d'application mais plus il sera difficile de tout vérifier. Il faut faire des choix discriminants et
fixer des priorités sur les caractéristiques suivantes : (i) formalisme visuel, (ii) types de données,
(iii) algorithmique (calcul fonctionnel), (iv) modularité (réutilisation), (v) aide à la preuve,
(vi) gestion du temps et simulation, (vii) analyse des traces, (viii) etc. La prise en compte
du temps et des horloges est très variable d'une approche à l'autre. De même la conduite des
preuve est plus ou moins technique. Un arbre de décision met en évidence les critères de choix.
le benchmark devra couvrir un exemple de chaque type de besoin (les feuilles de l'arbre).

6 Conclusion

Le travail présenté ici part d'une question simple, quel outil devrais-je choisir pour analyser
la dynamique d'un système à événements discrets. La réponse n'est pas simple et dans cet article
nous avons proposé se suivre une approche méthodologique pour aider le non-spécialiste à s'y
retrouver. Nous proposons un premier niveau de grille d'évaluation pour comparer les outils sur
différentes caractéristiques selon le formalisme, la démarche et les techniques associées. Nous
avons testé différents outils sur différentes études de cas dans l'idée de produire un benchmark de
comparaison. On peut représenter l'espace d'exploration par une matrice en trois dimensions :
les caractéristiques à prendre en compte, les outils et les domaines d'utilisation. L'algorithme de
décision consiste alors à naviguer dans cet espace pour déterminer une ou plusieurs solutions.
La réponse à la question doit aussi être modulée selon l'expertise de celui qui se la pose.
Actuellement la grille s'adresse au débutant et les avis sont à confirmer par d'autres utilisateurs.

Les perspectives sont nombreuses : (i) Enrichir le référentiel sur les trois axes. La grille
devra être enrichie en détaillant chaque caractéristique actuelle par des caractéristiques plus
fines, car les outils sont souvent spécialisés et efficients sur de types spécifiques de problèmes
formels. L'ensemble des outils n'est ni représentatif (on n'a pas les meilleurs représentants de
chaque catégorie) ni exhaustifs (la liste des outils n'est pas explorée). La grille doit être élargie en
considérant de nouveaux outils. Enfin, les études de cas ne sont pas représentatives. Le référentiel
doit définir des domaines d'application et des cas d'étude par domaine. (ii) L'algorithme de
décision est informel. Le structurer serait un plus pour aider l'ingénieur à mener sa réflexion,
partant d'une spécification de son besoin, en lien avec l'analogie des cas du benchmark à leur
satisfaction en trouvant un ou plusieurs outils candidats. (iii) La performance d'un outil est
souvent liée à sa spécialisation. Trouver un outil permettra de répondre partiellement à son
besoin, moyennant quelques compromis. L'étape supérieure est de trouver la combinaison d'outil
permettant de mieux couvrir son besoin.
Un travail collectif serait pertinent pour mener à terme ces perspectives.

Les auteurs remercient l'Agence Nationale de la Recherche (ANR) pour son soutien financier dans le
cadre du projet RODIC, numéro de subvention ANR-21-CE10-0017.

Références

[AD94] Rajeev Alur and David L Dill. A theory of timed automata. Theoretical computer science, 126(2):183-235, 1994.

[And18] Étienne André. A benchmark library for parametric timed model checking. In Cyrille Artho and Peter Csaba Ölveczky, editors, Formal Techniques for Safety-Critical Systems
- 6th International Workshop, FTSCS 2018, Gold Coast, Australia, November 16, 2018, Revised Selected Papers, volume 1008 of Communications in Computer and Information Science, pages 75-83. Springer, 2018.

[Arn90] André Arnold. MEC : a system for constructing and analysing transition systems, page 117-132. Springer Berlin Heidelberg, 1990.

[BBL<sup>+</sup>99] Béatrice Bérard, Michel Bidoit, François Laroussinie, Antoine Petit, and Philippe Schnoebel. Vérification de logiciels : techniques et outils du model-checking. Vuibert Informática. Vuibert, 1999. ISBN 2-7117-8646-3.

[BDL04] Gerd Behrmann, Alexandre David, and Kim G Larsen. A tutorial on uppaal. Formal methods for the design of real-time systems, pages 200-236, 2004.

[BLL<sup>+</sup>96] Johan Bengtsson, Kim Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. UPPAAL—a tool suite for automatic verification of real-time systems. Springer, 1996.

[BRV04] Bernard Berthomieu*, P-O Ribet, and François Vernadat. The tool tina-construction of abstract state spaces for petri nets and time petri nets. International journal of production research, 42(14):2741-2756, 2004.

[BV06] Bernard Berthomieu and François Vernadat. Time petri nets analysis with tina. In QEST, volume 6, pages 123-124, 2006.

[CCF<sup>+</sup>99] R Scott Cost, Ye Chen, Tim Finin, Yannis K Labrou, Yun Peng, et al. Modeling agent conversations with colored petri nets. In Working notes of the Autonomous Agents' 99 Workshop on Specifying and Implementing Conversation Policies, 1999.

[CL08] Christos G Cassandras and Stéphane Lafortune. Introduction to discrete event systems. Springer, 2008.

[CRS18] Rance Cleaveland, A. W. Roscoe, and Scott A. Smolka. Process Algebra and Model Checking, page 1149-1195. Springer International Publishing, 2018.

[Geh19] Vijay Gehlot. From petri nets to colored petri nets : A tutorial introduction to nets based formalism for modeling and simulation. In 2019 Winter Simulation Conference (WSC), pages 1519-1533, 2019.

[GLMR05] Guillaume Gardey, Didier Lime, Morgan Magnin, and Olivier (H ) Roux. Romeo : A tool for analyzing time petri nets. In Computer Aided Verification : 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005. Proceedings 17, pages 418-423. Springer, 2005.

[GLMS11] Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe. Cadp 2010 : A toolbox for the construction and analysis of distributed processes. In Int. conf. on tools and algorithms for the construction and analysis of systems, pages 372-387. Springer, 2011.

[GMBS96] Marie-Claude Gaudel, Bruno Marre, Gilles Bernot, and Françoise Schlienger. Précis de génie logiciel. Elsevier Masson, Barcelona, Spain, 1996.

[GV03] C. Girault and R. Valk. Petri Nets for Systems Engineering : A Guide to Modeling, Verification, and Applications. Springer, 2003.

[Hol04] Gerard J Holzmann. The SPIN model checker : Primer and reference manual, volume 1003. Addison-Wesley Reading, 2004.

[Nor03] Nordgren. Flexsim simulation environment. In Proceedings of the 2003 Winter Simulation Conference, 2003., volume 1, pages 197-200. IEEE, 2003.

[RWL<sup>+</sup>03] Anne Vinter Ratzer, Lisa Wells, Henry Michael Lassen, Mads Laursen, Jacob Frank Qvortrup, Martin Stig Stissing, Michael Westergaard, Søren Christensen, and Kurt Jensen. Cpn tools for editing, simulating, and analysing coloured petri nets. In International conference on application and theory of petri nets, pages 450-462. Springer, 2003.

[SSVS13] Carla Seatzu, Manuel Silva, and Jan H Van Schuppen. Control of discrete-event systems, volume 433. Springer, 2013.

[Zim07] Armin Zimmermann. Stochastic discrete event systems. Springer, 2007.
# A Études de cas support

Les outils ont été testés sur trois cas d'études. Le choix des cas d'étude est arbitraire et non représentatif. Nous aurions pu prendre des cas classiques de contrôle distribué comme le 'producteur/consommateur', rendez-vous, 'lecteurs/écrivain'. Nous avons souhaité des cas concrets, et les feux tricolores ou le cas Kanban sont simples et compréhensibles par tous. Nous disposons d'une base de modèles (automates synchronisé, RDP, UML...) pour nos enseignements qui ont permis de nous focaliser sur les outils et non les modèles. Ces deux cas sont des cas simplifié d'automate qui possèdes très peu de places/états ainsi que des arcs/transitions. Concernant le cas n°3, c'est un cas pour lequel nous disposons d'un modèle FlexSim réalisé par un collègue spécialiste, qui nous permet de comparer avec les autres approches. La base pourra s'enrichir des cas classiques de contrôle distribué comme le 'producteur/consommateur', rendez-vous, 'lecteurs/écrivain'. Nous n'avons pas considéré ici la vérification de logiciels ou d'architecture matérielles, domaines d'application d'une partie des outils de vérification formelle mentionnées dans la section suivante.

## A.1 Première étude de cas : Feux tricolores

Le premier cas d'étude que nous avons réalisé se base sur un très simple carrefour automobile composer de 4 feux rouges (Nord, Sud, Est, Ouest) le principe de ce cas est que les feux doivent alterné en fonction de si il sont vertical ou horizontal entre le feu rouge et le feu vert pour se faire chaque feu possède trois états vert, orange et rouge les feux vert passe au orange pour laisser le temps aux usagers de s'arrêter est éviter un accident quand les feux passe de orange a rouge les feux précédemment rouge passe au vert. Diverses extensions existent : mode dégradé avec feux clignotants, carrefour avec feux de changement direction à gauche (8 feux). Ce cas est traité en UML dans [AV13] Pascal André and Alain Vailly. Développement de logiciel avec UML2 et OCL ; cours et exercices corrigés, volume 6 of Collection Technosup. Editions Ellipses, 2013. ISBN 9782729883539.

## A.2 Deuxième étude de cas : un atelier de fabrication Kanban

Le second cas d'étude est nommé Kanban. Il repose sur des étapes à réaliser pour obtenir des pièces ou objets ayant été traités par trois outils, appelés ici "postes". Entre chaque poste, il y a un conteneur permettant l'accumulation des pièces ou objets. On pourrait représenter cela comme un travailleur qui commence par récupérer les pièces ou objets dans le stockage initial, puis les perce avec une perceuse. Ensuite, il les dépose et revient plus tard pour les usiner avec une fraise. Après une pause, il les fixe sur un tour à métaux pour tailler les pièces ou objets, achevant ainsi leur processus de traitement. Ce cas est traité avec les automates synchronisés dans [AV02] Pascal André and Alain Vailly. Exercices corrigés de conception logicielle ; Modélisation des Systèmes d'Information volume 3 of Collection Technosup. Editions Ellipses, 2002. ISBN 2-7298-1289-X.

## A.3 Troisième étude de cas : chaîne de production

Le troisième cas d'étude est plus complexe que les deux précédents. Il reste cependant assez simple comparé à de véritables systèmes de production industrielle. Il est représenté sur la figure 6 et consiste en une boucle de plusieurs convoyeurs qui bloquent des palettes à chaque poste. Une source de palettes est placée avant le poste 1, permettant d'ajouter le nombre de palettes choisi dans le système. Les palettes se déplacent le long des convoyeurs, s'arrêtant aux
bloqueurs de chaque poste. Les palettes commencent leur parcours sans objets, puis, au poste 1, elles s'arrêtent pour qu'un bras robotique y dépose deux objets (représentés sous forme de fiole sur la figure 6). Les objets arrivent dans le système par une source au poste 1, qui dépose un objet sur un stockage à intervalles réguliers. Le robot prend ensuite les objets un par un et les dépose sur les palettes qui se présentent devant lui. Une fois que la palette bloquée obtient deux objets, elle peut continuer son chemin vers le poste 2.

Au poste 2, un opérateur humain prélève un des objets sur la palette pour l'apporter au processus du poste 2. Une fois la palette libérée d'un objet, elle continue son chemin jusqu'au poste 3. L'opérateur du poste 2, une fois son processus terminé, reprend l'objet traité et le dépose sur sa palette bloquée au poste 3. Le poste 3 fonctionne de manière similaire au poste 2. Une fois les deux postes terminés, la palette continue son chemin vers le poste 4, où un transporteur dépose un par un les objets traités vers le dépôt de sortie. Les palettes continuent ce cycle indéfiniment tant que le système est alimenté en objets.

<figure><img src="image_7.png" /><figcaption>FIGURE 6 – Etude de cas réalisé dans l'outil de modélisation FlexSim</figcaption></figure>

# B Approche, formalisme, outils

Les chaînes de production industrielles sont principalement des systèmes composés de machines dans lesquels des objets sont traités au fur et à mesure qu'ils évoluent dans la chaîne. Il existe de nombreuses méthodes pour simuler ces comportements à l'aide d'outils numériques, comme les formalismes simples des réseaux de Petri (RDP) et des automates, chacun simulant l'état des systèmes décrits précédemment de manière différente. D'autres formalismes plus complexes permettent la création de systèmes de simulation plus avancés, mais notre objectif est que les outils trouvés ou développés soient utilisables par le plus grand nombre de personnes. Cela signifie que ces outils doivent être facilement et rapidement utilisables par des personnes ayant peu de connaissances en modélisation de systèmes. Nous nous sommes donc basés et concentrés sur les deux formalismes simples cités plus tôt, à savoir les RDP et les automates. Ces formalismes étant largement implémentés depuis de nombreuses années, de nombreux outils permettent de les utiliser. Chaque outil implémente une version différente de
ces formalismes. Il est donc important de décrire et d'analyser chaque version dans la suite de cet article. Concernant les outils, on trouve des listes telles que celle de wikipedia <fnref n="10" /> mais aussi dans les ouvrages [BBL+99] ou des surveys.

## B.1 Les Réseaux de Pétri (RDP)

Les réseaux de Petri (RDP) [GV03] sont un formalisme facile à visualiser et à représenter pour modéliser des flux dans un système. Les RDP sont constitués de quatre éléments principaux : les places, les jetons, les transitions et les arcs. Les places sont représentées par des cercles et peuvent contenir zéro ou plusieurs jetons, sous forme de points. Ces jetons permettent d'activer les transitions reliées à la place où ils se trouvent. Les transitions sont représentées par une petite barre (ligne) d'où partent et arrivent des flèches, qui sont les arcs. Une transition prend des jetons dans les places d'entrée qui lui sont reliées et place des jetons dans les places de sortie qui lui sont associées. Pour qu'une transition soit activée, toutes ses places d'entrée doivent contenir les jetons requis. Lorsqu'une transition est activée, elle consomme les jetons des places d'entrée en les faisant disparaître, puis crée des jetons dans toutes les places de sortie. À chaque activation d'une transition, le système est modifié, ce qui permet de créer un flux de jeton permettant de représenter un système, comme le cycle des feux de signalisation à un carrefour.

**RDP temporisés** Les RDP temporisés se caractérise par l'ajout d'une horloge de temps global qui va permettre d'ajouter des minuteurs dans notre système. Par exemple sur un feu rouge, le temps qu'il prend avant de repasser au orange peut être définie comme un compteur qui se décrémente au fur et à mesure que le temps avance. Les RDP temporisé utilisent différentes manière pour gérer ce genre de problème. La première version Une manière courante est d'ajouter un compteur sur les transitions. Ce compteur fait en sorte que lorsqu'une transition obtient tous les jetons dans ces places d'entrées elle ne peut quand même pas être tirée, car avant de pouvoir l'être, il faut que le compteur de temps global ait augmenté du temps de la transition. Une deuxième version utilisant le temps sur les transitions consiste à pouvoir les tirer quand elles sont activables mais attendre le temps de la transition avant de mettre les jetons dans ses places de sorties. Une troisième version permet d'ajouter du temps à chaque jetons présent dans le système, chaque jeton peut être utilisé seulement si le temps global est plus élevé que le temps du jeton. Il est important de précisé que à un temps global donnée le système doit tirer toutes les transitions qui peuvent l'être. Il existe d'autre façon de gérer le temps dans des RDP mais elles ne seront pas développées dans ce papier. Le temps est une donnée très importante surtout dans la modélisation de modèle industriel c'est une des données nécessaire pour calculer la productivité du système testé.

**RDP colorés** Les RDP utilisant des couleurs améliorent les jetons en leur ajoutant une distinction. La couleur associée un jeton lui donne une catégorie qui permet ensuite d'avoir des transitions ne prennent qu'un type de couleur. Cette version des RDP permet de trier les jetons en les séparant grâce à des transitions dédiées à certaine couleur. Par exemple une place ayant un jeton bleu et un jeton rouge peut avoir une transition qui ne prend que les jetons bleu pour faire une action dans le système et inversement avec une transition rouge. Les couleurs permettent ainsi de différencier les jetons pour réaliser des actions différentes en concurrence

**RDP avec des objets** Les RDP avec des objets sont une amélioration des RDP colorés qui permet encore plus de possibilité de différencier chaque jetons du système [CCF+99]. Un objet est une définition comme la classe int ou string qui est définie pour être utilisé dans le système. Il

<footnote n="10">10. https://en.wikipedia.org/wiki/List_of_model_checking_tools</footnote>
est possible de créer autant de types d'objet que souhaité et de les utilisées comme des couleurs
pour distingué jetons. Mais, si la coloration n'ajoute que la distinction des jetons, les objets
peuvent se fusionner entre eux pour former des jetons composer de plusieurs objets. C'est une
caractéristique très utile dans un système de modélisation car elle représente la façon qu'ont les
objets du systèmes à interagir. Comme exemple, on définit un objet fiole et un objet palette,
le système modélisé dépose des fioles sur ces palettes afin de déplacer les fioles. Les palettes se
déplacent sur des convoyeurs entres plusieurs machines de traitement, parfois sans fiole dessus,
parfois avec plusieurs fioles. L'assemblage des deux objets dans la modélisation permet de
simuler à l'identique du réel les comportements des objets. Ces assemblages et désassemblage
d'objets permettent de nouveau comportement dans le RDP.

## B.2 Les Automates

Les automates sont un modèle mathématique utilisé pour représenter des systèmes dynamiques et discrets. Un automate est généralement composé de deux éléments principaux : les états et les transitions (arcs). Les états sont représentés par des cercles, ils décrivent les différentes situations dans lesquelles le système peut se trouver comme un interrupteur avec deux état ouvert ou fermer. Un état peut être initial, final ou simplement une place de transitions entre ces deux états. Les transitions sont représentées par des flèches, les transitions indiquent les passages possibles d'un état à un autre.

**Automates temporisé** Les automates temporisés ont été proposé par Alur et Dill en 1990 [AD94] pour y ajouter des informations supplémentaires sur l'écoulement du temps de chaque automate. Cela permet de connaître le temps d'exécution d'un automate et d'éviter qu'il reste trop longtemps inactif ou ne s'active qu'à un certain moment, sans pour autant modifier la structure du modèle. Les automates temporisés sont composés de deux éléments principaux : l'automate principal, avec un état initial, ses états, ses arcs de transition, et en second lieu, l'ajout d'une horloge permettant d'imposer des contraintes sur les arcs. Le temps permet de connaître le temps nécessaire pour qu'un objet soit traité, mais aussi de coordonner chaque sous-automate pour qu'ils avancent au même rythme. Par exemple, cela permet de coordonner chaque convoyeur pour faire avancer les objets en même temps, ou de réaliser plusieurs actions sur deux objets différents disposés sur deux postes de construction. Par exemple, pendant que le robot met un certain temps à récupérer les objets du stock pour les déposer sur la palette, un autre objet peut être traité par les machines gérées par les opérateurs et déposé dans le stockage final.

## B.3 Algèbres de Processus

Les algèbres de processus décrivent le comportement d'un système (le process) sous forme
de calculs définis par une algèbre. Ce comportement est fait d'événements et actions enchaînées
par le système dans un ordre défini. Il existe de nombreuses algèbres de processus Les principaux algèbres de processus utilisés sont : CSP (Communicating sequential processes) de Hoare
CCS (Calculus of Communicating Systems) de Milner, Pi-calcul, aussi de Milner, mais arrivé
plus tard. LOTOS (Language Of Temporal Ordering Specification) ajoute les types d'abstraits
de données à CSP pour couvrir un spectre plus large. C'est une norme ISO 8807 utilisée pour
la spécification des protocoles dans les standards ISO OSI. Il a depuis donné lieu au langage
BIP (Behavior, Interaction, Priority) qui intègre les composants logiciels. Dans les outils mentionnons notamment CADP [GLMS11] (Construction and Analysis of Distributed Processes) <fnref n="11" />

<footnote n="11">11. https://cadp.inria.fr/</footnote>
développé à Grenoble et CADP et FDR tool<fnref n="12" />.

Dans cette catégorie, nous avons choisi l'outil SPIN, largement répandu. L'outil *model che-cker* Spin <fnref n="13" /> repose sur un langage de modélisation nommé Promela inspiré du langage et de la syntaxe C, ce qui le rend relativement lisible et structuré. Contrairement au langage C, Promela ne sert pas à écrire des programmes à exécuter sur une machine, mais à décrire le comporte-ment abstrait d'un système sous forme de processus qui peuvent s'exécuter en parallèle. Chaque processus peut être vu comme un automate avec des états internes, des transitions et des règles d'exécution. L'utilisation se fait en plusieurs étapes :

- Écriture du modèle en Promela : il s'agit d'abord de décrire les différents processus (*proctype*), les canaux de communication (*chan*), les variables locales et globales, ainsi que la logique de chaque composant du système. Chaque processus représente un comportement que l'on souhaite modéliser.

- Initialisation : une fois les processus définis, le bloc *init* permet de spécifier leur instanciation (avec l'instruction *run*) et ainsi de mettre en marche le système modélisé.

- Simulation : Spin offre la possibilité de simuler l'exécution du modèle, soit manuellement en choisissant les transitions à franchir, soit de manière automatique ou aléatoire. Cette étape est essentielle pour observer le comportement du système et détecter d'éventuelles anomalies dès la phase de modélisation.

- Vérification formelle : Spin permet d'appliquer une vérification des propriétés du système, notamment exprimées en logique temporelle linéaire (LTL). On peut ainsi prouver, par exemple, l'absence de blocage (deadlock), la garantie d'atteindre un état souhaité, ou le respect de contraintes de sûreté et de vivacité.

<figure><img src="image_8.png" /><figcaption>FIGURE 7 – Le processus de Spin pour la modélisation d'un système</figcaption></figure>

<footnote n="12">12. https://cocotec.io/fdr/</footnote>

<footnote n="13">13. https://spinroot.com/</footnote>
## B.4 Simulation

FlexSim est un outil spécialisé dans la création de chaînes de production. Il permet de modéliser dans une fenêtre de visualisation 3D (voir figure 6) des systèmes de flux. L'outil rend possible la création d'un modèle grâce à des modules par défaut qu'il est possible de déplacer dans l'espace de visualisation. Chaque composants peut être assemblés avec d'autres grâce à des connections, soit automatiques intégré dans FlexSim, soit en définissant le comportement via du code. Les composants peuvent être lourdement paramétrés pour changer leur comportement et reflété au maximum la réalité afin d'être au plus proche de la configuration réel. FlexSim implémente des mécanismes comme la gestion du temps ou des évènements aléatoires étant essentiels dans des simulations de chaîne de production. Pour réaliser des actions non prises en charge par défaut dans l'outil, il est possible de les développer en langage de programmation FlexScript qui est une dérive propriétaire de FlexSim se basant sur le langage C#. Une fois la modélisation d'un système créé, il est possible de lancer sa simulation pour tester le système afin de vérifié s'il se comporte correctement. La simulation permet de générer des statistiques lors de son déroulement ce qui permet de comparer les modèles simuler. FlexSim donne la possibilité de créer ses propres bibliothèques pour les réutiliser dans d'autres projets ce qui entraîne une facilité pour créer de nouveau modèle sans partir de zéro.

## B.5 Analyse des Propriétés

Les RDP et les automates sont deux formalismes qui se vérifie grâce à différentes analyses. Il y a deux grand types d'analyses qui sont respectivement statique et dynamique. Les analyses statiques sont faites directement sur les modèles réalisés en testant le bon déroulé du système. C'est à dire par exemple de produire la simulation du système en déplaçant soit les jetons soit en changeant d'état dans un automate. Une simulation peut se terminer de plusieurs façons en fonction de comment sont formés les systèmes formels testé. Une simulation peut se retrouver bloquée d'une façon inapproprié ce qui signifie qu'il y a une erreur dans la modélisation. Autrement, si le système est correctement définie alors la simulation peut se retrouver dans un état final s'il se termine, mais elle peut aussi ne jamais se terminer si le système est une boucle infinie. La simulation permet une fois qu'elle est finis d'obtenir les traces de l'exécution mais aussi des analyses de performances qui permettent de déterminer si un modèle est meilleur qu'un autres. Le deuxième types d'analyses, les analyses dynamiques quand elles sont réalisées doivent pouvoir satisfaire certaines propriétés, la première étant l'atteignabilité de chaque place'état de l'automate ou du RDP. Signifiant que chaque place du système doit pouvoir être atteints par des jetons ou être activés. Les RDP permettent également d'être transformé en un automate afin de vérifié de nouvelles propriétés sur cet automate grâce à une analyse des états. L'automate ou le RDP doit pouvoir vérifier l'absence de place morte (dead marking) et de transitions morte (dead transitions), c'est-à-dire s'assurer qu'il n'y a pas de situations où le système se bloque et où certaines transitions ou places deviennent inutilisables. Enfin, les propriétés doivent être testées sur la simulation et sur sa vivacité (liveness properties) pour voir si deux états peuvent être atteints parallèlement ou s'ils sont capables de s'activer successivement [BBL+99].

Le Model Checking est une technique de vérification formelle qui permet de s'assurer que les modèles respectent certaines propriétés spécifiées. Cette technique est particulièrement utile pour les systèmes critiques où les erreurs peuvent avoir des conséquences graves. Le Model Checking consiste à explorer systématiquement toutes les configurations possibles du système pour vérifier si les propriétés souhaitées sont satisfaites. Une méthode efficace utilisée par les outils de vérification formelle consiste à spécifier les propriétés du système à l'aide de formalismes
logiques adaptés. Par exemple, considérons une propriété globale exprimée sur le système de
convoyeurs composé de quatre postes de travail (décrit dans la partie 2.1) (figure 6). On souhaite
vérifier qu'une palette ne peut jamais quitter le poste 1 sans avoir exactement deux produits
dessus. Cette contrainte peut être formulée de la manière suivante :

$$
\forall ((\text{etat\_poste1} = \text{EXPEDITION}) \rightarrow (\text{contenu\_palette\_poste1} = \text{PALETTE\_2PRODUITS}))
$$

Cette formule se décompose comme suit :

— L'opérateur $\forall$ (toujours) indique que la propriété doit être vraie à tout moment de l'exécution du système.

— L'implication $\rightarrow$ établit une relation conditionnelle entre deux états.

— La partie gauche etat\_poste1 = EXPEDITION correspond à la condition : lorsque le poste 1 est en état d'expédition (prêt à envoyer la palette).

— La partie droite contenu\_palette\_poste1 = PALETTE\_2PRODUITS correspond à la consé-
quence : la palette doit contenir exactement deux produits.

En langage naturel, cette propriété signifie : « À tout instant, si le poste 1 expédie une palette, alors cette palette contient nécessairement deux produits. »

Cette vérification est essentielle pour garantir la cohérence du fonctionnement du système. Elle devra être formulée et validée dans les différents outils de modélisation et de vérification étudiés, chacun utilisant ses propres mécanismes pour exprimer et prouver ce type de contrainte.

B.6 Outils sélectionnés

Nous avons testé au moins un outil dans chaque sous-catégorie RdP (Romeo<sup>14</sup> [GLMR05], Tina<sup>15</sup> [BRV04], CPN Tools<sup>16</sup> [RWL<sup>+</sup>03]), Automate (UPPAAL<sup>17</sup> [BLL<sup>+</sup>96]), Algèbres de processus (SPIN<sup>18</sup> [Ho04]). Nous avons aussi fait des tests avec Renew<sup>19</sup>, Imitator<sup>20</sup>, Itemis<sup>21</sup> (statcharts) et JFLAP<sup>22</sup>.

Nos critères de sélection ont été un choix crucial dans nos expérimentation afin que toutes les variantes des formalismes décrit en amont soit couvert par la sélection. Il faut commencer par des outils très simple comme Tina et Romeo pour prendre en main les formalismes brut. Puis ensuite, explorer des outils implémentant les ajouts possibles à ces formalismes pour connaitre les nécessités afin de réaliser une bonne simulation de système de production industrielle. Celui-ci devant permettre de réaliser des tests de performance sur la production de la chaîne de production tout en gardant une certaine modularité dans la modélisation du système. On souhaite pouvoir décomposer notre système en plusieurs sous systèmes pouvant communiquer entre eux, permettant ainsi au utilisateurs de créer un assemblage de modules plutôt que créer le système dans son intégralité. La vérification des propriétés se ferait alors dans chaque module et serait plus simple pour déterminer où se trouve les erreurs. Pour résumer, il faut dans les caractéristiques un outils capable d'avoir une capacité de compréhension et de création simple mais également capable de pouvoir vérifié les propriétés liés à ces systèmes.

B.6.1 Tina v3.4.4

<footnote n="14">14. https://romeo.ls2n.fr/</footnote>

<footnote n="15">15. https://projects.laas.fr/tina/</footnote>

<footnote n="16">16. https://cpntools.org/</footnote>

<footnote n="17">17. https://uppaal.org/</footnote>

<footnote n="18">18. https://spinroot.com/</footnote>

<footnote n="19">19. http://www.renew.de/</footnote>

<footnote n="20">20. https://www.imitator.fr/</footnote>

<footnote n="21">21. https://www.itemis.com/en/yakindu-statechart-tools</footnote>

<footnote n="22">22. https://www.jflap.org/</footnote>
L'outil Tina est reconnu pour être un "Analyseur de RDP temporisés" [BV06] et permet de créer, simuler et analyser des RDP et RDP temporisés avec une interface simple à prendre en main. Il existe deux manières de concevoir un RDP dans Tina : il est possible de le créer visuellement grâce à l'utilisation de cercles pour les places, de rectangles pour les transitions et de flèches pour les arcs. Une fois la forme du système recréée visuellement, les places peuvent être remplies de jetons et il y a le moyen d'ajouter des intervalles de temps sur les transitions. Une fois un RDP produit, il est possible de simuler son exécution et de vérifier ses propriétés. Les systèmes de vérifications par défauts dans Tina sont : (i) l'analyse d'état : Permet de créer l'automate d'état associé au RDP pour vérifier de nouvelles propriétés. (ii) l'analyse structurale : Réalise l'analyse des propriétés structurelles du RDP en vérifiant la gestion des flux de jetons sur les places et transitions. (iii) vérification de l'accessibilité : vérifie qu'il n'y a pas de places inutilles dans le système. Cette analyse vérifie aussi les état et transition inutilisés. (iv) vérification du RDP : vérifie que le RDP modélisé est correcte dans sa conception.

<figure><img src="image_9.png" /><figcaption>FIGURE 8 – Graph de marquage avec Tina</figcaption></figure>

Tina comporte un outil de simulation sur les RDP et RDP temporisés plus pratique que ses concurrents présenté plus bas dans cet article. Le temps étant la seule extension de RDP supportés, l'outil Tina se concentre sur sa gestion et gère seule la gestion du compteur de temps en milliseconde lors de la simulation. L'outil permet de simuler le RDP à tester de deux manières différentes, soit pas à pas en cliquant sur les transitions activables en gérant soit même l'avancement du temps. Soit en cliquant sur un bouton random qui active étape par étape aléatoirement chaque transitions. L'aléatoire active toutes les transitions possible à un temps données avant d'avancer le compteur de temps. Si deux transitions sont activables depuis une même place alors le RDP n'est pas déterministe et le tirage ce réalise aléatoirement. L'outil de calcul d'atteignabilité avec Tina (cf. Figure 8) propose nombre d'options pour explorer l'espace d'état. En particulier, la construction d'un graphe d'état est intéressante pour la vérification de propriétés.

## B.6.2 Romeo v3.10.5

L'outil Romeo permet de créer et simuler des RDP avec une interface simplifier et facile a prendre en main sur des RDP simple. [GLMR05] Pour ce faire le logiciel propose un quadrillage pour permettre d'aligner les places représenter sous la forme d'un cercle et les transitions représenter sous la forme de rectangle facilement. L'outil permet l'ajout d'un intervalle de temps sur les transitions se qui permet de joué le rôle d'un bloqueur pour empêcher les transitions d'être franchi successivement. Pour la partie une peu plus complexe Romeo permet également l'utilisation de message permettant la séparation des RDP et permet une meilleurs lisibilité global. Enfin il permet l'utilisation de variables ainsi que l'ajout de bloqueur lié au variable. Une fois le RDP crée il est possible grâce a l'onglet simulation de le testé en appuyant sur les transitions ou en crée une séquence composé des nom des transitions a prendre et obtenir de vérifier ses propriété avec l'onglet checker. Romeo comporte un outils de creation de RDP plus approfondi que l'outils Tina et CPN Tools pour avoir plusieurs RDP en même temps avec la possibilité d'ajouter des variables et bloqueurs permettant de simuler des envoie de message. Pour la partie simulation Romeo est moins performant car il ne permet pas de faire passer des transitions aléatoirement est oblige l'utilisateur a connaitre les transitions qu'il souhaite passer et qui pourront
passer a l'avance ou de passer les transitions manuellement.

### B.6.3 CPN Tools v4.0.1

"Colored Petri Nets" de son diminutif CPN Tools est un outil permettant de créer des RDP temporisés [Geh19] tout en y ajoutant le formalisme des RDP avec des objets. Les RDP générés peuvent être analysé en vérifiant des propriétés grâce à plusieurs outils de vérification comme l'analyse d'état qui génère l'automate d'état associé au RDP. La façon de créer un RDP sans objets dans CPN Tools ne diffère pas des autres outils. Les places et les transitions sont aussi représenter par des cercles et des rectangles. Le temps lui fonctionne sur les jetons, c'est à dire que chaque jeton du système a un temps associé à lui même. L'outils gère une varirables de temps global ce qui empêche les jetons ayant leur temps plus élevé que le temps global d'être utilisés dans le système. Donc si il existe place1 -> transition1 -> place2 avec un jeton@10 (un jeton de temps 10) dans p1 alors si le temps global est 5 la transition t1 ne peut être activé. Il faut que le temps global soit incrémenter jusqu'à minimum 10 pour pouvoir activer t1. Le temps de chaque jeton peut être incrémenter lors du passage par un arc ou une transition. reprenons l'exemple juste avant mais en ajoutant @5 comme valeur de temps à ajouter, alors lors de l'activation de t1 le jeton se trouvant dans p2 sera jeton@15. Le temps du jeton en sortie de la transition est l'addition du temps maximum des places d'entrée + temps de la transition + temps de l'arc de sortie. CPN Tools autorise dans la conception de ces RDP de définir une infinité d'objets définie avec le mot clé "colset" qui peuvent ensuite être associés aux jetons du système. Il est aussi possible de créer des assemblages d'objets pour déplacer un groupe d'objets dans le RDP. Cet possibilité permet de créer des transitions qui ne prennent qu'un seul type d'objets, ce comportement permet de nouvelles manière de modéliser.

### B.6.4 UPPAAL 4.1.26

L'outil UPPAAL permet de créer et de simuler des automates avec une interface simplifiée, facile à utiliser pour des automates simples. Pour ce faire, le logiciel permet de créer un automate avec des cercles correspondant aux états et des flèches correspondant aux arcs ou transitions [BDL04]. Pour des automates un peu plus complexes, UPPAAL permet de créer des automates communicants avec l'envoi de messages (avec des points d'exclamation pour l'envoi ou des points d'interrogation pour la réception), ainsi que la création de variables globales et locales, permettant de créer des bloqueurs ou des compteurs.

Une fois l'automate créé, il est possible, grâce à l'onglet simulation, de tester l'automate manuellement en choisissant les transitions à prendre, ou de manière aléatoire dans le même onglet de simulation concrète. Enfin, on peut vérifier les propriétés de l'automate dans l'onglet vérification.

UPPAAL est un outil pratique à utiliser pour les automates grâce à sa partie graphique qui facilite la création et la simulation rapide d'un automate, contrairement à Spin qui est exclusivement textuel. UPPAAL peut également simuler l'automate de trois manières différentes : avec une partie graphique (encadrée en rouge sur la figure 9) où chaque automate change d'état avec un déplacement marqué en rouge, il peut également se lire sur un diagramme de séquence (encadrée en vert) ou encore sous forme textuelle pour les transitions prises (encadrée en bleu).

### B.6.5 Spin v. 6.5.0

L'outil Spin "Simple Promela Interpreter" [Hol04] est un vérificateur de modèle dédié à la vérification formelle de système concurrents notamment pour les protocoles de communication ou les systèmes logiciels complexes et est exprimé avec le langage Promela. Spin ne propose pas d'interface graphique comme les outils cités avant et cela peut rendre l'outil moins accessible pour une prise en main rapide, mais repose sur une description textuelle du système qui nécessite une certaine rigueur pour modéliser correctement les processus. Promela permet de modéliser aussi bien des processus synchrones, qui nécessitent une réponse pour poursuivre leur exécution, que des processus asynchrones, capables d'évoluer
<figure><img src="image_10.png" /><figcaption>FIGURE 9 – Simulation d'envoi de message entre deux utilisateurs</figcaption></figure>

de manière indépendante. Comme UPPAAL, Spin prend en charge à la fois des canaux de communication entre processus et l'utilisation de variables, tandis que Romeo se concentre principalement sur la manipulation de variables pour contrôler les conditions de franchissement des transitions. Spin permet également de définir des contraintes temporelles et logiques, tout en offrant une simulation du modèle avant la vérification formelle.

# C Application aux études de cas

Nous avons expérimenté l'étude de cas avec différents outils de modélisation et de vérification dédiés à la vérification formelle de la dynamique des systèmes. Entre autres, nous avons expérimenté avec des outils de réseaux de Petri (Tina, Romeo, CPN tools), des automates communicants (UPPAAL), ou des processus (SPIN). Dans ce qui suit, nous illustrons nos expériences avec trois d'entre eux.

## C.1 Cas d'étude A.1 avec un RDP sur Tina

La Figure 10 représente deux modèles pour le cas 1 avec Tina.
<figure><img src="image_11.png" /><figcaption>FIGURE 10 - Cas d'étude Feux tricolores modélisé sur Tina</figcaption></figure>

## C.2 Cas d'étude A.2 avec un RDP sur Tina

La Figure 11 représente un modèle simpliste pour le cas 2 avec Tina.

<figure><img src="image_12.png" /><figcaption>FIGURE 11 - Cas d'étude Kanban modélisé sur Tina (version simpliste)</figcaption></figure>

La Figure 12 représente le modèle pour le cas 2 avec Tina.

<figure><img src="image_13.png" /><figcaption>FIGURE 12 - Cas d'étude Kanban modélisé sur Tina</figcaption></figure>
## C.3 Cas d'étude A.3 avec un RDP sur Tina

Voir le texte de l'article. Nous ne donnons ici que l'édition du modèle avec Tina dans la Figure 13.

<figure><img src="image_14.png" /><figcaption>FIGURE 13 – Cas d'étude simplifié traité avec Tina</figcaption></figure>

<figure><img src="image_15.png" /><figcaption>FIGURE 14 – Espace d'états du Cas d'étude simplifié V3 traité avec Tina</figcaption></figure>
## C.4 Cas d'étude A.1 avec un RDP sur CPN Tools

La Figure 15 représente deux modèles pour le cas 1 avec CPN Tools.

<figure><img src="image_16.png" /><figcaption>FIGURE 15 - Cas d'étude Feux tricolores modélisé sur CPN Tools</figcaption></figure>

## C.5 Cas d'étude A.2 avec un RDP sur CPN Tools

La Figure 16 représente le modèle pour le cas 2 avec CPN Tools.

à insérer

<caption>FIGURE 16 - Cas d'étude Kanban modélisé sur CPN Tools</caption>

## C.6 Cas d'étude A.3 avec un RDP sur CPN Tools

On retrouve dans ce cas d'étude la même structure que dans le cas d'étude sur Tina mais l'ajout du formalismes des objets permet d'ajouter les types d'objets que l'on définie au jetons du système. Cela enlève le besoin d'ajouter des bloqueurs dans le système car il est possible de sélectionner le type de jetons pris par une transition. Donc lorsque un jeton arrive à une place proche d'un poste la transition pour passer au convoyeur suivant ne peut pas être franchie car elle nécessite le type d'objet obtenue après actions du poste pour être franchie.

Sur la figure ci-dessous, il est possible de voir les déclarations de types d'objets présent dans le système. Elles sont séparé en trois types de declarations. Il y a les objet simple comme PALETTE, les objets composés comme STATE_PALETTE1 qui est la fusion d'une palette et d'un produit non traité, et enfin il y a les combinaisons comme COMBINED1 qui permettent à une place d'accueillir les différents types de jetons associé au combined.

CPN Tools permet de vérifier des propriétés sur les RDP créés grâce à des algorithmes de vérification. Les vérifications produites sur un RDP incluent avant tout le calcul de l'automate d'état associé au réseau de Petri, comme illustré sur la figure 19. D'autres propriétés vérifiées par CPN Tools sont des propriétés de bornitude ou de vivacité.
<figure><img src="image_17.png" /><figcaption>FIGURE 17 – Cas d'étude chaîne de production modélisé sur CPN Tools</figcaption></figure>

<figure><img src="image_18.png" /><figcaption>FIGURE 18 – Declarations des objets dans CPN Tools</figcaption></figure>

<figure><img src="image_19.png" /><figcaption>FIGURE 19 – Exemple d'un calcul des états par CPN Tools</figcaption></figure>

<figure><img src="image_20.png" /><figcaption>FIGURE 20 – Exemple de calcul de propriétés de vivacité par CPN Tools</figcaption></figure>
## C.7 Cas d'étude A.1 avec un RDP sur Romeo

Voici la représentation du premier cas d'étude "Feux tricolore" représenté sur Romeo il est composé de 12 places ils représentent les cadrants Nord-Sud et Ouest-Est ainsi que chaque états des feux rouge, orange et vert coloré dans leurs couleurs respectives sur l'image.

<figure><img src="image_21.png" /><figcaption>FIGURE 21 - Cas d'étude Feux tricolore sur Romeo</figcaption></figure>

## C.8 Cas d'étude A.2 avec un RDP sur Romeo

Voici la reproduction du deuxième cas d'étude "Kanban" représenté sur Romeo on observe deux places et une transitions pour chaque contenaire et trois places pour chacun des postes pour permettre le passage de 4 objets par 4 objets et pour les postes il doivent limiter le passage des objets et modifier les objets un à un ainsi que débloquer le passage pour 4 nouveaux objets.

<figure><img src="image_22.png" /><figcaption>FIGURE 22 - Cas d'étude Kanban sur Romeo</figcaption></figure>

## C.9 Cas d'étude A.3 avec un RDP sur Romeo

La spécification du réseau de Petri (PN) avec Romeo [GLMR05] est donnée dans Figure 23. Dans ce RDP la structure est différente de CPN Tools et Tina car l'outils a un semblant de modularité avec des liens invisibles crée par l'ajout de variables qui permet de bloquer ou laisser passer des jetons 23. Ce RDP possède 9 parties dont 4 pour les convoyeurs, 4 autres pour les postes et un dernier pour la source de palette, la source pour les objets est intégré a la partie du poste 1. Les postes décrivent les actions suivantes :

- Poste 1 : Un robot charge deux objets un par un sur la palette bloquer en attendent les objets.

- Poste 2 : Un opérateur récupère un objet d'un premier bloqueur, le dépose dans une machine pour traitement, puis le replace sur la palette bloquer au seconde bloqueur.

- Poste 3 : Un opérateur récupère un objet du bloqueur, le dépose dans une machine pour traitement, puis le replace sur la palette.
— Poste 4 : Un transporteur récupère les objets de la palette bloquer pour les déposer dans un dépôt (encadré en jaune).

<figure><img src="image_23.png" /><figcaption>FIGURE 23 – Cas d'étude chaîne de production modélisé sur Romeo</figcaption></figure>

Dans Romeo, la structure du PN semble être modulaire, mais elle ne l'est pas vraiment puisque des liens cachés sont créés par l'ajout de variables (actions vertes dans la Figure 23) qui permettent de bloquer ou de faire passer des jetons. On peut également ajouter du temps aux transitions pour permettre aux transitions d'être activées dans un certain ordre. Le RDP temporisé permet la simulation pour l'évaluation des performances liées au temps.

La vérification avec Romeo couvre les aspects statiques (outil *Structural*), la vérification de l'espace d'états (outil *State Space*), l'analyse de traces (outil *checker*) et la simulation (outil *Simulator*).

Romeo permet de vérifier des propriétés par *model-checking* à l'aide du *Checker*, les propriétés pouvant être spécifiée et personnalisée avant d'être vérifiées une par une.

Romeo permet aussi de simuler un comportement pas à pas avec le Simulator (actions vertes dans la Figure 24). Un inconvénient est de ne pas pouvoir déterminer un scénario, éventuellement aléatoire pour couvrir une trace d'exécution complète sur un espace de temps donné.
<figure><img src="image_24.png" /><figcaption>FIGURE 24 – Vérification de propriété sur Romeo</figcaption></figure>

<figure><img src="image_25.png" /><figcaption>FIGURE 25 – Simulation pas à pas sur Romeo</figcaption></figure>
## C.10 Cas d'étude A.1 avec un automate sur UPPAAL

La Figure 26 représente le modèle pour le cas 1 avec UPPAAL.

à ajouter

<caption>FIGURE 26 – Cas d'étude Feux tricolores modélisé sur UPPAAL</caption>

## C.11 Cas d'étude A.2 avec un automate sur UPPAAL

La Figure 27 représente le modèle pour le cas 1 avec UPPAAL.

A insérer

<caption>FIGURE 27 – Cas d'étude Kanban modélisé sur UPPAAL</caption>

## C.12 Cas d'étude A.3 avec un automate sur UPPAAL

Voir le texte de l'article pour le modèle.

On peut observer sur la Figure 28 que les propriétés vérifié sont signalées en vert et en rouge celles dont la vérification a échoué.

<figure><img src="image_26.png" /><figcaption>FIGURE 28 – Vérification de propriété sur UPPAAL</figcaption></figure>

Pour la simulation, nous avons obtenu l'extrait suivant de la trace d'exécution :

```json
{"init": {"locs": [0, 0, 0, 5, 0, 0, 0, 5, 0, 0, 5, 0, 0, 0, 0], "vars": [0, 0, 0, 3, 10],
"fpvars": [], "clocks": [0, 0, 0, 0, 0], "lim": {"max": 1.0, "strict": false}},
"transitions": [{"delay": 0.03589417110197246, "edges": [{"parts": [{"procnum": 13,
"eid": 0, "sel vals": []}]}, {"parts": [{"procnum": 0, "eid": 14, "sel vals": []}]}],
"state": {"locs": [1, 0, 0, 5, 0, 0, 0, 5, 0, 0, 5, 0, 0, 0, 0], "vars": [0, 0, 0, 2, 10],
"fpvars": [], "clocks": [0.0, 0.03589417110197246, 0.03589417110197246],
"lim": {"max": 0.9641058288980275, "strict": false}}, {"delay": 0.7239756981476212,
"edges": [{"parts": [{"procnum": 0, "eid": 1, "sel vals": []}]}, {"parts": [{"procnum": 1,
"eid": 2, "sel vals": []}]}, {"state": {"locs": [1, 1, 0, 5, 0, 0, 0, 5, 0, 0, 5, 0, 0, 0],
"vars": [0, 0, 0, 2, 10], "fpvars": [], "clocks": [0.0, 0.7598698692495937,
0.7598698692495937], "lim": {"max": 0.24013013075040635, "strict": false}}],
"delay": 0.1596498075028585, "edges": [{"parts": [{"procnum": 1, "eid": 3,
```
"sel vals":[]]},{"parts": [{"procnum":2,"eid":5,"sel vals":[]]}],
"state":{"locs":[1,2,1,5,0,0,0,5,0,0, ...

C.13 Cas d'étude A.1 sur SPIN

La Figure 29 représente le modèle pour le cas 1 avec SPIN.

à ajouter

<caption>FIGURE 29 – Cas d'étude Feux tricolores modélisé sur SPIN</caption>

C.14 Cas d'étude A.2 sur SPIN

La Figure 30 représente le modèle pour le cas 1 avec SPIN.

à ajouter

<caption>FIGURE 30 – Cas d'étude Kanban modélisé sur SPIN</caption>

C.15 Cas d'étude A.3 sur SPIN

Le fonctionnement du système a également été vérifié à l'aide du vérificateur de modèles SPIN [Hol04], modélisant le comportement en langage Promela. Chaque station est représentée par un processus concurrent (*proctype*) et les transferts de palettes sont modélisés par des canaux synchrones.

Chaque poste de travail est modélisé comme un processus :

- Poste1() initialise une palette vide, y place deux objets, puis la transmet au poste suivant.

- Poste2() récupère la palette, traite un premier objet, puis attend une synchronisation.

- Poste3() traite le second objet, uniquement après synchronisation avec le poste 2.

- Poste4() reçoit la palette avec les objets traités, les retire, puis retourne la palette vide au poste 1.

Les interactions entre les postes de travail sont modélisées à l'aide de canaux synchrones, comme indiqué dans la Figure 31.

- chan posteX_to_posteY = [0] of {int} permet de transmettre une palette entre deux postes.

- chan sync_poste2_poste3 = [0] of {int} assure une synchronisation stricte entre les opérateurs des postes 2 et 3.

La modélisation inclut également des constantes et variables globales représentant l'état des palettes et la disponibilité des ressources du système (cf. Figure 31). Les constantes permettent de suivre l'état des palettes à chaque étape du processus et facilitent l'identification des transitions entre états dans les processus. Les variables modélisent la disponibilité des ressources critiques utilisées par les opérateurs ou machines.

En pratique, le système a été représenté en définissant un processus pour chaque poste de travail. Le comportement de chaque opérateur ou machine a été décrit étape par étape. Des canaux de communication ont été utilisés pour simuler les déplacements des palettes et coordonner les actions entre les postes. Une synchronisation spécifique a été ajoutée entre les
/* Définition des canaux de communication */
chan poste1_to_poste2 = [1] of {byte};
chan poste2_to_poste3 = [1] of {byte};
chan poste3_to_poste4 = [1] of {byte};
chan poste4_to_poste1 = [1] of {byte};

/* Définition des constantes */
#define PALETTE_VIDE 0
#define PALETTE_2PRODUITS 2
#define PALETTE_1PRODUIT 1
#define PALETTE_2PRODUITS_TRAITES 3

/* Variables globales */
bool produit_disponible = true;
bool machine1_libre = true;
bool machine2_libre = true;
bool chariot_libre = true;

/* Canal pour synchroniser le dépôt des produits traités */
chan sync_poste2_poste3 = [1] of {bool};

<caption>FIGURE 31 – Spécification de canaux, contantes et variables with SPIN</caption>

postes 2 et 3, à l'aide d'un canal dédié, afin de garantir que les produits soient déposés sur la
pulse dans le bon ordre. Enfin, tous les processus sont lancés dans le bloc init :

init { run Poste1(); run Poste2(); run Poste3(); run Poste4(); }

Finalement, la vérification du système a été réalisée à l'aide de propriétés LTL (Linear Temporal Logic) définies dans le modèle Promela. Certaines propriétés ont été formulées pour vérifier différents aspects du comportement du système :

/* Propriétés LTL à vérifier */
ltl termine { <> tour_complet }
ltl pas_de_blobage { []>(etat_poste1 == EXPEDITION && etat_poste2 == EXPEDITION && etat_poste3 == EXPEDITION && etat_poste4 == EXPEDITION) }
ltl ordreCorrect { [](etat_poste1 == EXPEDITION -> <> etat_poste2 == RECEPTION) }
ltl securite_machines { []!((!machine1_libre) && (!machine2_libre) && p2_en_attente && p3_en_attente) }
ltl vivacite { [](produit_disponible -> <>tour_complet) }

<caption>FIGURE 32 – Vérification des propriétés avec SPIN</caption>

Le listing suivant décrit l'exécution d'un script d'analyse statique et de vérification structu-
relle de l'espace d'état :

(Spin Version 6.5.1 -- 20 December 2019)
+ Partial Order Reduction

Full statespace search for:
never claim + (termine)
assertion violations + (if within scope of claim)
acceptance cycles + (fairness disabled)
invalid end states - (disabled by never claim)

State-vector 100 byte, depth reached 97, errors: 0
423 states, stored (846 visited)
1192 states, matched
2038 transitions (= visited+matched)
6 atomic steps
hash conflicts: 0 (resolved)

Stats on memory usage (in Megabytes):
0.052 equivalent memory usage for states (stored*(State-vector + overhead))
0.284 actual memory usage for states
128.000 memory used for hash table (-w24)
0.534 memory used for DFS stack (-m10000)
128.730 total actual memory usage

unreached in prototype Poste1
rodicProp.pml:64, state 7, "p1_en_attente = 1"
```
rodicProp.pml:65, state 8, "printf('Poste1: En attente de produit\n')"
rodicProp.pml:66, state 9, "produit_disponible = 1"
rodicProp.pml:67, state 10, "p1_en_attente = 0"
(4 of 21 states)
unreached in proctype Poste2
rodicProp.pml:107, state 11, "p2_en_attente = 1"
rodicProp.pml:108, state 12, "printf('Poste2: En attente de machine libre\n')"
rodicProp.pml:109, state 13, "machine1_libre = 1"
rodicProp.pml:110, state 14, "p2_en_attente = 0"
(4 of 24 states)
unreached in proctype Poste3
rodicProp.pml:145, state 8, "p3_en_attente = 1"
rodicProp.pml:146, state 9, "printf('Poste3: En attente de machine libre\n')"
rodicProp.pml:147, state 10, "machine2_libre = 1"
rodicProp.pml:148, state 11, "p3_en_attente = 0"
(4 of 26 states)
unreached in proctype Poste4
rodicProp.pml:187, state 7, "p4_en_attente = 1"
rodicProp.pml:188, state 8, "printf('Poste4: En attente de chariot libre\n')"
rodicProp.pml:189, state 9, "chariot_libre = 1"
rodicProp.pml:190, state 10, "p4_en_attente = 0"
rodicProp.pml:206, state 21, "etat_poste4 = 0"
rodicProp.pml:207, state 22, "-end-"
(6 of 22 states)
unreached in init
(0 of 8 states)
unreached in proctype Moniteur
rodicProp.pml:227, state 1, "assert(!(((p2_en_attente&&p3_en_attente)&&!(machine1_libre))
&&!(machine2_libre))))"
rodicProp.pml:230, state 2, "((tour_complet==1))"
rodicProp.pml:231, state 3, "-end-"
(3 of 3 states)
unreached in claim termine
_spin_nvr.tmp:6, state 6, "-end-"
(1 of 6 states)
pan: elapsed time 0 seconds
```

Nous avons testé diverses propriétés telles que :

1. **Terminaison** : le système finit par effectuer un tour complet.

2. **Absence de blocage** : tous les postes atteignent l'état d'expédition, garantissant l'absence de blocage.

3. **Ordre correct** : lorsque le poste 1 expédie une palette, le poste 2 finit par la recevoir.

4. **Sécurité des machines** : les deux machines ne peuvent pas être simultanément indisponibles avec les deux opérateurs en attente.

5. **Vivacité** : si un produit est disponible, un tour complet finit par être effectué.

Par exemple, l'exécution de la vérification pour la propriété `pas_de_blocage` a donné les résultats de la Figure 33.

Cette trace de vérification montre les résultats essentiels pour la propriété `pas_de_blocage`. SPIN a trouvé un cycle d'acceptation à la profondeur 111, ce qui confirme la validation de notre propriété. Le système a exploré 55 états et transitions pour parvenir à cette conclusion, avec une profondeur maximale de 112. La présence d'une erreur signalée est normale et attendue, car SPIN fonctionne en cherchant des contre-exemples à la négation de la propriété testée. Le message "search not completed" est normal car SPIN s'arrête automatiquement dès qu'il trouve la preuve que notre propriété est correcte.

# D Analyse de l' existant

Dans cette section nous présentations des recherches sur l'analyse de l' existant.
```
pan:1: acceptance cycle (at depth 111)
pan: wrote rodic_prop.pml.trail
```

```
(Spin Version 6.5.1 -- 20 December 2019)
Warning: Search not completed
  + Partial Order Reduction
```

Full statespace search for:
```
never claim                 + (pas_de_blocage)
assertion violations      + (if within scope of claim)
acceptance cycles         + (fairness disabled)
invalid end states         - (disabled by never claim)
```

State-vector 108 byte, depth reached 112, errors: 1
```
55 states, stored
0 states, matched
55 transitions (= stored+matched)
3 atomic steps
hash conflicts:      0 (resolved)
```

<caption>FIGURE 33 – Exécution de la propriété pas de blocage</caption>

## D.1 IA Générative

Prompt : je cherche une classification des systèmes à événements discrets prenant en compte modélisation, vérification et simulation

La classification des **systèmes à événements discrets (SED)** peut être abordée selon plusieurs dimensions, notamment la **modélisation**\*, la **véرification**\*\* et la **simulation**\*\*.

Voici une classification structurée et détaillée prenant en compte ces trois axes :

---

### 1. **Par Type de Modèle Utilisé**

#### a) **Réseaux de Petri (Petri Nets)**

* **Modélisation**\*\* : Formelle, graphique, bien adaptée aux systèmes concurrents et synchrones.

* **Vérification**\*\* : Analyse de propriétés comme l'accessibilité, la vivacité, le blocage, etc.

* **Simulation**\*\* : Possible à travers des outils comme CPN Tools, PIPE, WoPeD.

#### b) **Automates à États Finis (Finite State Machines - FSM)**

* **Modélisation**\*\* : Représenté les états et transitions selon des événements.

* **Vérification**\*\* : Analyse de séquences valides, détection d'erreurs d'états.

* **Simulation**\*\* : Intégrée dans divers outils (ex. UML state diagrams).

#### c) **Automates Temporisés (Timed Automata)**

* **Modélisation**\*\* : Extension des FSM avec des horloges ; modélise des contraintes temporelles.

* **Vérification**\*\* : Utilisation d'outils comme UPPAAL pour prouver des propriétés temporelles.

* **Simulation**\*\* : Simulation des comportements temporels via UPPAAL.

#### d) **Langages de Modélisation à Événements Discrets**

* **DEVS (Discrete Event System Specification)**\*\*

* **Modélisation**\*\* : Hiérarchique, modulaire, formel.

* **Vérification**\*\* : Moins naturel, nécessite souvent des traductions vers d'autres formalismes.

* **Simulation**\*\* : Très puissant, natif dans DEVS (CD\*\*, adevs, MS4 Me).

* **Statecharts (par David Harel)**\*\*

* **Modélisation**\*\* : Étend les automates avec hiérarchie, concurrence, synchronisation.

* **Vérification**\*\* : Possible avec des outils comme Rhapsody ou Yakindu.

* **Simulation**\*\* : Simulation directe avec les outils de modélisation.
---

## 2. **Par Objectif Principal**

<table><thead><tr><th>Objectif</th><th>Formalismes courants</th><th>Remarques</th></tr></thead><tbody><tr><td>**Modélisation**</td><td>DEVS, Réseaux de Petri, FSM, Statecharts</td><td>Structuration, abstraction, modularité.</td></tr><tr><td>**Vérification**</td><td>Automates temporisés, Réseaux de Petri, Kripke structures</td><td>Utilisation de méthodes formelles, model-checking.</td></tr><tr><td>**Simulation**</td><td>DEVS, Statecharts, outils de co-simulation</td><td>Exploration du comportement dynamique.</td></tr></tbody></table>

---

## 3. **Par Niveau de Formalisme**

<table><thead><tr><th>Niveau</th><th>Exemples</th><th>Usage typique</th></tr></thead><tbody><tr><td>**Formalisme faible**</td><td>Statecharts, UML, Simulink (discret)</td><td>Développement rapide, simulation.</td></tr><tr><td>**Formalisme moyen**</td><td>FSM, DEVS</td><td>Bon équilibre entre modélisation et simulation.</td></tr><tr><td>**Formalisme élevé**</td><td>Réseaux de Petri, Automates temporisés</td><td>Vérification formelle, preuve de propriétés.</td></tr></tbody></table>

---

## 4. **Par Domaine d'Application**

* **Systèmes embarqués** : Automates temporisés, Statecharts.

* **Systèmes de production** : Réseaux de Petri, DEVS.

* **Télécommunications / réseaux** : Automates stochastiques, Réseaux de files d'attente.

* **Systèmes critiques** : Model-checking sur automates temporisés ou hybrides.

---

## 5. **Synthèse Graphique (tableau récapitulatif)**

<table><thead><tr><th>Forme</th><th>Modélisation</th><th>Vérification</th><th>Simulation</th><th>Outils</th></tr></thead><tbody><tr><td>**FSM**</td><td>++</td><td>+</td><td>+</td><td>UML, SCXML</td></tr><tr><td>**Petri Nets**</td><td>+++</td><td>+++</td><td>+</td><td>PIPE, CPN Tools</td></tr><tr><td>**Timed Automata**</td><td>++</td><td>+++</td><td>+</td><td>UPPAAL</td></tr><tr><td>**DEVS**</td><td>+++</td><td>+</td><td>+++</td><td>CD++, adevs</td></tr><tr><td>**Statecharts**</td><td>++</td><td>+</td><td>++</td><td>Yakindu, Rhapsody</td></tr></tbody></table>

---

Souhaitez-vous que je vous aide à choisir un formalisme adapté à un projet ou système concret ?

Prompt : existe t-il des classification de formalismes SED ?

Oui, **plusieurs classifications des formalismes de systèmes à événements discrets (SED)** existent dans la littérature, en fonction de critères comme :

* le **niveau d'abstraction**,

* la **nature du formalisme** (formel/informel, graphique/textuel),

* l'**objectif** (modélisation, vérification, simulation),

* le **paradigme** (état-transition, synchronisation, temps, etc.).

Voici un **aperçu structuré des classifications** les plus reconnues :

---

## * 1. **Classification par Paradigme de Modélisation**

<table><thead><tr><th>Paradigme</th><th>Formalismes typiques</th><th>Caractéristiques</th></tr></thead><tbody><tr><td>**État/Transition**</td><td>Automates, FSM, Statecharts</td><td>Décrit les états discrets et les transitions.</td></tr><tr><td>**Réseaux**</td><td>Réseaux de Petri, SDF (synchronous dataflow)</td><td>Représentation des dépendances entre événements ou</td></tr><tr><td>** fonctions événementielles**</td><td>DEVS, DSDE</td><td>Basé sur la génération et la propagation d'événements.</td></tr><tr><td>**Langages à logique temporelle**</td><td>TLA+, LTL, CTL</td><td>Modélisation axée sur la vérification logique.</td></tr><tr><td>**Processus concurrents**</td><td>CSP, CCS, LOTOS</td><td>Orienté communication entre processus.</td></tr></tbody></table>

---

## * 2. **Classification selon la Temporalité**
<table><thead><tr><th>Type de formalismes</th><th>Exemples</th><th>Usage</th></tr></thead><tbody><tr><td>**Sans notion de temps**</td><td>FSM, Petri Nets (classiques)</td><td>Systèmes logiques purs.</td></tr><tr><td>**Avec temps discret**</td><td>Timed Automata, Time Petri Nets</td><td>Vérification de délais, temps d'attente.</td></tr><tr><td>**Avec temps continu**</td><td>Hybrid Automata, DEVS continu</td><td>Systèmes mixtes ou hybrides.</td></tr><tr><td>**Stochastiques**</td><td>Réseaux de files d'attente, Petri Nets stochastiques</td><td>Analyse probabiliste.</td></tr></tbody></table>

---

## * 3. **Classification par Capacité de Vérification**

<table><thead><tr><th>Type</th><th>Formalismes associés</th><th>Méthodes</th></tr></thead><tbody><tr><td>**Analytiques**</td><td>Réseaux de files, Markov, Petri Nets</td><td>Analyse mathématique.</td></tr><tr><td>**Symboliques / formels**</td><td>Automates temporisés, Kripke structures</td><td>Model checking, preuves formelles.</td></tr><tr><td>**Simulationnelles**</td><td>DEVS, Statecharts, Simulink (discret)</td><td>Observation de scénarios.</td></tr></tbody></table>

---

## * 4. **Classification par Niveau de Formalisme**

Proposé notamment par **Zeigler et al.** (créateur du formalisme DEVS), ce cadre distingue :

<table><thead><tr><th>Niveau de formalisation</th><th>Exemples</th><th>Objectifs</th></tr></thead><tbody><tr><td>**Informel**</td><td>Diagrammes UML, pseudo-code</td><td>Communication humaine.</td></tr><tr><td>**Semi-formel**</td><td>Statecharts, SysML, AADL</td><td>Outils de conception.</td></tr><tr><td>**Formel**</td><td>DEVS, Timed Automata, Petri Nets</td><td>Vérification rigoureuse.</td></tr></tbody></table>

---

## * 5. **Classification selon l'Objectif Principal**

<table><thead><tr><th>Objectif principal</th><th>Formalismes adaptés</th></tr></thead><tbody><tr><td>**Modélisation hiérarchique**</td><td>DEVS, Statecharts</td></tr><tr><td>**Spécification de comportement**</td><td>FSM, Petri Nets</td></tr><tr><td>**Vérification formelle**</td><td>Timed Automata, Petri Nets, LTL</td></tr><tr><td>**Simulation discrète**</td><td>DEVS, GPSS, Arena</td></tr></tbody></table>

---

## * Références utiles

1. **Zeigler, Bernard P.**, *Theory of Modeling and Simulation* - Classification fondée sur le formalisme DEVS.

2. **W. Reisig**, *Petri Nets: An Introduction* - Approche structurelle.

3. **J. Sifakis**, travaux sur automates temporisés (avec Alur).

4. **Grosu et Smolka**, sur la comparaison Timed Automata vs. DEVS.

5. **IEEE 1516 HLA Standard**, pour les environnements de simulation.

---

Souhaitez-vous que je vous fournisse un **diagramme de classification graphique** ou un **tableau comparatif détaillé** des formalismes SED ?
Table des matières

1 Introduction 1

2 Méthodologie 2

2.1 Etudes de cas 2

2.2 Approches SED et outils candidats 2

2.3 Analyse des Propriétés 3

2.4 Approches et outils sélectionnés 3

3 Expérimentations 3

3.1 Cas d'étude A.3 avec un RDP sur Tina 3.4.4 4

3.2 Cas d'étude A.3 avec un automate sur UPPAAL 6

4 Synthèse des résultats préliminaires 7

4.1 Généralités 8

4.2 Expressivité du langage 9

4.3 Vérification 10

4.4 Simulation 11

5 Discussion 11

6 Conclusion 13

A Études de cas support 15

A.1 Première étude de cas : Feux tricolores 15

A.2 Deuxième étude de cas : un atelier de fabrication Kanban 15

A.3 Troisième étude de cas : chaîne de production 15

B Approche, formalisme, outils 16

B.1 Les Réseaux de Pétri (RDP) 17

B.2 Les Automates 18

B.3 Algèbres de Processus 18

B.4 Simulation 20

B.5 Analyse des Propriétés 20

B.6 Outils sélectionnés 21

B.6.1 Tina v3.4.4 21

B.6.2 Romeo v3.10.5 22

B.6.3 CPN Tools v4.0.1 23

B.6.4 UPPAAL 4.1.26 23

B.6.5 Spin v. 6.5.0 23

C Application aux études de cas 24

C.1 Cas d'étude A.1 avec un RDP sur Tina 24

C.2 Cas d'étude A.2 avec un RDP sur Tina 25

C.3 Cas d'étude A.3 avec un RDP sur Tina 26

C.4 Cas d'étude A.1 avec un RDP sur CPN Tools 27

C.5 Cas d'étude A.2 avec un RDP sur CPN Tools 27

C.6 Cas d'étude A.3 avec un RDP sur CPN Tools 27
<table><tr><td>C.7</td><td>Cas d'étude A.1 avec un RDP sur Romeo</td><td>29</td></tr><tr><td>C.8</td><td>Cas d'étude A.2 avec un RDP sur Romeo</td><td>30</td></tr><tr><td>C.9</td><td>Cas d'étude A.3 avec un RDP sur Romeo</td><td>30</td></tr><tr><td>C.10</td><td>Cas d'étude A.1 avec un automate sur UPPAAL</td><td>32</td></tr><tr><td>C.11</td><td>Cas d'étude A.2 avec un automate sur UPPAAL</td><td>32</td></tr><tr><td>C.12</td><td>Cas d'étude A.3 avec un automate sur UPPAAL</td><td>32</td></tr><tr><td>C.13</td><td>Cas d'étude A.1 sur SPIN</td><td>33</td></tr><tr><td>C.14</td><td>Cas d'étude A.2 sur SPIN</td><td>33</td></tr><tr><td>C.15</td><td>Cas d'étude A.3 sur SPIN</td><td>33</td></tr><tr><td>D</td><td>Analyse de l'existant</td><td>36</td></tr><tr><td>D.1</td><td>IA Générative</td><td>36</td></tr></table>