ST-LUSTRE: A novel spatio-Temporal language towards safety-critical cyber-physical systems

Safety-Critical Cyber-Physical Systems (SCCPSs) are a special kind of Cyber-Physical Systems (CPSs) which highlight the importance of system correctness and safety. To apply automatic testing or model checking technique in CPSs, a model that fully captures the features is required to serve as input. So, a novel efficient spatio-Temporal language and the analysis techniques are demanded to support both temporal and spatial expression and reasoning. In fact, a synchronous language, LUSTRE, is widely used in safety-critical systems development. However, LUSTRE lacks spatial constructors. Thus, it is difficult to express the behaviors related to spatial features in SCCPSs. In this paper, we propose a language named ST-LUSTRE to support the unified modeling of spatial and temporal properties of CPSs. We define the syntax and semantics of ST-LUSTRE. Its semantics is interpreted on the topological space and natural number which is based on time sets. We also specify typical SCCPSs properties in ST-LUSTRE. ST-LUSTRE is successfully applied to a communication based train control system of Shanghai Fuxin Intelligent Transportation Solutions CO.,Ltd. (FITSCO).