Fex: A Model Checking Framework for Event Sequences
Loading...
Date
Author(s)
Citation for Previous Publication
Link to Related Item
Abstract
Description
Technical report TR08-14. In this report, we present a model checking based verification framework, called Fex, for verifying event sequence related program properties. First, the program under investigation is instrumented such that all potential exceptions can be easily raised. Then the program is sliced to retain only control flow and the event sequence related program constructs. Program properties are presented as executable specification and are fed into JPF model checker along with the sliced program to search for any possible property violations. In order to show the effectiveness of the Fex tool, several field studies namely Exception reliability verification, API conformance verification and Java access rights verification are conducted. The limitation and the future improvement of the Fex tool are also discussed. | TRID-ID TR08-14
Item Type
http://purl.org/coar/resource_type/c_93fc
Alternative
Other License Text / Link
Subject/Keywords
Language
en