Show simple item record

dc.contributor.authorDrusinsky, Doron
dc.contributor.authorHavelund, Klaus
dc.dateJan 01, 2003en_US
dc.date.accessioned2018-09-27T00:06:26Z
dc.date.available2018-09-27T00:06:26Z
dc.date.issued2003-01
dc.identifier.other20040010841
dc.identifier.urihttp://hdl.handle.net/10945/60082
dc.identifier.urihttps://ntrs.nasa.gov/search.jsp?R=20040010841
dc.descriptionInternational Conference on Dependable Systems and Networks and Networks Workshop on Model Checkingen_US
dc.descriptionApproved for public release, distribution unlimiteden_US
dc.description.abstractExecution-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.en_US
dc.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.en_US
dc.titleExecution-Based Model Checking of Interrupt-Based Systemsen_US
dc.typePreprint
dc.contributor.corporateAmes Research Center
dc.subject.authorTEMPORAL LOGICen_US
dc.subject.authorMATHEMATICAL MODELSen_US
dc.subject.authorPROGRAM VERIFICATION (COMPUTERS)en_US
dc.subject.authorCOMPUTER SYSTEMS PROGRAMSen_US
dc.subject.authorOPERATING SYSTEMS (COMPUTERS)en_US
dc.subject.authorJAVA (PROGRAMMING LANGUAGE)en_US
dc.subject.authorREAL TIME OPERATIONen_US
dc.subject.authorAPPLICATIONS PROGRAMS (COMPUTERS)en_US
dc.subject.authorRUN TIME (COMPUTERS)en_US
dc.subject.authorSOFTWARE DEVELOPMENT TOOLSen_US


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record