OS‐in‐the‐Loop verification for multi‐tasking control software. (17th November 2022)

• Record Type: Journal Article
• Authors: Choi, Yunja
• Is Part Of: Software testing, verification & reliability. Volume 33:Number 1(2023)
• Page Start: n/a
• Page End: n/a
• Publication Date: 2022-11-17
• Subjects: heterogeneous composition -- model checking -- multi‐tasking -- OS‐in‐the‐Loop; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1834
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: 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. Abstract : OiL verification improves the exactness and scalability of rigorous verification by performing heterogeneous composition of controllers with the formal OS model and by limiting the search spaces using the notion of controlled concurrency. A set of case studies show that the approach reduces false alarm ratio from 100% to 5.26% and is able to reason about real‐scale complex multi‐tasking embedded software, which has been impossible with existing approaches.