- 158 views
- 147 downloads
Fex: A Model Checking Framework for Event Sequences
-
- Author(s) / Creator(s)
-
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
-
- Date created
- 2008
-
- Subjects / Keywords
-
- Type of Item
- Report
-
- License
- Attribution 3.0 International