The Library
Model checking, testing and verification working together
Tools
UNSPECIFIED (2005) Model checking, testing and verification working together. In: Automated Verification of Critical Systems Workshop (AVoCS), Southampton, ENGLAND, APR 02, 2003-APR 03, 2004. Published in: FORMAL ASPECTS OF COMPUTING, 17 (2). pp. 201-221. doi:10.1007/s00165-005-0059-8 ISSN 0934-5043.
Research output not available from this repository.
Request-a-Copy directly from author or use local Library Get it For Me service.
Official URL: http://dx.doi.org/10.1007/s00165-005-0059-8
Abstract
We present a symbolic model checking approach that allows verifying a unit of code, e.g., a single procedure or a collection of procedures that interact with each other. We allow temporal specifications that assert over both the program counters and the program variables. We decompose the verification into two parts: (1) a search that is based on the temporal behavior of the program counters, and (2) the formulation and refutation of a path condition, which inherits conditions constraining the program variables from the temporal specification. This verification approach is modular, as we do not require that all the involved procedures are provided. Furthermore, we do not request that the code is based on a finite domain. The presented approach can also be used for automating the generation of test cases for unit testing.
Item Type: | Conference Item (UNSPECIFIED) | ||||
---|---|---|---|---|---|
Subjects: | Q Science > QA Mathematics > QA76 Electronic computers. Computer science. Computer software | ||||
Journal or Publication Title: | FORMAL ASPECTS OF COMPUTING | ||||
Publisher: | SPRINGER | ||||
ISSN: | 0934-5043 | ||||
Official Date: | August 2005 | ||||
Dates: |
|
||||
Volume: | 17 | ||||
Number: | 2 | ||||
Number of Pages: | 21 | ||||
Page Range: | pp. 201-221 | ||||
DOI: | 10.1007/s00165-005-0059-8 | ||||
Publication Status: | Published | ||||
Title of Event: | Automated Verification of Critical Systems Workshop (AVoCS) | ||||
Location of Event: | Southampton, ENGLAND | ||||
Date(s) of Event: | APR 02, 2003-APR 03, 2004 |
Data sourced from Thomson Reuters' Web of Knowledge
Request changes or add full text files to a record
Repository staff actions (login required)
View Item |