ERA

Download the full-sized PDF of Fex: A Model Checking Framework for Event SequencesDownload the full-sized PDF

Analytics

Share

Permanent link (DOI): https://doi.org/10.7939/R34M91C40

Download

Export to: EndNote  |  Zotero  |  Mendeley

Communities

This file is in the following communities:

Computing Science, Department of

Collections

This file is in the following collections:

Technical Reports (Computing Science)

Fex: A Model Checking Framework for Event Sequences Open Access

Descriptions

Author or creator
Li, Xin
Additional contributors
Subject/Keyword
model checking
Type of item
Computing Science Technical Report
Computing science technical report ID
TR08-14
Language
English
Place
Time
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.
Date created
2008
DOI
doi:10.7939/R34M91C40
License information
Creative Commons Attribution 3.0 Unported
Rights

Citation for previous publication

Source
Link to related item

File Details

Date Uploaded
Date Modified
2014-04-29T21:04:25.933+00:00
Audit Status
Audits have not yet been run on this file.
Characterization
File format: pdf (Portable Document Format)
Mime type: application/pdf
File size: 908388
Last modified: 2015:10:12 16:59:38-06:00
Filename: TR08-14.pdf
Original checksum: cfc13f9bea109e25615fcb106402eb5d
Well formed: true
Valid: true
Status message: File header gives version as 1.4, but catalog dictionary gives version as 1.3
File title: report
File author: Xin Li
Page count: 118
Activity of users you follow
User Activity Date