Current-state opacity modelling and verification in partially observed Petri nets.

*(English)*Zbl 1440.93024Summary: System opacity is a widely studied security notion, implying that a secret behaviour of a given system cannot be seen or assessed by an external observer based on the system evolution. This work deals with the problem of current-state opacity formulation and verification in the context of discrete event systems modelled with partially observed Petri nets (POPNs) (i.e., Petri nets containing place sensors that measure the number of tokens in observable places and event sensors that indicate the firing of observable transitions). A Petri net system is recognized as current-state opaque if the current-state estimate is never entirely contained in the set of secret states. In this regard, we introduce the notion of discernible markings to design a reduced state estimator called a discernible reachability graph, and then come up with formal modelling of current-state opacity in POPN systems. The main idea of the proposed approach consists in proving that if a system is current-state opaque, its current-state estimate, possibly established by an intruder, contains at least one non-secret state. We exploit the mathematical feasibility to formulate this concept by defining and solving an integer linear programming problem with respect to a given secret and an observation sequence collected from sensors. In the light of the proposed modelling, necessary and sufficient conditions are proposed for opacity verification, and examples are given to expose the results.

##### MSC:

93B03 | Attainable sets, reachability |

93C65 | Discrete event control/observation systems |

93-10 | Mathematical modeling or simulation for problems pertaining to systems and control theory |

68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |

90C10 | Integer programming |

PDF
BibTeX
XML
Cite

\textit{I. Saadaoui} et al., Automatica 116, Article ID 108907, 10 p. (2020; Zbl 1440.93024)

Full Text:
DOI

##### References:

[1] | Ahmad, Farooq; Huang, Hejiao; Wang, Xiaolong, A technique for reachability graph generation for the Petri net models of parallel processes, International Journal of Electrical and Electronics Engineering, 3, 57-61 (2009) |

[2] | Baldan, Paolo; Beggiato, Alessandro, Multilevel transitive and intransitive non-interference, causally, Theoretical Computer Science, 706, 54-82 (2018) · Zbl 1380.68292 |

[3] | Basile, Francesco; De Tommasi, Gianmaria, An algebraic characterization of language-based opacity in labeled Petri nets, IFAC-PapersOnLine, 51, 7, 329-336 (2018) |

[4] | Basile, Francesco; De Tommasi, Gianmaria; Sterle, Claudio, Non-interference enforcement in bounded Petri nets, (Proc. 2018 IEEE conference on decision and control (2018), IEEE), 4827-4832 |

[5] | Ben-Kalefa, Majed; Lin, Feng, Opaque superlanguages and sublanguages in discrete event systems, Cybernetics and Systems, 47, 392-426 (2016) |

[6] | Bisschop, Johannes, AIMMS optimization modeling (2006), Lulu. com |

[7] | Bryans, Jeremy W.; Koutny, Maciej; Mazaré, Laurent; Ryan, Peter Y. A., Opacity generalised to transition systems, (Proc. international workshop on formal aspects in security and trust (2005), Springer), 81-95 |

[8] | Bryans, Jeremy W.; Koutny, Maciej; Mazaré, Laurent; Ryan, Peter Y. A., Opacity generalised to transition systems, International Journal of Information Securit, 7, 421-435 (2008) |

[9] | Bryans, Jeremy W.; Koutny, Maciej; Ryan, Peter Y. A., Modelling opacity using Petri nets, Electronic Notes in Theoretical Computer Science, 121, 101-115a (2005) · Zbl 1272.68292 |

[10] | Cabasino, Maria Paola; Giua, Alessandro; Pocci, Marco; Seatzu, Carla, Discrete event diagnosis using labeled Petri nets. An application to manufacturing systems, Control Engineering Practice, 19, 989-1001 (2011) |

[11] | Cabasino, Maria Paola; Giua, Alessandro; Seatzu, Carla, Fault detection for discrete event systems using Petri nets with unobservable transitions, Automatica, 46, 1531-1539 (2010) · Zbl 1201.93074 |

[12] | Cong, X. Y.; Fanti, M. P.; Mangini, A. M.; Li, Z. W., On-line algorithm for current state opacity enforcement in a Petri net framework, IFAC-PapersOnLine, 51, 7, 349-354 (2018) |

[13] | Cong, Xuya; Fanti, Maira Pia; Mangini, Agostino Marcello; Li, Zhiwu, On-line verification of initial-state opacity by Petri nets and integer linear programming, ISA Transactions (2019) · Zbl 1401.93043 |

[14] | Hadjicostis, Christoforos N.; Keroglou, Christoforos, Opacity formulations and verification in discrete event systems, (Proc. emerging technology and factory automation (ETFA), 2014 IEEE (2014), IEEE), 1-12 · Zbl 1398.93216 |

[15] | Jacob, Romain; Lesage, Jean-Jacques; Faure, Jean-Marc, Overview of discrete event systems opacity: Models, validation, and quantification, Annual Review of Control, 41, 135-146 (2016) |

[16] | Jussien, Narendra, Rochart, Guillaume, & Lorca, Xavier (2008). Choco: an open source java constraint programming library. In Proc. workshop on open-source software for integer and contraint programming (pp. 1-10). |

[17] | Lefebvre, Dimitri; Leclercq, Edouard; Guerin, François, Design of observations graphs for partially observed Petri nets: Application to the diagnosability analysis of DES, (Proc. 52nd IEEE annual conf. decision control (2013), IEEE), 6329-6334 |

[18] | Murata, Tadao, Petri nets: Properties, analysis and applications, Proceedings of the IEEE, 77, 541-580 (1989) |

[19] | Ru, Yu; Hadjicostis, Christoforos N., Fault diagnosis in discrete event systems modeled by partially observed Petri nets, Discrete Event Dynamic Systems, 19, 4, 551 (2009) · Zbl 1180.93069 |

[20] | Saboori, Anooshiravan; Hadjicostis, Christoforos N., Notions of security and opacity in discrete event systems, (Proc. 46th IEEE conf. decision control (2007), IEEE), 5056-5061 |

[21] | Saboori, Anooshiravan; Hadjicostis, Christoforos N., Verification of initial-state opacity in security applications of discrete event systems, Information Sciences, 246, 115-132 (2013) · Zbl 1320.68119 |

[22] | Saboori, Anooshiravan; Hadjicostis, Christoforos N., Current-state opacity formulations in probabilistic finite automata, IEEE Transactions on Automatic Control, 59, 120-133 (2014) · Zbl 1360.68570 |

[23] | Silva, Manuel; Terue, Enrique; Colom, José Manuel, Linear algebraic and linear programming techniques for the analysis of place/transition net systems, (Advanced course on petri nets (1996), Springer), 309-373 · Zbl 0926.68086 |

[24] | Tong, Yin; Li, Zhiwu; Seatzu, Carla; Giua, Alessandro, Decidability of opacity verification problems in labeled Petri net systems, Automatica, 80, 48-53 (2017) · Zbl 1370.93172 |

[25] | Tong, Yin; Li, Zhiwu; Seatzu, Carla; Giua, Alessandro, Verification of state-based opacity using Petri nets, IEEE Transactions on Automatic Control, 62, 2823-2837 (2017) · Zbl 1369.68265 |

[26] | Wu, Yi-Chin; Lafortune, Stéphane, Comparative analysis of related notions of opacity in centralized and coordinated architectures, Discrete Event Dynamic Systems, 23, 3, 307-339 (2013) · Zbl 1272.93084 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.