Research On Perturbed Signal Temporal Logic PertSTL And Its Online Monitoring Method

Cyber-Physical Systems(CPS)is widely used in safety-critical fields such as smart transportation and smart buildings,and its safety is of utmost importance.How to verify the safety properties of CPS is one of the challenging issues to ensure its safety.Signal Temporal Logic(STL)is widely used to specify the real-valued and continuous-time properties of CPS,but it cannot express signal perturbations because of only considering the changes in signal time-domain.Signal perturbations caused by unforeseen stochastic factors will affect the safety of CPS and even change the satisfaction of STL properties.Therefore,to analyze the safety issues of CPS affected by perturbations,it is of great significance to extend STL to support specify signal perturbations and propose corresponding verification methods.Online monitoring method(also known as runtime verification)is an effective method to verify STL properties,but there are still many challenges in how to propose an efficient online monitoring method for the extended STL specification language.In response to the above problems,this paper aims at the impact of perturbations on the safety of CPS,from a logic-oriented perspective,expands STL to Perturbed Signal Temporal Logic(PertSTL)with a perturbation range,and proposes online PertSTL based on Simulink Monitoring methods to help analyze the worst impact of signal perturbations within a certain range on the verification results.The main work includes:?Perturbed Signal Temporal Logic PertSTL and the calculation method of the worst perturbation value of the signal are proposed.This paper proposes the syntax,Boolean semantics,and quantitative semantics of PertSTL and seeks the perturbation that causes the worst impact within the range of perturbation threshold,that is,the worst perturbation.To analyze the worst perturbation,this paper classifies signal into three types according to formula structure and proposes two algorithms to calculate the worst perturbation.?Aiming at the verification problem of PertSTL properties,this paper proposes a method to implement PertSTL online monitor based on Simulink to analyze the impact of perturbation on the verification results.For the two semantics,combined with the worst perturbation value,three types of mapping rules of PertSTL atomic predicates,Boolean operators,and temporal operators to Simulink blocks are given.Based on three types of mapping rules,a PertSTL online monitor construction method is proposed,which mainly includes:constructing a parse tree of PertSTL;the elements of parse tree correspond to the Simulink blocks,an online monitor is constructed sequentially from bottom to top.?The tool SOMPS(Simulink Online Monitor of PertSTL)is designed and implemented.According to the input PertSTL formula,SOMPS can automatically generate the Simulink-based PertSTL online monitor,which provides tool support.This tool supports the construction of two types of online monitors:Boolean online monitors and quantitative online monitors,which correspond to PertSTL's Boolean semantic model and quantitative semantic model respectively.?The verification results of PertSTL properties are analyzed and the scalability of three online monitors is compared.Through two cases of automobile automatic transmission system and building automatic temperature control system,the effectiveness and practicality of constructing an online monitor to analyze the impact of perturbation on system safety based on PertSTL properties are demonstrated.In addition,this paper analyzes the scalability of the three online monitors by changing the number of rooms in the temperature control system and proves the scalability of the online monitor based on Simulink.