Automation of Modular Verification Using the Assumption-Guarantee Approach
Date Issued
2004
Date
2004
Author(s)
Tsai, Ming-Heisn
DOI
en-US
Abstract
Correctness of a component-based software design induces the need
of modular verification. As one component of a design may not know
the implementation details of others, assumption-guarantee
reasoning serves as a good framework for such verification tasks.
In this thesis, we investigate the automation of modular
verification, achieved by converting such problems to model
checking problems, using assumption-guarantee specifications
written in quantified propositional temporal logic (QPTL). Though
QPTL is very expressive, the complexity of checking the validity
of a QPTL formula is extremely high, which is mainly caused by the
existence of quantifications over program variables. Besides,
modern model checkers for temporal logic do not support such
quantifications. We show how these quantifications can be
eliminated so that model checkers can be used to automate the
modular verification tasks. Two small examples are constructed for
illustration of the approach.
Subjects
時態邏輯
模組化驗證
複雜度
假設保證
驗證
verification
composition
assumption-guarantee
model checking
temporal logic
Type
other
File(s)![Thumbnail Image]()
Loading...
Name
ntu-93-R91725014-1.pdf
Size
23.31 KB
Format
Adobe PDF
Checksum
(MD5):c05e0fa1b0792414dd0ea2e1c7c31965