The stochastic semantics and verification for periodic control systems

• Published in: Science China. Information sciences 2012-12, Vol.55 (12), p.2675-2693
• Main Authors: Yang, MengFei, Wang, Zheng, Pu, GeGuang, Qin, ShengChao, Gu, Bin, He, JiFeng
• Format: Article
• Language: English
• Subjects: Aerospace industry; Computer Science; Control systems; Information Systems and Communication Service; Markov chains; MDM; Research Paper; Semantics; Specification and description languages; Statistical analysis; Statistical models; Temporal logic; 区间时序逻辑; 周期性任务; 控制系统; 语义; 随机; 马尔可夫链; 验证系统
• ISSN: 1674-733X; 1869-1919
• DOI: 10.1007/s11432-012-4750-0

Periodic control systems （PCS） are widely used in the embedded industry like aerospace and au- tomotive. Such systems usually run periodic tasks and respond to the external signals. Based on our previous work on Mode diagram modeling （MDM） notations for specifying the periodic control system, we present the stochastic semantics for MDM in this paper. The stochastic semantics of MDM is based on the Markov chain. The semantics proposed here provides the basis for the satisfaction of formulae of the interval temporal logic （ITL） based specification language that is aimed to specify the properties of PCS. To verify whether the sys- tem satisfies the ITL-based properties, we apply the statistical model checking technique to efficiently estimate the probability of the system satisfying the given property with a desired level of confidence. The empirical experiments show that our approach is both effective and efficient.