Analysis of safeness in a Petri net-based specification of the control part of cyber-physical systems

• Autorzy: Wojnakowski Marcin , Wiśniewski Remigiusz , Bazydło Grzegorz , Popławski Mateusz

Identyfikatory

DOI

10.34768/amcs-2021-0045

• Języki publikacji: EN

Abstrakty

EN

The paper proposes an algorithm for safeness verification of a Petri net-based specification of the control part of cyber-physical systems. The method involves a linear algebra technique and is based on the computation of the state machine cover of a Petri net. Contrary to the well-known methods, the presented idea does not require obtaining all sequential components, nor the computation of all reachable states in the system. The efficiency and effectiveness of the proposed method have been verified experimentally with a set of 243 test modules (Petri net-based systems). The results of experiments show high efficiency of the proposed method since a solution has been found even for such nets where popular techniques are not able to analyze the safeness of the system. Finally, the presented algorithm is explained in detail using a real-life case-study example of the control part of a cyber-physical system.

Słowa kluczowe

EN

safeness; control part; cyber physical system; Petri net; state machine cover; place invariant

PL

bezpieczeństwo baz danych; część kontrolna; system cyberfizyczny; sieć Petriego; maszyna stanów; niezmiennik miejsca

• Wydawca: Oficyna Wydawnicza Uniwersytetu Zielonogórskiego
• Czasopismo: International Journal of Applied Mathematics and Computer Science
• Rocznik: 2021
• Tom: Vol. 31, no. 4
• Strony: 647--657
• Opis fizyczny: Bibliogr. 60 poz., rys., tab.

Twórcy

autor

Wojnakowski Marcin

• Institute of Control and Computation Engineering, University of Zielona Góra, ul. Szafrana 2, 65-516 Zielona Góra, Poland

autor

Wiśniewski Remigiusz

• Institute of Control and Computation Engineering, University of Zielona Góra, ul. Szafrana 2, 65-516 Zielona Góra, Poland

autor

Bazydło Grzegorz

• Institute of Control and Computation Engineering, University of Zielona Góra, ul. Szafrana 2, 65-516 Zielona Góra, Poland

autor

Popławski Mateusz

• Institute of Control and Computation Engineering, University of Zielona Góra, ul. Szafrana 2, 65-516 Zielona Góra, Poland

Bibliografia

• [1] Aalst, W.M.P., Wil, Hee, K. and Kees (2004). Workflow Management—Models, Methods and Systems, MIT Press, Cambridge.
• [2] Aalst, W.v.d. (2016). Process Mining: Data Science in Action, 2nd Edn, Springer, Berlin.
• [3] Badouel, E., Bernardinello, L. and Darondeau, P. (1995). Polynomial algorithms for the synthesis of bounded nets, in P.D. Mosses et al. (Eds), TAPSOFT’95: Theory and Practice of Software Development, Springer, Berlin, pp. 364–378.
• [4] Barkalov, A., Titarenko, L. and Mielcarek, K. (2018). Hardware reduction for lut-based mealy FSMs, International Journal of Applied Mathematics and Computer Science 28(3): 595–607, DOI: 10.2478/amcs-2018-0046.
• [5] Best, E., Devillers, R. and Koutny, M. (2001). Petri Net Algebra, Springer, Berlin.
• [6] Best, E. and Wimmel, H. (2000). Reducing k-safe Petri nets to pomset-equivalent 1-safe petri nets, in M. Nielsen and D. Simpson (Eds), Application and Theory of Petri Nets 2000, Springer, Berlin, pp. 63–82.
• [7] Carmona, J., Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L. and Yakovlev, A. (2008). A symbolic algorithm for the synthesis of bounded Petri nets, in K.M. van Hee and R. Valk (Eds), Applications and Theory of Petri Nets, Springer, Berlin, pp. 92–111.
• [8] Chen, C., Liu, Z., Wan, S., Luan, J. and Pei, Q. (2020). Traffic flow prediction based on deep learning in internet of vehicles, IEEE Transactions on Intelligent Transportation Systems 22(6): 3776–3789.
• [9] Cheng, A., Esparza, J. and Palsberg, J. (1995). Complexity results for 1-safe nets, Theoretical Computer Science 147(1–2): 117–136.
• [10] Clempner, J. (2014). An analytical method for well-formed workflow/Petri net verification of classical soundness, International Journal of Applied Mathematics and Computer Science 24(4): 931–939, DOI: 10.2478/amcs-2014-0068.
• [11] Cortadella, J., Kishinevsky, M., Lavagno, L. and Yakovlev, A. (1998). Deriving Petri nets from finite transition systems, IEEE Transactions on Computers 47(8): 859–882.
• [12] Dey, N., Ashour, A.S., Shi, F., Fong, S.J. and Tavares, J.M.R.S. (2018). Medical cyber-physical systems: A survey, Journal of Medical Systems 42(4) 1–13, Article no. 74.
• [13] Dideban, A. and Alla, H. (2008). Reduction of constraints for controller synthesis based on safe Petri Nets, Automatica 44(7): 1697–1706.
• [14] Du, N., Hu, H. and Zhou, M. (2020). Robust deadlock avoidance and control of automated manufacturing systems with assembly operations using Petri nets, IEEE Transactions on Automation Science and Engineering 17(4): 1961–1975.
• [15] Esparza, J., Ledesma-Garza, R., Majumdar, R., Meyer, P. and Niksic, F. (2014). An SMT-based approach to coverability analysis, in A. Biere and R. Bloem (Eds), Computer Aided Verification, Springer, Cham, pp. 603–619.
• [16] Fabre, E. (2006). On the construction of pullbacks for safe Petri nets, in S. Donatelli and P. S. Thiagarajan (Eds), Petri Nets and Other Models of Concurrency, ICATPN 2006, Springer, Berlin, pp. 166–180.
• [17] Feng, Y., Xing, K., Zhou, M., Wang, X. and Liu, H. (2020). Robust deadlock prevention for automated manufacturing systems with unreliable resources by using general Petri nets, IEEE Transactions on Systems, Man, and Cybernetics: Systems 50(10): 3515–3527.
• [18] Finkbeiner, B., Gieseking, M., Hecking-Harbusch, J. and Olderog, E.-R. (2020). AdamMC: A model checker for Petri nets with transits against flow-LTL, in S.K. Lahiri and C. Wang (Eds), Computer Aided Verification, Springer, Cham, pp. 64–76.
• [19] Girault, C. and Valk, R. (2003). Petri Nets for Systems Engineering: A Guide to Modeling, Verification, and Applications, Springer, Berlin.
• [20] Giua, A. and Xie, X. (2005). Control of safe ordinary Petri nets using unfolding, Discrete Event Dynamic Systems 15(4): 349–373.
• [21] Guo, H.,Man, K.L., Ren, Q., Huang, Q., Hahanov, V., Litvinova, E. and Chumachenko, S. (2017). FPGA implementation of VLC communication technology, 31st International Conference on Advanced Information Networking and Applications Workshops (WAINA), Taipei, Taiwan, pp. 586–590.
• [22] Guo, Y., Hu, X., Hu, B., Cheng, J., Zhou, M. and Kwok, R.Y.K. (2018). Mobile cyber physical systems: Current challenges and future networking applications, IEEE Access 6: 12360–12368.
• [23] Hahanov, V., Hussein, M.A.A., Hahanova, A. and Man, K.L. (2016). Cyber physical computing, 2016 IEEE East-West Design Test Symposium (EWDTS), Yerevan, Armenia, pp. 1–8.
• [24] Huang, B., Zhou, M., Wang, C., Abusorrah, A. and Al-Turki, Y. (2021). Deadlock-free supervisor design for robotic manufacturing cells with uncontrollable and unobservable events, IEEE/CAA Journal of Automatica Sinica 8(3): 597–605.
• [25] Huang, D., Deng, Z., Wan, S., Mi, B. and Liu, Y. (2018). Identification and prediction of urban traffic congestion via cyber-physical link optimization, IEEE Access 6: 63268–63278.
• [26] Jasiul, B., Szpyrka, M. and Śliwa, J. (2015). Formal specification of malware models in the form of colored Petri nets, in J.J.J.H. Park et al. (Eds), Computer Science and Its Applications, Springer, Berlin, pp. 475–482.
• [27] Jiang, Z., Li, Z., Wu, N. and Zhou, M. (2018). A Petri net approach to fault diagnosis and restoration for power transmission systems to avoid the output interruption of substations, IEEE Systems Journal 12(3): 2566–2576.
• [28] Kaid, H., Al-Ahmari, A., Li, Z. and Davidrajuh, R. (2020). Automatic supervisory controller for deadlock control in reconfigurable manufacturing systems with dynamic changes, Applied Sciences 10(15): 1–34, Article no. 5270.
• [29] Karatkevich, A. (2007). Dynamic Analysis of Petri Net-Based Discrete Systems, Springer, Berlin.
• [30] Koh, I. and DiCesare, F. (1990). Transformation methods for generalized Petri nets and their applications to flexible manufacturing systems, Rensselaer’s 2nd International Conference on Computer Integrated Manufacturing, Troy, USA, pp. 364–371.
• [31] Lee, E.A. and Seshia, S.A. (2016). Introduction to Embedded Systems: A Cyber-Physical Systems Approach, 2nd Edn, MIT Press, Cambridge.
• [32] Li, B., Khlif-Bouassida, M. and Toguyéni, A. (2018). On-the-fly diagnosability analysis of bounded and unbounded labeled Petri nets using verifier nets, International Journal of Applied Mathematics and Computer Science 28(2): 269–281, DOI: 10.2478/amcs-2018-0019.
• [33] Lizarraga, A., Begovich, O. and Ramírez, A. (2020). Fault diagnosis for a three-wheel omidirectional vehicle: A geometric approach, 17th International Conference on Electrical Engineering, Computing Science and Automatic Control (CCE), Mexico City, USA, pp. 1–6.
• [34] Luo, J., Liu, Z., Wang, S. and Xing, K. (2020). Robust deadlock avoidance policy for automated manufacturing system with multiple unreliable resources, IEEE/CAA Journal of Automatica Sinica 7(3): 812–821.
• [35] Martínez, J. and Silva, M. (1982). A simple and fast algorithm to obtain all invariants of a generalised Petri net, in C. Girault and W. Reisig (Eds), Application and Theory of Petri Nets, Springer, Berlin, pp. 301–310.
• [36] Murata, T. (1989). Petri nets: Properties, analysis and applications, Proceedings of the IEEE 77(4): 541–580.
• [37] Pan, L., Yang, B., Jiang, J. and Zhou, M. (2020). A time Petri Net with relaxed mixed semantics for schedulability analysis of flexible manufacturing systems, IEEE Access 8: 46480–46492.
• [38] Rajkumar, R.R., Lee, I., Sha, L. and Stankovic, J. (2010). Cyber-physical systems: The next computing revolution, 47th Design Automation Conference, DAC’10, Anaheim, USA, p. 731.
• [39] Ramirez-Trevino, A., Ruiz-Beltran, E., Rivera-Rangel, I. and Lopez-Mellado, E. (2007). Online fault diagnosis of discrete event systems: A Petri net-based approach, IEEE Transactions on Automation Science and Engineering 4(1): 31–39.
• [40] Ran, N., Hao, J., He, Z. and Seatzu, C. (2018a). Diagnosability analysis of bounded Petri nets, IEEE 23rd International Conference on Emerging Technologies and Factory Automation (ETFA), Turin, Italy, Vol. 1, pp. 1145–1148.
• [41] Ran, N., Su, H., Giua, A. and Seatzu, C. (2018b). Codiagnosability analysis of bounded Petri nets, IEEE Transactions on Automatic Control 63(4): 1192–1199.
• [42] Ran, N., Su, H. and Wang, S. (2017). An improved approach to test diagnosability of bounded petri nets, IEEE/CAA Journal of Automatica Sinica 4(2): 297–303.
• [43] Shih, C.-S., Chou, J.-J., Reijers, N. and Kuo, T.-W. (2016). Designing CPS/IoT applications for smart buildings and cities, IET Cyber-Physical Systems: Theory Applications 1(1): 3–12.
• [44] Szpyrka, M. and Jasiul, B. (2017). Evaluation of cyber security and modelling of risk propagation with Petri nets, Symmetry 9(3): 32.
• [45] White, A., Karimoddini, A. and Karimadini, M. (2020). Resilient fault diagnosis under imperfect observations-A need for Industry 4.0 era, IEEE/CAA Journal of Automatica Sinica 7(5): 1279–1288.
• [46] Wiśniewski, R. (2017). Prototyping of Concurrent Control Systems Implemented in FPGA Devices, Springer, Cham.
• [47] Wiśniewski, R., Barkalov, A., Titarenko, L. and Halang, W. (2011). Design of microprogrammed controllers to be implemented in FPGAs, International Journal of Applied Mathematics and Computer Science 21(2): 401–412, DOI: 10.2478/v10006-011-0030-1.
• [48] Wiśniewski, R., Bazydło, G., Szcześniak, P. and Wojnakowski, M. (2019a). Petri net-based specification of cyber-physical systems oriented to control direct matrix converters with space vector modulation, IEEE Access 7: 23407–23420.
• [49] Wiśniewski, R., Karatkevich, A., Adamski, M., Costa, A. and Gomes, L. (2018). Prototyping of concurrent control systems with application of Petri nets and comparability graphs, IEEE Transactions on Control Systems Technology 26(2): 575–586.
• [50] Wisniewski, R., Grobelna, I. and Karatkevich, A. (2020). Determinism in cyber-physical systems specified by interpreted Petri nets, Sensors 20(19): 1–22, Article no. 5565.
• [51] Wiśniewski, R., Wiśniewska, M. and Jarnut, M. (2019b). C-exact hypergraphs in concurrency and sequentiality analyses of cyber-physical systems specified by safe Petri nets, IEEE Access 7: 13510–13522.
• [52] Xia, C. and Li, C. (2021). Property preservation of Petri synthesis net based representation for embedded systems, IEEE/CAA Journal of Automatica Sinica 8(4): 905–915.
• [53] Yang, F., Wu, N., Qiao, Y., Zhou, M., Su, R. and Qu, T. (2018). Petri net-based efficient determination of optimal schedules for transport-dominant single-arm multi-cluster tools, IEEE Access 6: 355–365.
• [54] Zaitsev, D.A. (2006). Compositional analysis of Petri nets, Cybernetics and Systems Analysis 42(1): 126–136.
• [55] Zaitsev, D.A. (2016). Sleptsov nets run fast, IEEE Transactions on Systems, Man, and Cybernetics: Systems 46(5): 682–693.
• [56] Zaitsev, D.A., Shmeleva, T.R. and Groote, J.F. (2019). Verification of hypertorus communication grids by infinite Petri nets and process algebra, IEEE/CAA Journal of Automatica Sinica 6(3): 733–742.
• [57] Zhang, Y., Qiu, M., Tsai, C.-W., Hassan, M.M. and Alamri, A. (2017). Health-CPS: Healthcare cyber-physical system assisted by cloud and big data, IEEE Systems Journal 11(1): 88–95.
• [58] Zhou, M. and Wu, N. (2009). System Modeling and Control with Resource-Oriented Petri Nets, 1st Edn, CRC Press, Boca Raton.
• [59] Zhu, Q., Zhou, M., Qiao, Y. and Wu, N. (2018). Petri net modeling and scheduling of a close-down process for time-constrained single-arm cluster tools, IEEE Transactions on Systems, Man, and Cybernetics: Systems 48(3): 389–400.
• [60] Zurawski, R. and Zhou, M. (1994). Petri nets and industrial applications: A tutorial, IEEE Transactions on Industrial Electronics 41(6): 567–583.

Uwagi

Opracowanie rekordu ze środków MNiSW, umowa Nr 461252 w ramach programu "Społeczna odpowiedzialność nauki" - moduł: Popularyzacja nauki i promocja sportu (2021).