以時間邏輯為表示法的模組細步化
Other Title
Modular Refinement in Temporal Logic
Date Issued
2001
Date
2001
Author(s)
DOI
892213E002109
Abstract
When developing a large system, we
typically start with the abstract specifications of
its constituent modules and gradually refine the
abstract modules into concrete,
straightforwardly implementable modules.
Correctness of this modular refinement process
entails proof obligations of the form that the
composition of more concrete modules
implements the composition of more abstract
modules. The verification task can be made
easier if there exist proof rules that offer the
possibility of breaking those proof obligations
down to the module level. In this research, we
investigate the use of linear-time temporal logic,
specifically LTL of Manna and Pnueli, in
facilitating the aforementioned modular
refinement process.
Abadi and Lamport pioneered the work on
modular refinement with temporal logic. They
showed that assumption-guarantee
specifications play a fundamental, thought
implicit, role in modular refinement. We have
subsequently demonstrated the advantage of
LTL over TLA, the temporal logic used by
Abadi and Lamport, in formulating
assumption-guarantee specifications. We set to
again take advantage of the expressive power
of LTL so as to obtain more easily
understandable and usable modular refinement
rules. The main results of this work include a
modular refinement rule for closed systems and
a generalized one for open systems or modules;
both are purely syntactical within LTL.
Subjects
Assumption-Guarantee
Compositional Verification
Concurrent
Systems
Systems
Decomposition
Modular Refinement
Modular Verification
Refinement
Specification
Temporal Logic
Verification
Publisher
臺北市：國立臺灣大學資訊管理學系暨研究所
Type
other
File(s)![Thumbnail Image]()
Loading...
Name
892213E002109.pdf
Size
255.2 KB
Format
Adobe PDF
Checksum
(MD5):ace27f645e3943c017dd3c4bb2c569ff