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 journalArticle

    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 languageEnglish
    Pages (from-to)2675-2693
    JournalScience China Information Sciences
    Volume55
    Issue number12
    DOIs
    Publication statusPublished - 2012

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

  • Cite this