Font Size: a A A

Model Checking Of Cyber Physical System Based On Co-simulation And Statistical Model Checking

Posted on:2019-04-18Degree:MasterType:Thesis
Country:ChinaCandidate:K Q JiangFull Text:PDF
GTID:2428330566460754Subject:Software engineering
Abstract/Summary:PDF Full Text Request
Cyber Physical System(CPS)is a complex system with features such as heterogeneity and uncertainty.Therefore,the simulation,verification and analysis of the system face enormous challenges.To solve this problem,this paper proposes a verification method based on co-simulation and Statistical Model Checking(SMC).This method can use SMC technique to verify and analyse the traces generated by co-simulation,and provides an effective method for quantitatively evaluating heterogeneous CPS.It mainly includes three phases.Firstly,the system architecture is modeled by System Modeling Language(SysML).Secondly,the co-simulation model is built based on the Functional Mock-up Interface(FMI)standard,and the co-simulation process of the model is performed.Finally,the traces obtained by co-simulation are evaluated using SMC technique.The main contributions of this paper include:Based on timed automata,the correctness of coordination behavior between heterogeneous components of the system is verified.Firstly,mapping rules from Functional Mock-up Unit(FMU)to timed automata is proposed.Secondly,based on timed automata,the simulation model and the master algorithm of co-simulation are formalized.Finally,the UPPAAL verification tool is used to verify the deadlock and reachability of the formal models.Through this method,the correctness of the co-simulation process is verified.In addition,we also use the water tank case to demonstrate the effectiveness of the method.A distributed SMC algorithm based on abstraction and learning is proposed to improve the efficiency of SMC,and the design and implementation of the algorithm are presented.There are two main factors that directly affect the efficiency of the SMC algorithm: the speed at which the simulator generates a single trace and the number of traces generated during the verification process.For these two factors,we use distributed technology to increase the speed of producing a single simulation trace,and use abstraction and learning methods to reduce the number of simulation traces generated during the verification process,thereby effectively improving the efficiency of SMC.Finally,we design and develop the statistical model checking tool(Co-SMC)based on co-simulation.This tool implements the FMI-based co-simulation and the improved SMC algorithm proposed in this paper.With this tool,we analyzed two cases: energy aware building system and robot path planning system.Through the verification and analysis of these two cases,we find that the verification method proposed in this paper is effective,and the improved SMC algorithm is accurate and efficient.
Keywords/Search Tags:Cyber physical system, Co-simulation, Statistical model checking, Functional Mock-up Interface, Distributed technology, Timed automata
PDF Full Text Request
Related items