Une Approche Basée sur la Logique TPN-TCTL pour la Conception Sûre des Systèmes Embarqués
La criticité des systèmes embarqués nécessite de garantir un niveau de sûreté de fonctionnement convenable. Un des problèmes principaux rencontrés lors d’une étude de sûreté de fonctionnement de ces systèmes est la prise en compte de manière efficace et réaliste des contraintes de fonctionnement en temps réel auxquelles ils sont soumis. Dans cet article, nous proposons une approche d’analyse de la sûreté de fonctionnement des systèmes embarqués qui s’appuie sur un cadre formel basé sur l’équivalence entre l’accessibilité dans les réseaux de Petri temporels et la prouvabilité d’une formule en logique temporelle temps-réel TCTL. La traduction du réseau de Petri en logique TCTL permet de proposer une nouvelle définition formelle de la notion de scénario qui mène le système vers un état redouté (dangereux) à partir d’un état de fonctionnement normal, afin de comprendre les raisons de la dérive qui peut avoir des conséquences dramatiques pour le système et l’utilisateur, et prévoir les configurations nécessaires qui permettent de les éviter dès la phase de conception du système.
Afifa GHENAI, Mohamed BENMOHAMMED