SELus: Towards Spatio-Temporal Modeling and Quantitative Evaluation for Cyber-Physical Systems

Synchronous language is routinely used to model safety-critical control systems. In recent years, it is gradually being applied to cyber-physical systems (CPS) which emphasise high levels of correctness and safety. It is based on the assumption that the system reacts instantaneously to input events and can compute the output before the next input event, so it is well suited for expressing temporal logic. However, it lacks effective constructs for expressing spatial properties in CPS. Moreover, spatio-temporal properties in CPS are indispensable, requiring not only qualitative analysis but also quantitative analysis. Therefore, we propose SELus, a new synchronous language based on Lustre, to provide the capability of modeling spatio-temporal properties in CPS, enabling the representation of spatial topological relationships and the performance of quantitative analysis on them. To formally verify the SELus model, we introduce a set of mapping rules to transform the SELus model into the Ptolemy II model. The resulting Ptolemy II model is used in Ptolemy II to perform quantitative analysis of the SELus model. Experiments are conducted on lane changing system, showcasing the usability and effectiveness of our language.