TY - JOUR
T1 - OS-in-the-Loop verification for multi-tasking control software
AU - Choi, Yunja
N1 - Publisher Copyright:
© 2022 John Wiley & Sons Ltd.
PY - 2023/1
Y1 - 2023/1
N2 - 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.
AB - 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.
KW - heterogeneous composition
KW - model checking
KW - multi-tasking
KW - OS-in-the-Loop
UR - http://www.scopus.com/inward/record.url?scp=85143332497&partnerID=8YFLogxK
U2 - 10.1002/stvr.1834
DO - 10.1002/stvr.1834
M3 - Article
AN - SCOPUS:85143332497
SN - 0960-0833
VL - 33
JO - Software Testing Verification and Reliability
JF - Software Testing Verification and Reliability
IS - 1
M1 - e1834
ER -