Vérification formelle d'un modèle BPMN à durée limitée avec un courtier de messages utilisant des automates temporisés

Key Points

• Ce travail démontre l'efficacité des automates temporisés pour vérifier les modèles BPMN, en assurant qu'ils respectent les contraintes temporelles.
• Les résultats clés révèlent que le processus de model checking a validé avec succès les propriétés à durée limitée dans des conditions spécifiques.
• La vérification formelle a été conduite à l'aide d'automates temporisés pour évaluer l'interaction entre le modèle BPMN et le courtier de messages.
• Cette analyse met en lumière d'éventuelles lacunes dans les implémentations BPMN, soulignant les considérations nécessaires pour les systèmes en temps réel.