Verification of Current-State Opacity in Time Labeled Petri Nets With Its Application to Smart Houses
Tao Qin, Li Yin, Naiqi Wu, Zhiwu Li
Abstract
This work addresses the verification of current-state opacity with respect to a real-time observation generated from time-dependent systems. The secret behavior of a time-dependent system is defined as a set of states in a time labeled Petri net. The current-state opacity of a real-time observation means that a given secret remains opaque to the intruder who can partially observe the system behavior in the framework of a time labeled Petri net at a given time instant. We introduce a novel directed graph, called a parallel state class graph, to represent the parallel evolution of time-dependent systems exhaustively. Based on the parallel state class graph, we design an algorithm for the construction of a critical observer and show that the current-state opacity of a real-time observation in time labeled Petri nets can be efficiently solved by the critical observer. This approach is computationally competitive since the critical observer can be constructed by solving a number of linear programming problems. <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Note to Practitioners</i> —In computer-integrated real-time systems, their correctness-related properties usually depend on time constraints. System opacity guarantees that particular system information cannot be disclosed or inferred by external observers, which is a generalization of many information flow properties associated with system safety, particularly in aerospace, automotive, and healthcare domains. This research addresses the verification problem of this property for a discrete event system modeled with time labeled Petri nets. By developing a graph-theoretical structure that can be readily managed by security engineers, a type of diagram called a critical observer is derived which is able to detect the privacy of the system at a given time instant. This research provides a systematic and efficient approach for practitioners to check a desired privacy strategy of time-constrained safety systems.