NTRS - NASA Technical Reports Server

Back to Results
Execution-Based Model Checking of Interrupt-Based SystemsExecution-based model checking (EMC) is a verification technique based on executing a multi-threaded/multiprocess program repeatedly in a systematic manner in order to explore the different interleavings of the program. This is in contrast to traditional model checking, where a model of a system is analyzed Several execution-based model-checking tools exist at this point, such as for example Verisoft and Java PathFinder. The most common formal specification languages used by EMC tools are un- timed, either just assertions, or linear-time temporal logic (LTL). An alternative verification technique is Runtime Execution Monitoring (REM), which is based on monitor- ing the execution of a program, checking that the execution trace conforms to a requirement specification. The Temporal Rover and DBRover are such tools. They provide a very rich specification language, being an extension of LTL with real-time constraints and time-series. We show how execution-based model checking, combined with runtime execution monitoring, can be used for the verification of a large class of safety critical systems commonly known as interrupt-based systems. The proposed approach is novel in that: (i) it supports model checking of a large class of applications not practically verifiable using conventional EMC tools, (ii) it supports verification of LTL assertions extended with real-time and time-series constraints, and (iii) it supports the verification of custom schedulers.
Document ID
Document Type
Preprint (Draft being sent to journal)
Drusinsky, Doron (Naval Postgraduate School Monterey, CA, United States)
Havelund, Klaus (Kestrel Technology, LLC Moffett Field, CA, United States)
Date Acquired
August 21, 2013
Publication Date
January 1, 2003
Subject Category
Computer Systems
Distribution Limits
Public Use Permitted.
Document Inquiry