Fault Diagnosis And Opacity Verification Of Discrete Event Systems By Petri Nets

In modern society,discrete event systems have extremely wide practical application backgrounds,such as flexible manufacturing systems,computer communication networks,and urban transportation systems.As one of the challenging fields in control theory,the study of discrete event systems has become an important branch of control theory research,which has drawn great attention from the international control theory community.The evolution of discrete event systems is event-driven,and the moments in which events occur are discrete.There are extremely intricate interactions between these events.In particular,dangerous factors such as physical failure and information leakage always threaten the safe operation of the system.In recent years,the importance of system security has aroused the attention of academia and industry on formal methods of system security.Based on system security,people have proposed concepts such as fault diagnosis,opacity,and critical observability.In particular,fault diagnosis includes monitoring system's behavior,determining the occurrence of any failure,and determining its type or source.Opacity focuses on the information security and privacy issues of a system.It aims to determine whether the secret behavior of a given system remains opaque to external observers.Due to the partial observability of the system,external observers of the system(including diagnosers and intruders)cannot fully observe all the events that occur in the system.The notion of critical observability derives from the security application of cyber-physical systems,its main aim is to detect whether the current state of the system is in a critical set representing dangerous operations.In this thesis,the fault diagnosis,opacity verification,and critical observability of discrete event systems are studied by using Petri net as modeling tool and integer linear programming.The main results of this thesis are outlined as follows.1.We first use the technique of integer linear programming to solve the problem of decentralized on-line fault diagnosis for discrete event systems in a Petri net framework.The decentralized architecture consists of a set of local sites communicating with a coordinator that decides whether the system behaviour is normal or subject to some possible faults.To this aim,some results allow defining the rules applied by the coordinator and the local sites to provide the global diagnosis results.Moreover,two protocols for the detection and diagnosis of faults are proposed: they differ for the information exchanged between local sites and coordinator and the diagnostic capability.In addition,a sufficient and necessary condition under which the second presented protocol can successfully diagnose a fault in the decentralized architecture is proved.Finally,some examples are presented to show the efficiency of the proposed approach.2.Opacity is a security and privacy property that evaluates whether an external observer(intruder)can infer a secret of a system by observing its behaviour.This thesis is the first work that proposes an on-line approach to address the problem of current-state opacity in discrete event systems modeled in a labeled Petri net framework and by observing its evolution.An observation of the system is said to be current-state opaque if the intruder is unable to determine whether the current state of the system is within a set of secret states,otherwise it is said to be not current-state opaque.The proposed approach to verify the current-state opacity works on-line: the verification algorithm waits for the occurrence of an observable event and uses integer linear programming problem solutions to verify if the behaviour of the system is current-state opaque to the intruder under the given observation.Moreover,the proposed method is applied in two different settings: i)a centralized approach where the intruder has full knowledge of the system model but can partially observe the system behaviour;ii)a decentralized approach where a set of intruders can observe different event sets and collaborate with a coordinator to disclose the same secret.Finally,experimental results are presented to demonstrate that the proposed method is suitable for large scale net systems,which cannot be implemented by a traditional method based on the state computation.3.This thesis deals with a problem related to the observability of discrete event systems: the initial-state opacity.Given a set of system states(the secret),a system observation is called initial-state opaque if an agent(named intruder),who can partially observe the system,cannot determine whether the set of initial states consistent with an event sequence is included in the secret.Such a character can describe security problems in cyber-infrastructures,such as Internet and mobile communication networks or national defense service systems.This work presents a novel on-line methodology to verify the notion of initial-state opacity of discrete event systems that are modeled by labeled Petri nets.By working on-line,the intruder records an event and exploits integer linear programming problem for checking the initial-state opacity of the system's evolution under the given observation.Compared with the traditional methods that need to compute the reachability graph,a set of examples show that the presented methodology is more efficient.4.Critical observability of discrete event systems is also an observability related problem of discrete event systems.In particular,if the observer can detect that the system is or is not in critical states by its partial observation,a net system is said to be critically observable.In this thesis,two methods are first proposed to verify the critical observability of two kinds of Petri net systems(safe Petri nets and Petri nets with unknown initial marking)by using integer linear programming,which do not need to compute the reachability graph thus avoiding the state explosion problem.In addition,we demonstrate the validity and the effectiveness of the proposed methods through some examples.