Execution-Based Model Checking of Interrupt-Based Systems
MetadataShow full item record
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.
International Conference on Dependable Systems and Networks and Networks Workshop on Model Checking
RightsThis 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.
Showing items related by title, author, creator and subject.
Galinski, Jonathan J. (Monterey, California: Naval Postgraduate School, 2015-09);This thesis provides natural language requirements and associated formal specifications for an electric power grid. These specifications are the first step in using bounded constraint solving to detect early bleak states ...
Michael, James Bret; Shing, Man-Tak (Monterey, California. Naval Postgraduate School, 2007-09); NPS-CS-07-010This paper presents a framework to incorporate computer-based validation techniques to the independent validation and verification (IV&V) of software systems. The framework allows the IV&V team to capture its own understanding ...
Drusinsky, Doron; Shin, Man-Tak; Michael, James Bret (2008);This paper presents a framework for augmenting independent validation and verification (IV & V) of software systems with computer-based IV & V techniques. The framework allows an IV & V team to capture its own understanding of ...