<BODY BGCOLOR="#FFFFFF" TEXT="#000000" LINK="#0000FF" VLINK="#330088" ALINK="#FF0044">
<title>Gerard J. Holzmann, Abstracts</title>
<center><h3>Abstracts, Gerard J. Holzmann</h3></center>
<p><img src="/cm/share/paper.gif" alt="----------"><p>
<h3>Software Model Checking: Extracting verification models from source code</h3>
Invited Paper.
<i>Proc. PSTV/FORTE99</i>
Publ. Kluwer, Oct. 1999, Beijing China.
<i><a href="gz/fortepstv99.ps.gz">(Postscript)</a></i>
<p>(with Margaret H. Smith)
<p>
To formally verify a large software application, the standard
method is to invest a considerable amount of time and expertise
into the manual construction of an abstract model, which is then
analyzed for its properties by either a mechanized or by a human
prover.
There are two main problems with this approach.
The first problem is that this verification method can be no more
reliable than the humans that perform the manual steps.
if rate of error for human work is a function of problem size, this
holds not only for the construction of the original application
but also for the construction of the model.
This means that the verification process tends to become unreliable
for larger applications. The second problem is one of timing and
relevance. Software applications built by teams of programmers can
change rapidly, often daily. Manually constructing a faithful
abstraction of any one version of the application, though, can take
weeks or months. The results of a verification, then, can quickly
become irrelevant to an ongoing desing effort.
In this paper we sketch a verification method that aims to avoid
these problems. This method, based on automated model extraction
from C code, was first applied in the verification of the call
processing software for a new Lucent Technologies'
system called PathStar(r).
<p>
<h3>A Practical Method for Verifying Event-Driven Software</h3>
Invited Paper.
<i>Proc. ICSE99, International Conference on Software Engineering.</i>
Publ. IEEE/ACM. May 1999, Los Angeles.
<i><a href="gz/icse_99.ps.gz">(Postscript)</a></i>
<p>(with Margaret H. Smith)
<p>
Formal verification methods are used only
sparingly in software development.
The most successful methods to date are based
on the use of model checking tools. To use
such tools, the user defines a faithful
abstraction of the application (the model),
defines how the application interacts with its
environment, and formulates the properties that it
should satisfy. Each step in this process can
become an obstacle, and, generally, to complete
the entire verification process successfully
often requires specialized knowledge of
verification techniques and a considerable
investment of time.
<br>
In this paper we describe a verification method
that requires little or no specialized knowledge
in model construction. It allows us to extract a model
mechanically from the source of an application.
Interface definitions and property specifications have
meaningful defaults that can get the user started quickly
with a verification effort. The defaults can be adjusted
when desired.
All checks can be executed mechanically, even when the
application itself continues to evolve. Compared to
conventional software testing, the thoroughness of a
check of this type is unprecedented.
<h3>On Checking Model Checkers</h3>
Invited Paper.
<i>Proc. CAV98, Vancouver, June 1998, LNCS 1427, pp. 61-70.</i>
<i><a href="gz/cav98.ps.gz">(Postscript)</a></i>
<p>
It has become a good practice to expect authors
of new algorithms for model checking applications
to provide not only rigorous evidence of an
algorithm's correctness, but also
evidence of its practical significance. Though the rules for
determining what is and what is not a good proof of
correctness are clear, no comparable rules are usually
enforced for determining the soundness of the data that
the author provides to support a claim to practical
value. We consider here how we can flag the more common
types of omission.
<h3>Interval Reduction through Requirements Analysis</h3>
<i>Bell Labs Technical Journal, Vol. 3, No. 2, 1998, pp. 22-31.</i>
<i><a href="gz/bltj98.ps.gz">(Postscript)</a></i>
<p>(with Margaret H. Smith)
<p>
A notable part of
the delays that can be encountered in
system design projects are caused
by logical inconsistencies that are often
inadvertently inserted in the early phases
of software design.
<br>
Many of these inconsistencies are ultimately
caught in design and code reviews, or in systems testing.
In the current design process, though, these errors
are rarely caught {\em before} the implementation of
the system nears completion.
<br>
We show that modeling and verifying the requirements separately,
before system design proper begins, can help to intercept the
ambiguities and inconsistencies that may otherwise not
be caught until testing or field use.
By doing so, one can prevent a class of errors
from entering the development phase, and thereby reduce
time to market, while at the same time
improving overall design quality.
<br>
We demonstrate this approach with an example
where we use the LTL model checking system {\sc Spin},
developed at Bell Labs, to mechanically verify the
logical consistency of a high level design for one of
Lucent's new products.
It is estimated that interval reductions of 10 to 20 percent
can be achieved by applying early fault detection
techniques of this type.
<h3>Designing executable abstractions</h3>
Keynote address.
<i>Proc. Formal Methods in Software Practice, March 1998</i>
<i><a href="gz/fmsp98.ps.gz">(Postscript)</a></i>
<p>
It is well-known that in general the problem of deciding
whether a program halts (or can deadlock) is undecidable.
Model checkers, therefore, cannot be applied to arbitrary
programs, but work with well-defined abstractions of programs.
The feasibility of a verification often depends on the type
of abstraction that is made. Abstraction is indeed the most
powerful tool that the user of a model checking tool can apply,
yet it is often perceived as a temporary inconvenience.
<h3>Validating Requirements for Fault Tolerant Systems using Model Checking</h3>
<i>Proc. ICRE98, International Conference on Requirements Engineering, April 1998</i>
<i><a href="gz/nasa98.ps.gz">(Postscript)</a></i>
<p>(with F. Schneider, S.M. Easterbrook, J.R. Callahan)
<p>
Model checking is shown to be an effective tool in validating
the behavior of a fault tolerant embedded spacecraft controller.
The case study presented here shows that by judiciously
abstracting away extraneous complexity, the state space of the
model could be exhaustively searched allowing critical functional
requirements to be validated down to the design level.
Abstracting away detail not germane to the problem of interest
leaves by definition a partial specification. The success of this
procedure shows that it is feasible to effectively validate a
partial specification with this technique. Three anomalies were
found in the system. One was an error in the detailed requirements,
and the other two were missing/ambiguous requirements. Because
the method allows validation of partial specifications, it is also
an effective approach for maintaining fidelity between a co-evolving
specification and an implementation.
<h3>A Minimized Automaton Representation of Reachable States</h3>
<i>June 1997, to appear in STTT (Software Tools for Technology Transfer, Springer Verlag)</i>
<i><a href="gz/sttt98.ps.gz">(Postscript)</a></i>
<p>(with Anuj Puri)
<p>
We consider the problem of storing a set of states S as a
deterministic finite automaton (DFA). We show that inserting
or deleting states can be done in expected time linear
in the length of the state descriptor. The insertions and deletions
preserve the minimality of the DFA.
We discuss an application of this work to the reduction of the mem
Design and Validation of Computer Protocols
5星 · 超过95%的资源 需积分: 9 175 浏览量
2009-03-01
23:24:31
上传
评论
收藏 1.33MB RAR 举报 
Design and Validation of Computer Protocols.rar （29个子文件） 
Protocol_book 
abs.html 46KB
ch5_pdf.gz 49KB conclusion_pdf.gz 3KB README.html 4KB whatispin.html 14KB ch9_pdf.gz 52KB appE_pdf.gz 125KB appC_pdf.gz 21KB ch14_pdf.gz 57KB appB_pdf.gz 9KB ch7_pdf.gz 98KB ch3_pdf.gz 81KB ch2_pdf.gz 88KB popd.html 11KB ch10_pdf.gz 23KB preface_pdf.gz 6KB ch6_pdf.gz 43KB references_pdf.gz 46KB ch8_pdf.gz 81KB ch12_pdf.gz 114KB ch11_pdf.gz 89KB ch4_pdf.gz 116KB appF_pdf.gz 10KB ch1_pdf.gz 61KB contents_pdf.gz 9KB ch13_pdf.gz 52KB gerard.html 5KB appD_pdf.gz 54KB appA_pdf.gz 44KB资源评论
yza05082015-06-11找了好久，谢谢分享！ 协议设计基础书籍，好用。- gabriel_wangjx2011-10-24内容还不错 涉及到了软件设计验证的一些理论
bobey
- 粉丝: 7
- 资源: 22
最新资源
- 基于Java和Javascript的工程建设综合管理系统材料管理模块设计源码 - material
- c51_2_2.c
- ASCII American Standard Code for Information Interchange
- 一个chm格式的 SQL 函数手册-SQL语言手册文档
- 计算当前月份的天数和剩余天数
- 基于ARM的指令调度和延迟分支
- 基于Vue和TypeScript的极简聊天应用设计源码 - HasChat
- 基于Vue2全家桶和Zcool数据的图片收集网站设计源码 - cool-picture
- 基于C和C++的二维绘制工具设计源码 - DrawPro
- Object.defineProperty 的 IE 补丁object-defineproperty-ie-master.zip
资源上传下载、课程学习等过程中有任何疑问或建议，欢迎提出宝贵意见哦~我们会及时处理！
点击此处反馈
