Timed Output Synchronised Petri nets et Synchronized States Class Graph : formalismes pour l'étude temporelle de la sécurité des systèmes cyber-physiques
Mouna Gaouar  1  , Rabah Ammour  1@  , Isabel Demongodin  1  , Dimitri Lefebvre  2  
1 : LIS, Marseille
Aix-Marseille Université - AMU, CNRS : UMR7020
2 : Groupe de Recherche en Electrotechnique et Automatique du Havre
Université Le Havre Normandie

Les réseaux de Petri synchronisés constituent un formalisme approprié pour représenter les systèmes cyber-physiques, étant donné que l'activation des transitions est régie par l'occurrence d'événements d'entrée et qu'un ensemble de transitions activées est déclenché en une seule fois. Une extension de ce formalisme, appelée Output Synchronized Petri nets a été proposée pour générer des événements de sortie. Ainsi, le système peut être contrôlé par des événements d'entrée associés à des transitions commandables et peut être observé grâce à des événements de sortie émis par les valeurs de marquage et/ou les changements de marquage. Dans ce résumé, nous présentons une extension temporisée de ce formalisme appelée Timed Output Synchronized Petri net. Ce formalisme étant défini par des variables de temps continues (i.e., horloges), l'espace d'état qui en résulte est souvent infini. Aussi nous proposons une abstraction de cet espace sous forme de graphe de classes d'états, appelées Synchronized State Class Graph. Ces formalismes à évènements discrets présentent un cadre d'étude approprié pour appréhender l'analyse des cyber-attaques temporelles pour les systèmes cyber-physiques.



  • Poster
Personnes connectées : 1 Vie privée
Chargement...