Logic Model Checking of Time-Periodic Real-Time Systems
Mihai Florian, Ed Gamble, Gerard J. Holzmann · Infotech@Aerospace 2012 · 2012
In this paper we report on the work we performed to extend the logic model checker SPIN with builtin 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. I.