Developing methods for verifying the discrete-event model elements

Authors: Gorokhova A.S., Zavadskaya L.A., Novichkova M.A.
Published in issue: #4(93)/2024
DOI:
Category: Mathematics | Chapter: Computational Mathematics
Keywords: discrete-event system, finite automata, robot group, Petri nets, reachability tree, behavior specification, logical string sequence structure, verification
Published: 08.10.2024

The paper considers simulation processes in a discrete-event system (DES) to control a group of mobile robots, control object model verification methods, and the DES specification. Since errors could appear in the model construction, further simulation using an incorrectly constructed model could result in additional workload, excessive computation waste and lead to an unacceptable result. The paper proposes an opportunity to improve system quality by applying the DES elements validation, using the Petri net software tools analysis and specification correctness. It presents the DES two-stage verification at the level of constructing the control object model in general and at the level of concrete specification of the system behavior. At the first stage, the simulated system is represented as a Petri net. Through construction and analysis of the reachability tree constrained to a finite size, the network is being checked to meet the security, liveliness, reachability and connectivity properties. At the second step, the system behavior model is checked for correctness in transitions between the events and coherence of the event chain. The paper proposes practical implementation of the verification system realized in the C++ programming language. The results could serve as a basis in developing a system that allows automating the design process for the robot group control systems.

References

[1] Ambartsumyan A.A., Potekhin I.P. Group control in discrete-event systems. Problems of Control, 2012, no. 5, pp. 46–53. (In Russ.).

[2] Kozov A.V., Volosatova T.M., Tachkov A.A. Directions of automation of design of control systems for groups of mobile robots. Fundamental and applied problems of safety, survivability, reliability, stability and efficiency of systems. III Int. scientific-practical. conf., dedicated to the 110th anniversary of the birth of Academician N.A. Pilyugin: collection of works. Yelets, Yelets State University named after I.A. Bunin Publ., 2019, pp. 335–339. (In Russ.).

[3] Vasiliev I.A., Polovko S.A., Smirnova E.Yu. Organization of group control of mobile robots for special robotics tasks. Informatics, Telecommunications and Management, 2013, no. 1 (164), pp. 119–123. (In Russ.).

[4] Ambartsumyan A.A. Supervisory control of structured dynamic discrete-event systems. Avtomat. i Telemekh., 2009, no. 8, pp. 156–176. (In Russ.).

[5] Ambartsumyan A.A. Network-centric control on Petri nets in a structured discrete-event system. UBS, 2010, vol. 30 (1), pp. 506–535. (In Russ.).

[6] Veretelnikova E.L. Theoretical informatics. Theory of Petri nets and modeling of systems: a tutorial. Novosibirsk, NSTU Publishing House, 2018, 82 p. (In Russ.).

[7] Kotov V.E. Petri Nets. Moscow, Nauka. Main Editorial Board of Physical and Mathematical Literature, 1984, 160 p. (In Russ.).

[8] Kozov A.V. Implementation of a Computer Model of a Discrete-Event Group Control System for Mobile Robots. Extreme Robotics, 2022, vol. 1, no. 1, pp. 139–146. (In Russ.).

[9] Ambartsumyan A.A., Aristov V.V. Petri Nets as an Apparatus for Modeling and Synthesizing Supervisory Control of Discrete-Event Systems. Dynamics of Systems, Mechanisms and Machines, 2012, no. 1, pp. 217–220. (In Russ.).