Execution-Based Model Checking of Interrupt-Based Systems
Loading...
Authors
Drusinsky, Doron
Havelund, Klaus
Subjects
TEMPORAL LOGIC
MATHEMATICAL MODELS
PROGRAM VERIFICATION (COMPUTERS)
COMPUTER SYSTEMS PROGRAMS
OPERATING SYSTEMS (COMPUTERS)
JAVA (PROGRAMMING LANGUAGE)
REAL TIME OPERATION
APPLICATIONS PROGRAMS (COMPUTERS)
RUN TIME (COMPUTERS)
SOFTWARE DEVELOPMENT TOOLS
MATHEMATICAL MODELS
PROGRAM VERIFICATION (COMPUTERS)
COMPUTER SYSTEMS PROGRAMS
OPERATING SYSTEMS (COMPUTERS)
JAVA (PROGRAMMING LANGUAGE)
REAL TIME OPERATION
APPLICATIONS PROGRAMS (COMPUTERS)
RUN TIME (COMPUTERS)
SOFTWARE DEVELOPMENT TOOLS
Advisors
Date of Issue
2003-01
Date
Jan 01, 2003
Publisher
Language
Abstract
Execution-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.
Type
Preprint
Description
International Conference on Dependable Systems and Networks and Networks Workshop on Model Checking
Series/Report No
Department
Organization
Ames Research Center
Identifiers
NPS Report Number
Sponsors
Funder
Format
Citation
Distribution Statement
Approved for public release; distribution is unlimited.
Rights
This publication is a work of the U.S. Government as defined in Title 17, United States Code, Section 101. Copyright protection is not available for this work in the United States.