JPL Technical Report Server

Logic model checking of time-periodic real-time systems

Show simple item record

dc.contributor.author Florian, Mihai
dc.contributor.author Gamble, Ed
dc.contributor.author Holzmann, Gerard
dc.date.accessioned 2015-03-10T23:33:44Z
dc.date.available 2015-03-10T23:33:44Z
dc.date.issued 2012-06-19
dc.identifier.citation Infotech @ Aerospace 2012, Garden Grove, California, June 19-21, 2012 en_US
dc.identifier.clearanceno 12-2143
dc.identifier.uri http://hdl.handle.net/2014/44963
dc.description.abstract 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. en_US
dc.description.sponsorship NASA/JPL en_US
dc.language.iso en_US en_US
dc.publisher Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2012 en_US
dc.subject software analysis en_US
dc.title Logic model checking of time-periodic real-time systems en_US
dc.type Preprint en_US


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search


Browse

My Account