Modeling and Verification Methods for Spatio-Temporal Consistency of CPS in Uncertain Environments

When cyber-physical systems (CPSs) are operational, its computing units frequently interact with complex and uncertain physical environments in time and space. To ensure the safety of the system, it is often necessary that the physical entities and information systems of CPS operate in a consistent manner at the temporal and spatial levels. However, most of the existing studies on spatio-temporal consistency modeling and verification of CPS are limited in the ability to deal with uncertainties. To address this issues, in this article, we propose a modeling and verification method for spatio-temporal consistency of CPS in uncertain environments. First, we propose a modeling language (stochastic spatio-temporal modeling language, SSTL) for the spatio-temporal domain of CPS. It can explicitly model the spatio-temporal constraints of CPS as well as deal with the spatio-temporal behavior of accompanying probabilities. Second, we propose a framework for spatio-temporal consistency verification. In the first step of this framework, we propose a worst-case time satisfiability algorithm to verifying the time safety of CPS. In the second step, we develop a prototype tool called "SSTL2NSHA" that is able to convert SSTL into the NHSA model supported by UPPAAL-statistical model checking (UPPAAL-SMC). Thereby the CPS model described by SSTL can be verified in UPPAAL-SMC for spatial safety constraints. Finally, we illustrate the effectiveness of the approach in this article with a traffic alert and collision avoidance system.