In this paper we report on the work we performed to extend the logic model checker SPIN with built-in support for the verification of periodic, real-time embedded software systems, as commonly used in aircraft, automobiles, and spacecraft. We first extended the SPIN verification algorithms to model priority based scheduling policies. Next, we added a library to support the modeling of periodic tasks. This library was used in a recent application of the SPIN model checker to verify the engine control software of an automobile, to study the feasibility of software triggers for unintended acceleration events.
Logic Model Checking of Time-Periodic Real-Time Systems
AIAA Infotech @ Aerospace 2012 Conference ; 2012 ; Garden Grove, CA, United States
2012-06-19
Conference paper
No indication
English
Logic Model Checking of Time-Periodic Real-Time Systems
AIAA | 2012
|2012-2607 Logic Model Checking of Time-Periodic Real-Time Systems
British Library Conference Proceedings | 2012
|Analysis of real-time code by model checking
IEEE | 2000
|