Diagnosability of event patterns in safe labeled time Petri nets: a model-checking approach - LAAS - Laboratoire d'Analyse et d'Architecture des Systèmes Accéder directement au contenu
Article Dans Une Revue IEEE Transactions on Automation Science and Engineering Année : 2022

Diagnosability of event patterns in safe labeled time Petri nets: a model-checking approach

Résumé

Checking the diagnosability of a time discrete event system usually consists in determining whether a single fault event can always be identified with certainty after a finite amount of time. The aim of this paper is to extend this type of analysis to more complex behaviors, called event patterns, and to propose an effective method to check diagnosability with the use of modelchecking techniques. To do so, we propose to convert the pattern diagnosability problem into checking a linear-time property over a specific time Petri net. Note to Practitioners-This paper is motivated by the problem of improving the monitoring and the supervision of systems like automated and robotised manufacturing systems. Based on a model of the system, the paper proposes a method to assert with certainty whether the available set of sensors will always provide enough information to ensure that a complex and unexpected behavior has not happened in the system. The proposed method uses a publicly available model-checking tool to perform this analysis.
Fichier principal
Vignette du fichier
tase.pdf (5.38 Mo) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)

Dates et versions

hal-03139863 , version 1 (12-02-2021)

Identifiants

Citer

Yannick Pencolé, Audine Subias. Diagnosability of event patterns in safe labeled time Petri nets: a model-checking approach. IEEE Transactions on Automation Science and Engineering, 2022, 19 (2), pp.1151 - 1162. ⟨10.1109/TASE.2020.3045565⟩. ⟨hal-03139863⟩
66 Consultations
28 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More