MDM: A Mode Diagram Modeling Framework

Zheng Wang, GeGuang Pu, Jianwen Li, Jifeng He, Shengchao Qin, Kim G. Larsen, Jan Madsen, Bin Gu

    Research output: Contribution to journalConference article

    Abstract

    Periodic control systems used in spacecrafts and automotives are usually period-driven and can be decomposed into different modes with each mode representing a system state observed from outside. Such systems may also involve intensive computing in their modes. Despite the fact that such control systems are widely used in the above-mentioned safety-critical embedded domains, there is lack of domain-specific formal modelling languages for such systems in the relevant industry. To address this problem, we propose a formal visual modeling framework called mode diagram as a concise and precise way to specify and analyze such systems. To capture the temporal properties of periodic control systems, we provide, along with mode diagram, a property specification language based on interval logic for the description of concrete temporal requirements the engineers are concerned with. The statistical model checking technique can then be used to verify the mode diagram models against desired properties. To demonstrate the viability of our approach, we have applied our modelling framework to some real life case studies from industry and helped detect two design defects for some spacecraft control systems.
    Original languageEnglish
    Pages (from-to)135-149
    JournalElectronic Proceedings in Theoretical Computer Science, EPTCS
    Volume105
    DOIs
    Publication statusPublished - 2012
    Event1st International Workshop on Formal Techniques for Safety-Critical Systems
    - Kyoto, Japan
    Duration: 12 Nov 201212 Nov 2012
    Conference number: 1

    Fingerprint Dive into the research topics of 'MDM: A Mode Diagram Modeling Framework'. Together they form a unique fingerprint.

  • Cite this

    Wang, Z., Pu, G., Li, J., He, J., Qin, S., Larsen, K. G., Madsen, J., & Gu, B. (2012). MDM: A Mode Diagram Modeling Framework. Electronic Proceedings in Theoretical Computer Science, EPTCS, 105, 135-149. https://doi.org/10.4204/EPTCS.105.10