Semantic Model And Its Applications Of Parameterized Spatial-temporal Consistency Language

Cyber-Physical Systems is a new trend of real-time systems recently.It combines the computational process with the physical process and is a multidimensional complex system,which realizes the real-time sensing,dynamic control and information service through the technologies of 3C(Computation,Communication,Control).Some agents in Cyber-Physical Systems have the requirements of the spatial-temporal information,leading to the situation where it is difficult for the existing formal methods to model these systems,accurately.So,a location-triggered specification language for real-time systems,denoted as STeC,is proposed and STeC language can model real-time systems,which stress the spatial-temporal consistency.However,STeC does not take the environment into consideration,which is an important factor that affects the actual operation of the agent.Based on the STeC language,this paper proposes a Parameterized SpatialTemporal Consistency Language pSTeC,which adds parameter “environment” and designs operation curves of the agent,meaning that it designs differential equations the agent,describing the velocity and acceleration.When the environment changes,pSTeC can guarantee spatial-temporal consistency of the agent through adjusting operation curves.Firstly,this paper introduces the syntax of pSTeC through adding parameter“environment”.Based on it,the paper builds operational semantics and denotational semantics of pSTeC and proves the equivalence between them.Secondly,this paper uses the driverless car's barking as an example to introduce how to use the pSTeC language.According to the driverless car's barking,the paper uses the pSTeC language to describe the braking process.The paper also builds operational semantics of pSTeC under the different environments and it can guarantees spatial-temporal consistency of the agent through adjusting differential equations,describing the velocity and acceleration.Finally,this paper introduces the simulation tool of spatial-temporal consistency based on the driverless car's barking.After the user selects environment and inputs other parameters,the tool can simulate the operation curve of the driverless car.While the driverless car brakes under other environment,the tool can give a suitable initial speed of braking under the new environment and simulate its operation curve,which guarantees spatial-temporal consistency.This paper also gives some advice about how to brake safely.