CPS-Oriented Hybrid Process Calculus Modeling And Statistical-Based Performance Evaluation

Cyber-physical Systems is a new generation of intelligent systems in which software and hardware devices are closely related to each other.With the development of automation technology,communication technology and computer technology,CPS has gradually matured and is increasingly used in actual production and life.At the same time,people's requirements for CPS are no longer limited to the function expansion of the system,and the performance indicators of CPS are beginning to be taken seriously.Under the premise of ensuring safety and reliability,people tend to adopt systems with better performance.At present,there are few researches on the formal methods related to CPS performance evaluation.After the collation and research on CPS features and performance indicators,this paper proposes to introduce formal modeling and analysis methods into the performance evaluation of CPS.Using the statistical model detection and performance evaluation semantic CTSL to obtain performance parameters for the HPCCS-based CPS model.The innovation points of this paper are as follows:(1)As a formal modeling method,process calculus can describe the synchronization relationship between processes.This paper uses process calculus to model CPS,expands probability selection and differential equations based on process TCCS,and proposes a new CPS modeling language HPCCS.AADL is a commonly used system modeling language.AADL can be used to develop large component systems,such as avionics systems and train control systems.This paper extends AADL random behavior and hybrid behavior,and proposes Hybrid-AADL for CPS modeling.However,AADL is a semi-formal modeling language that cannot directly used to model checking.This paper proposes a conversion algorithm from Hybrid-AADL to HPCCS,and indirectly checks the Hybrid-AADL model by checking the converted HPCCS model.(2)The performance evaluation of CPS requires a performance evaluation language with sufficient expressive power and no ambiguity.This paper proposes a performance evaluation language CTSL(Continuous Time Stochastic Language)based on PLTL and CTL.Through the CTSL based on the real-valued state formula,we can express the real-valued properties that traditional sequential logic cannot describe,and can describe the performance of the system.The example shows that the performance index of the system can be described by CTSL formula.(3)In order to calculate the CTSL formula for a given HPCCS model,the HPCCS process discretization algorithm is first discretized,and then the exact solution of the CTSL formula is calculated by path traversal of the discretized model.Since HPCCS can be combined by multiple processes concurrently,the exact solution method will soon face the problem of state space explosion as the combined process increases.Therefore,the Bayesian statistical model detection algorithm is used to classify CTSL into four types of formulas,and Bayesian statistical detection algorithms are given according to the properties of the four types of formulas.The efficiency of the CTSL formula calculation is improved by the extended Bayesian statistical model detection.Statistical model detection analysis can provide counter-information information for developers to analyze system performance bottlenecks.