Stability Verification of Self-Timed Control Systems using Model-Checking

Viktorio Semir El Hakim, Marco Jan Gerrit Bekooij

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    3 Citations (Scopus)
    149 Downloads (Pure)


    Cyber-physical control systems are typically time-triggered because the Analog to Digital (A/D) and Digital to Analog (D/A) converters are triggered by a periodic clock. This enables analytical stability analysis of closed-loop models in case the plant and controller are linear. However ensuring periodic sampling requires that a sampling period is selected larger than the Worst-Case Execution Times (WCETs) of the digital control tasks. Unfortunately, low sampling rates must be selected as a result of loose WCET bounds especially if multi-processor hardware is applied with shared data caches and SDRAM memory. In this paper we propose a model-checking based stability analysis approach for control systems that sample aperiodically. Our approach is targetting self-timed systems, where the A/D and D/A converters are driven by internal events, such as the completion of a task, which also trigger subsequent task executions. During self-timed execution the average sampling period tends to be significantly smaller than possible in time-triggered mode, and as a result the control performance is improved significantly. Self-timed systems also allow the use of a running average workload characterization of the tasks which is tighter than a WCET characterization, and which can greatly improve the accuracy of the stability analysis results. We show using two self-timed control systems that control performance in terms of stability and settling time improves for self-timed systems when the running average workload characterization is applied. Furthermore, we point at an essential feature that is needed for asymptotic stability analysis which is missing in well known model checkers such as SpaceEx.
    Original languageEnglish
    Title of host publication2018 21st Euromicro Conference on Digital System Design (DSD)
    EditorsMartin Novotný, Nikos Konofaos, Amund Skavhaug
    Number of pages8
    ISBN (Electronic)978-1-5386-7377-5
    ISBN (Print)978-1-5386-7378-2
    Publication statusPublished - 2018
    Event21st Euromicro Conference on Digital System Design, DSD 2018 - Prague, Czech Republic
    Duration: 29 Aug 201831 Aug 2018
    Conference number: 21


    Conference21st Euromicro Conference on Digital System Design, DSD 2018
    Abbreviated titleDSD
    Country/TerritoryCzech Republic
    Internet address


    • Hybrid Automata
    • Cyber-Physical Systems
    • Control Systems
    • Stability analysis
    • Model Checking


    Dive into the research topics of 'Stability Verification of Self-Timed Control Systems using Model-Checking'. Together they form a unique fingerprint.

    Cite this