The stochastic semantics and verification for periodic control systems

MengFei  Yang; Zheng  Wang; GeGuang  Pu; Shengchao Qin; Bin  Gu; Jifeng He

doi:10.1007/s11432-012-4750-0

The stochastic semantics and verification for periodic control systems

MengFei Yang, Zheng Wang, GeGuang Pu, Shengchao Qin, Bin Gu, Jifeng He

Research output: Contribution to journal › Article

Abstract

Periodic control systems (PCS) are widely used in the embedded industry like aerospace and automotive. 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 system 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.

Original language	English
Pages (from-to)	2675-2693
Journal	Science China Information Sciences
Volume	55
Issue number	12
DOIs	https://doi.org/10.1007/s11432-012-4750-0
Publication status	Published - 2012

Access to Document

10.1007/s11432-012-4750-0

Fingerprint Dive into the research topics of 'The stochastic semantics and verification for periodic control systems'. Together they form a unique fingerprint.

Cite this

Yang, M., Wang, Z., Pu, G., Qin, S., Gu, B., & He, J. (2012). The stochastic semantics and verification for periodic control systems. Science China Information Sciences, 55(12), 2675-2693. https://doi.org/10.1007/s11432-012-4750-0

@article{3103fa1692c1404ea57a32df49590482,

title = "The stochastic semantics and verification for periodic control systems",

abstract = "Periodic control systems (PCS) are widely used in the embedded industry like aerospace and automotive. 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 system 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.",

author = "MengFei Yang and Zheng Wang and GeGuang Pu and Shengchao Qin and Bin Gu and Jifeng He",

year = "2012",

doi = "10.1007/s11432-012-4750-0",

language = "English",

volume = "55",

pages = "2675--2693",

journal = "Science China Information Sciences",

issn = "1674-733X",

publisher = "Science in China Press",

number = "12",

}

TY - JOUR

T1 - The stochastic semantics and verification for periodic control systems

AU - Yang, MengFei

AU - Wang, Zheng

AU - Pu, GeGuang

AU - Qin, Shengchao

AU - Gu, Bin

AU - He, Jifeng

PY - 2012

Y1 - 2012

N2 - Periodic control systems (PCS) are widely used in the embedded industry like aerospace and automotive. 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 system 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.

AB - Periodic control systems (PCS) are widely used in the embedded industry like aerospace and automotive. 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 system 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.

U2 - 10.1007/s11432-012-4750-0

DO - 10.1007/s11432-012-4750-0

M3 - Article

VL - 55

SP - 2675

EP - 2693

JO - Science China Information Sciences

JF - Science China Information Sciences

SN - 1674-733X

IS - 12

ER -