Abstract
As the application of intelligent unmanned systems in open environments becomes increasingly widespread, temporal consistency in the system's dynamic evolution process has become a critical issue for determining whether the system is safe and reliable. To address this issue, this paper proposes a model checking-based method for verifying the temporal consistency of software evolution in intelligent unmanned systems, accurately modeling and verifying the temporal behavior of individual agents and multi-agent evolution in the system. First, a temporal consistency constraint verification framework for the evolution of intelligent unmanned systems is presented, under which a global time automaton network model is constructed. The framework defines global and local clock variables, enabling a unified representation of both the overall system process and the time properties of individual agents. Secondly, the temporal consistency constraint patterns under the three evolution operations-addition, deletion, and replacement-are described. Based on this, a temporal consistency verification algorithm is designed, covering dynamic operations such as the addition, deletion, and replacement of agents. The algorithm performs temporal consistency checks for each state through a marking function and depth-first search, ensuring the system's temporal consistency. Finally, a case study on verifying the temporal consistency of an intelligent autonomous vehicle system is presented. Through a series of operations such as the addition, deletion, and replacement of agents, the effectiveness and applicability of the proposed method are verified. The results show that the method can effectively detect temporal inconsistencies in the evolution process, improving the reliability of system evolution in open environments.