, Nous avons présenté, dans [2], une reformulation de l'analyse de la K-diagnosticabilité en unprobì eme de model-checking. L'idéé etait d'associeràassocierà la structure de Kripke (qui correspond au twin plant) une fonction delay() qui permet de compter le nombre de fois (en terme d'´ etats) o` u le modèle est resté dans une situation ambiguë
, pour une valeur donnée de K, il suffit de s'assurer que la valeur retournée par fonction delay() reste toujours inférieurè a K. Cette propriété peutêtrepeutêtre formulée par leprobì eme de model-checking suivant
, sinon il ne l'est pas La 2 ` eme question dans l'analyse de la K-diagnosticabilité est de déterminer la valeur minimale de K garantissant la diagnosticabilité (la K min -diagnosticabilité) Une technique, basée sur l'analyse incrémentale de la K-diagnosticabilité, a ´ eté utilisée dans [12]. L'adaptation directe de cette technique dans le contexte de model-checking consistè a introduire une incrémentation dans la spécificationspécificationà vérifier, i.e. par exemple, et ainsi de suite, avec ? qui représente la condition de diagnostic
, exprimer des propriétés impliquant des informations quantitatives en termes de nombre d'´ evènements ou d'´ etats. Par exemple, la détermination de délai maximal (ou minimal) entre deux spécifications CTL. Parmi les outils qui acceptent ce type de spécification, le model-checker NuSMV (que nous allons utiliser, par la suite
, la spécification correspondante est de cette forme : MAX [? , ¬?], avec l'expression " MAX " indiquant la recherche du délai maximal et ? représente la spécification CTL qui traduit le fait de rentrer dans une situation d'ambigu¨?téambigu¨?té, i.e. unétatunétat incertain, et ¬? indiquant la disparition de la situation d'ambigu¨?téambigu¨?té
, le résultat est soit un entier fini, qui représente donc la valeur K min , soit l'infini pour dire qu'il n'existe pas de délai maximal et par conséquent
, durant la construction des modèles intermédiaires, plusieurs techniques ontétéontété développéesauteur a essayé de tirer parti de la propriété de symétrie du twin plant en considérant l'occurrence desévènements desévènements fautifs uniquement sur l'une des copies du modèle. Par conséquent, ií elimine, a priori, le comportement certainement fautif du twin plant. [14, 13] ont proposé une approche, dans le cadre de l'analyse de la codiagnosticabilité, basée sur de multiples compositions synchrones entre le modèle et des motifs de supervision, dont le but est de générer aussi le comportement ambigu, La technique a une complexité polynomiale (O(|Q| 2 × (? ? ? f ))), avec |Q| le nombre d'´ etats du modèle. L'originalité de notre approche par rapportàrapportà ces travaux consiste en la décompositiondécompositionà priori de modèles tout en tirant
, ´ etats du twin-plant qui est utilisé pour la vérification de la diagnosticabilitédiagnosticabilitéà proprementparlé , ce qui améliore nettement le processus de la vérification. Finalement, nous avons fourni une spécification dans la logique temporelle RT-CTL pour analyser la K min -diagnosticabilité comme unprobì eme de model-checking. Par ailleurs, dans l'optique de proposer une reformulation générale et unifiée desprobì emes de diagnostic et diagnosticabilité des fautes, nous envisageons d'´ etendre nos travaux pour prendre en compte des types plus complexes de fautes
, Diagnosability analysis of input/output discrete event system using model checking. The 5th International Workshop on Dependable Control of Discrete Systems, 2015.
, Introduction to discrete event systems, 2007.
, NUSMV: a new symbolic model checker, International Journal on Software Tools for Technology Transfer (STTT), vol.2, issue.4, 2000.
DOI : 10.1007/s100090050046
, Formal verification of diagnosability via symbolic model checking, Int. Joint Conference on Artificial Intelligence, 2003.
, Peled. Model Checking, 1999.
, Efficient computation of most permissive observers in dynamic sensor activation problems, Int. Workshop on Logical Aspects of Fault-Tolerance, pp.1-28, 2011.
, Symbolic testing of diagnosability. 20th International Workshop on Principles of Diagnosis (DX-09), pp.131-138, 2009.
, A polynomial algorithm for testing diagnosability of discrete-event systems, IEEE Transactions on Automatic Control, issue.8, pp.46-1318, 2001.
, Failure Diagnosis of Discrete-Event Systems With Linear-Time Temporal Logic Specifications, IEEE Transactions on Automatic Control, vol.49, issue.6, pp.934-945, 2004.
DOI : 10.1109/TAC.2004.829616
, is-programmer.com/posts/ 45619, 2014.
, Toward an efficient approach for diagnosability analysis of DES modeled by labeled Petri nets, 2014 European Control Conference (ECC), 2014.
DOI : 10.1109/ECC.2014.6862505
URL : https://hal.archives-ouvertes.fr/hal-00999387
, Polynomial Time Verification of Decentralized Diagnosability of Discrete Event Systems, IEEE Transactions on Automatic Control, vol.56, issue.7, pp.1679-1684, 2011.
DOI : 10.1109/TAC.2011.2124950
, Decentralized failure diagnosis of discrete event systems, Part A : Systems and Humans, pp.384-395, 2006.
, Diagnosability of discrete-event systems, IEEE Transactions on Automatic Control, vol.40, issue.9, pp.1555-1575, 1995.
DOI : 10.1109/9.412626
, Polynomial-time verification of diagnosability of partially observed discrete-event systems, IEEE Transactions on Automatic Control, issue.9, pp.47-1491, 2002.
, Fault diagnosis in discrete-event systems: Framework and model reduction, IEEE Transactions on Automatic Control, vol.48, issue.7, pp.1199-1212, 2003.
DOI : 10.1109/TAC.2003.814099
, Overview of fault diagnosis methods for Discrete Event Systems, Annual Reviews in Control, vol.37, issue.2, pp.308-320, 2013.
DOI : 10.1016/j.arcontrol.2013.09.009