Une approche formelle basée BRS pour la spécification et la vérification des architectures des systèmes Multi-Agents

Le paradigme multi-agent (SMA) peut être particulièrement adapté à la construction de systèmes distribués, ouverts et concurrents. Il est reconnu, comme étant un moyen excellent et adéquat pour développer une variété d'applications industrielles de grande envergure dans différents domaines, tels que : la gestion des réseaux distribués, l'informatique en grille, les services web intelligents, etc. Ces systèmes doivent souvent opérer dans des environnements dynamiques et faire face au défi de l'évolution constante de leurs exigences ; donc ils doivent être flexibles, robustes et capables de s'adapter à leurs environnements. Ceci, rend difficile la conception et le développement des systèmes multi-agents reconfigurables. Dans ce travail, nous nous basons sur les méthodes formelles pour gérer la complexité des aspects liés à la conception des architectures de SMA. Plus précisément, nous proposons une approche de modélisation formelle basée sur les systèmes réactifs bigraphiques (BRS) pour la spécification et la vérification des architectures des systèmes multi-agents et leur reconfiguration. Les BRS présentent une solution prometteuse et efficace pour le développement des SMA sûrs et de qualité. En outre, ils permettent la vérification des propriétés pertinentes des SMA à l'aide d'outils de vérification de modèles bigraphiques.