Modeling,Simulation And Verification Research On Dynamic Behaviors Of CPS Based On Model-Driven

Cyber-Physical Systems(CPS)integrate discrete computational processes and continuous physical environment.The computational process monitors and controls the physical environment,which in turn affects the computation.Since the heterogeneous nature of CPS makes its dynamic behaviors very complicated,designing and analyzing CPS faces enormous challenges.On the one hand,the behaviors of computational parts are discrete and the evolution of the physical environment is continuous,so CPS are always hybrid.On the other hand,the open physical environment and the uncertainty of user behaviors result in unavoidable stochastic behaviors of CPS.In addition,CPS are often used in security-critical systems,and the dynamic behaviors of CPS must be ensured to be secure and trustworthy.Therefore,the modeling,simulation and verification of dynamic behaviors of CPS is necessary,but related work is still in the preliminary research stage.In this paper,we propose the modeling,simulation and verification approach of dynamic behaviors of CPS in a model-driven way.Focusing on the dynamic behaviors of CPS,a domain-specific modeling language named SHML(Stochastic Hybrid Modeling Language)is proposed to create dynamic behavioral models of CPS.This paper discusses the abstract syntax,concrete syntax and operational semantics of SHML,and implements the DSML based on GEMOC.Then,system designers can create conforming SHML models in the GEMOC modeling workbench.In order to support the simulation of SHML models,we support users to use the existing GEMOC execution engine and the newly integrated Scilab plug-in to simulate the SHML model.The newly integrated Scilab plug-in can support the simulation of continuous parts of SHML models,breaking the limitations of GEMOC Studio that currently can only support discrete semantic simulation.In order to support the verification of SHML models,we extract and define the UPPAAL metamodel and present the mapping rules from the SHML metamodel to the UPPAAL metamodel.Then the SHML model can be converted to the corresponding UPPAAL model according to well-designed mapping rules encoded in an automatic transformation engine,aiming at supporting the verification of SHML models.Finally,in order to prove the feasibility of the method of modeling,simulation and verification of dynamic behaviors of CPS based on model-driven,which is proposed in this paper,a temperature control system and a line recommendation system are used to illustrate the processes of system modeling,simulation,and verification.