OS-in-the-Loop verification for multi-tasking control software

Research output: Contribution to journalArticlepeer-review

Abstract

Embedded control software that controls safety-critical IoT devices requires systematic and comprehensive verification to ensure safe operation of the device. However, rigorous verification in this domain has not been feasible due to the high complexity of embedded control software, which is characterized by the frequent use of multi-tasking, interrupts, and periodic alarms. Realizing that two major factors, scalability and exactness, are extremely difficult to achieve at the same time but critical for effective and efficient verification in this domain, this work introduces a domain-specific compositional OS-in-the-Loop (OiL) verification approach and sets out to push the boundary in achieving both factors. The suggested approach (1) models the behavior of the underlying operating system to limit the search space using the notion of controlled concurrency, (2) performs heterogeneous composition of controllers with the formal OS model to reduce verification complexity, and (3) utilizes state-of-the-art verification techniques for the purpose of comprehensive verification up to a given search depth.

Original languageEnglish
Article numbere1834
JournalSoftware Testing Verification and Reliability
Volume33
Issue number1
DOIs
StatePublished - Jan 2023

Keywords

  • heterogeneous composition
  • model checking
  • multi-tasking
  • OS-in-the-Loop

Fingerprint

Dive into the research topics of 'OS-in-the-Loop verification for multi-tasking control software'. Together they form a unique fingerprint.

Cite this