NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Logic Model Checking of Time-Periodic Real-Time SystemsIn 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.
Document ID
20150008744
Document Type
Conference Paper
External Source(s)
Authors
Florian, Mihai (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Gamble, Ed (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Holzmann, Gerard (Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
May 26, 2015
Publication Date
June 19, 2012
Subject Category
Systems Analysis and Operations Research
Meeting Information
AIAA Infotech @ Aerospace 2012 Conference(Garden Grove, CA)
Distribution Limits
Public
Copyright
Other
Keywords
software analysis