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

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

1 Citation (Scopus)
39 Downloads (Pure)

Abstract

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)
PublisherIEEE
Pages312-319
Number of pages8
ISBN (Electronic)978-1-5386-7377-5
ISBN (Print)978-1-5386-7378-2
DOIs
Publication statusPublished - 2018
Event21st Euromicro Conference on Digital System Design 2018 - Prague, Czech Republic
Duration: 29 Aug 201831 Aug 2018
Conference number: 21
http://dsd-seaa2018.fit.cvut.cz/dsd/

Conference

Conference21st Euromicro Conference on Digital System Design 2018
Abbreviated titleDSD 2018
CountryCzech Republic
CityPrague
Period29/08/1831/08/18
Internet address

Fingerprint

Model checking
Model Checking
Stability Analysis
Workload Characterization
Control System
Execution Time
Sampling
Control systems
Analog-to-digital Converter
Digital to analog conversion
Analogue
Digital Control
Asymptotic stability
Multiprocessor
Trigger
Asymptotic Analysis
Asymptotic Stability
Cache
Closed-loop
Completion

Keywords

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

Cite this

El Hakim, Viktorio Semir ; Bekooij, Marco Jan Gerrit. / Stability Verification of Self-Timed Control Systems using Model-Checking. 2018 21st Euromicro Conference on Digital System Design (DSD) . IEEE, 2018. pp. 312-319
@inproceedings{2c9e3c7701e048f9a778021be5dffa99,
title = "Stability Verification of Self-Timed Control Systems using Model-Checking",
abstract = "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.",
keywords = "Hybrid Automata, Cyber-Physical Systems, Control Systems, Stability analysis, Model Checking",
author = "{El Hakim}, {Viktorio Semir} and Bekooij, {Marco Jan Gerrit}",
year = "2018",
doi = "10.1109/DSD.2018.00062",
language = "English",
isbn = "978-1-5386-7378-2",
pages = "312--319",
booktitle = "2018 21st Euromicro Conference on Digital System Design (DSD)",
publisher = "IEEE",
address = "United States",

}

El Hakim, VS & Bekooij, MJG 2018, Stability Verification of Self-Timed Control Systems using Model-Checking. in 2018 21st Euromicro Conference on Digital System Design (DSD) . IEEE, pp. 312-319, 21st Euromicro Conference on Digital System Design 2018, Prague, Czech Republic, 29/08/18. https://doi.org/10.1109/DSD.2018.00062

Stability Verification of Self-Timed Control Systems using Model-Checking. / El Hakim, Viktorio Semir; Bekooij, Marco Jan Gerrit.

2018 21st Euromicro Conference on Digital System Design (DSD) . IEEE, 2018. p. 312-319.

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

TY - GEN

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

AU - El Hakim, Viktorio Semir

AU - Bekooij, Marco Jan Gerrit

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Hybrid Automata

KW - Cyber-Physical Systems

KW - Control Systems

KW - Stability analysis

KW - Model Checking

U2 - 10.1109/DSD.2018.00062

DO - 10.1109/DSD.2018.00062

M3 - Conference contribution

SN - 978-1-5386-7378-2

SP - 312

EP - 319

BT - 2018 21st Euromicro Conference on Digital System Design (DSD)

PB - IEEE

ER -

El Hakim VS, Bekooij MJG. Stability Verification of Self-Timed Control Systems using Model-Checking. In 2018 21st Euromicro Conference on Digital System Design (DSD) . IEEE. 2018. p. 312-319 https://doi.org/10.1109/DSD.2018.00062