Modeling And Property Verification Of Indeterminate CPS

With the constant improvement of the quality of hardware product and the ability of data processing, the rapid development of network communication technique, and the enhancement of the level of the informatization of computer system, people are not only limited to the system function, but rather pay more attention on the reasonable and effective allocation of system resources ? performance and effectiveness optimization of the system, and the improvement of the control and service personalized for the requirement of engineering system and computer equipment. As a new intelligent system, CPS, integrating computing, communication and control, emerges in response to the requirement of times. CPS has been formed a new research field for academic and scientific circles, acquires the concern and attention from the domestic and overseas experts on many fields, such as computer, communicating, biology, traffic and so on.As the formal automatic verification technology, model checking has been wide applied to analyze the correctness of software and hardware design?communication protocol and securing authentication protocol. The uncertainty and inconsistent information unavoidable appears on the verifying processing of concurrent system, besides classical model checking cannot verify the system involving uncertainty information. In the past few years, there were even more applications on probability model checking in verifying properties of systems with uncertain information. However, in the real life, there exists some systems that do not satisfy the additive property of the probability measure, and cannot be verified in the probability system model. Hence, model checking theory based on possibility measure are introduced by professor Li. Yongming, which provides the theoretical foundation for the formal verification of complex system with uncertainty information. Since the indeterminate computer model and theory can actually response the real systems, there is more important meaning in applications.This paper mainly researches the indeterminate CPS model and presents the method of property verification. Under the condition of the impaction of the dynamic verification, on the uncertainty environment, the possibility measure on the CPS software system is introduced; the methods of indeterminate CPS model and property verification are given. Additionally, the possibility mixture automaton as the model of software operation is presented; the systematic dynamic model of possibility CPS software is defined. Meanwhile, a method to solve the possibility dynamic verification of CPS software model is discussed in detail. In particular, some qualitative properties of repeated reach-ability and persistence are verified. Finally, we prove the effectivity of the method from the theoretical proof and case study.