元件合成軟體之形式化驗證初探
Other Title
Toward Formal Verification of Component-Based Software
Date Issued
2004
Date
2004
Author(s)
DOI
922213E002061
Abstract
Component-based design has become a
prominent approach to software
development.In this project we
consider the task of formally specifying
and verifying behavioral correctness of
software built from independently
developed components.The task
requires a way for the component designer
to describe his component without
revealing the code,i.e.,to specify what
the component does but not how it gets
things done.It also requires a way for
the component-based software developer
to verify his system,given the source
code of the part that he coded and the
specifications of the components that he
used.
We adapt a compositional framework
that we have developed earlier for
carrying out the aforementioned
specification and verification tasks.
In particular,we demonstrate how the
framework may be used in a typical case
where some components of a system can be
reasoned only with their behavioral
specification but not their code.We
also investigate how the verification
tasks can be facilitated by automated
tools.
Subjects
Assumption-Guarantee
Component-Based Software
Compositional
Verification
Verification
Formal Methods
Model
Checkers
Checkers
Modular Verification
Proof
Assistants
Assistants
Software Components
Specification
Temporal Logic
Verification
Publisher
臺北市：國立臺灣大學資訊管理學系暨研究所
Type
other
File(s)![Thumbnail Image]()
Loading...
Name
922213E002061.pdf
Size
293.08 KB
Format
Adobe PDF
Checksum
(MD5):9d0e380fa15ec6c36910bb96ce14e64f