Formal Modeling,Verification And Analysis For Cyber Physical Systems Software

Cyber Physical Systems as the commanding height of information technology in the world today has been widely used in power systems,medical equipment,aerospace and other safety critical areas.Because CPS is a new kind of networked embedded systems that combine calculation process and physical environment,so it contains various and numerous embedded software which interact with each other by network,therefore,how to guarantee the trustworthiness of software and their interaction has become one of the hotspots in CPS research area.The trustworthiness guarantee of software involves many aspects of software development process.This paper intends to study the formal modeling methods,verification methods and analysis technologies applicable to CPS software in the software design stage,and solve the following four aspects of CPS software trustworthiness guarantee problem:To solve the problem of function and real-time property verification of CPS software,a software formal modeling method based on Time State Transition Matrix(TSTM)is proposed.TSTM introduces the clock function and the time constraint to make it suitable for modeling the behavior of real-time CPS software on the basis of keeping the original formal semantics of State Transition Matrix.On this basis,a TSTM model checking method based on Time Computing Tree Logic(TCTL)is proposed.In order to effectively alleviate the state space explosion,the method adopts Bounded Model Checking(BMC)technology.The experiments show that the method proposed in this paper can achieve good performance,which realizes the integrated modeling and verification of the logic function and time property in the software design stage.To meet the requirement of energy consumption prediction and analysis of CPS software,a formal software modeling method of green software based on Energy Consumption Time State Transition Matrix(ETSTM)is proposed.On the basis of TSTM.ETSTM introduces the energy consumption forecasting function based on the characteristic of software structure,which can be fitting by Back-Propagation(BP)neural network.Furthermore,the multi-scale analysis algorithms of energy consumption for CPS software based on explicit path search and BMC are provided.The experiments show that the proposed method is efficient,which can realize the pre-evaluation of energy consumption for CPS software in the software design stage and avoid the re-design of software due to the energy consumption and other green indicators do not meet the design constraints.To address the demand of dynamic performance evaluation of CPS software,a behavior model for CPS software based on Extended Deterministic and Stochastic Petri Nets(EDSPN)is proposed.By adding non-deterministic time semantics to the deterministic and stochastic Petri net model,EDSPN can represent the uncertain execution time of low-priority program caused by interrupt nesting,then effectively model the behavior of CPS software under interrupt-driven.In addition,an analysis method for EDSPN model based on Markov Regenerative Theory(MRT)is proposed,which includes the preemption strategy of transition,the selection method of the regeneration point,the calculation method of upper-bound execution time of the non-deterministic time transition and solution method of steady state probability.Finally,the performance of CPS software under multi-priority interrupt preemption is analyzed by the experiments.The influence of the interrupt firing frequency,the interrupt execution time and the number of interrupt priority on the performance of CPS software is discussed.To figure out the issue of the non-deterministic behavior analysis of CPS software,a formal definition of Labeled Markov Regenerative Processes(LMRGP)is proposed.On the basis of LMRGP,a probabilistic model checking method of Continuous Stochastic Logic(CSL)based on BMC strategy is proposed.Finally,by analyzing the CPS software model with multi-level interrupt,the non-deterministic behaviors of CPS software are quantitatively analyzed,and the solving ability of BMC method and non-BMC method is compared in the experiment to verify the effectiveness of the proposed method.