Monitor Synthesis for Parametric MTL Properties in Discrete Control Software
Hao Shi, Wei Yu Dong, Ge Zhou, Liangze Yin · 2017
With the increasingly application of discrete control software in automatic control field, the security and reliability of its behavior becomes even more essential. However, the traditional verification methods are of high complexity and poor flexibility, so the lightweight Runtime Verification becomes an alternative. In this paper, aiming at real-time properties in discrete control software, an improved runtime verification framework is pro-posed. According to characteristics of real-time properties, we introduce DT-MTL in specifications to describe these properties, and two algorithms of monitor's generation are proposed. Based on the idea of parametric runtime verification, the framework can be used to automate the monitoring of parameterized real-time properties, which are described by DT-MTL. We carried out experiments on the high speed train control system to prove the validity of the framework.