|
Résumé :
|
De nos jours, de nombreux systèmes à événements discrets deviennent de plus en plus complexes, structurellement dynamiques et interconnectés de manière variable. Ces systèmes sont conçus pour pouvoir modifier leur structure et/ou leur topologie, au moment de l’exécution, afin de s’adapter à des nouvelles circonstances/exigences. En tant qu’outil formel, l’utilisation de réseaux de Petri dans l’étude de tels systèmes attire de nombreux chercheurs. Bien que les réseaux de Petri (bas ou haut niveau) constituent un outil puissant et expressif, ils ne sont pas en mesure de spécifier/vérifier, de manière naturelle, des systèmes avancés dotés de structures dynamiques. En effet, les systèmes prenant en charge des environnements volatils, des variations continues et des structures reconfigurables devraient être extrêmement complexes. Pour surmonter ce problème, les chercheurs enrichissent les réseaux de Petri avec la reconfigurabilité. Néanmoins, augmenter le pouvoir de modélisation d’un formalisme diminue son pouvoir de décision. En fait, plusieurs propriétés deviennent indécidables. Par conséquent, les extensions proposées dans la littérature introduisant la reconfigurabilité dans les réseaux de Petri tentent de trouver un compromis entre les niveaux de modélisation et de vérification. Dans cette thèse, on définit trois approches – développées incrémentalement – pour la modélisation et la vérification des réseaux de Petri stochastiques généralisés (GSPNs) reconfigurables, tout en maintenant la vérifiabilité de plusieurs propriétés avec une complexité réduite. En premier lieu, on propose un formalisme, appelé GSPNs avec topologie modifiable (GSPNs-RT), qui étend les GSPNs en permettant la modélisation de topologies dynamiques et la transformation de GSPNs-RT en GSPNs équivalents, afin de tirer pleinement d’avantages des outils standard proposés pour la vérification des GSPNs. Ensuite, on propose un autre formalisme, appelé GSPNs dynamiques (D-GSPNs), qui permet de modéliser des structures dynamiques (les ensembles de places et de transitions sont dynamiques) et transforme les D-GSPNs en GSPNs équivalents. Cette transformation peut avoir lieu lorsque le modèle original disposent d’un nombre fini de configurations. Enfin, on étend les GSPNs à un formalisme reconfigurable, appelé GSPNs reconfigurable (RecGSPNs), qui prend en charge une plus large gamme de changements structurels possibles que ce qui est autorisé dans les approches existantes, ainsi que, permet à tout GSPN reconfigurable d’avoir un nombre infini de configurations tout en préservant la décidabilité de plusieurs propriétés importantes.
|
