SPIN模型检查器：并发系统缺陷检测工具

5星 · 超过95%的资源需积分: 10 166 浏览量更新于2024-07-25 1 收藏 3.91MB PDF 举报

"SPIN模型检测器是一种广泛使用的并发系统设计中的软件缺陷检测工具，由Gerard J. Holzmann编写并由Addison Wesley出版。该工具被应用于各种领域，从电话交换系统的复杂呼叫处理软件到行星际航天器的精密控制软件的验证。《Spin Model Checker： Primer and Reference Manual》是关于SPIN的最全面的参考指南，由工具的主要设计师撰写，旨在帮助用户深入理解其规格语言、理论基础，并提供解决最复杂软件验证问题的方法。" 在并发编程中，资源竞争是一个关键的问题，可能导致死锁、活锁和数据不一致性等错误。SPIN模型检测器就是为了解决这类问题而设计的，它使用一种称为Promela的语言来描述并发进程的行为。Promela是一种过程交互语言，允许开发者表示并发执行的线程以及它们之间的通信和同步。此参考手册首先介绍了SPIN模型检测器的基本概念，包括模型检查的基本原理，这是一种自动化的验证方法，用于检查系统是否满足预定的性质。通过逻辑模型检查，SPIN可以遍历所有可能的执行路径，确保没有可能导致错误的行为。在深入理论部分，读者将学习到如何使用Promela构建抽象和详细的验证模型。这些模型可以用来模拟并发系统的行为，包括进程的创建、通信机制（如信号量和消息传递）以及各种同步原语。此外，手册还涵盖了如何描述系统性质，例如无死锁、无饥饿状态等安全性与活性属性。 SPIN的命令行界面是另一个重点，用户将学习如何有效地使用命令行选项来配置和运行模型检查任务。这包括指定模型、设置断言、限制搜索空间以及报告和解释检查结果。手册还可能包含解决性能问题的技巧，如使用部分展开和动态符号执行等优化技术。此外，SPIN模型检测器的使用不仅限于软件工程，它也在硬件设计验证、协议分析和安全研究等领域有所应用。通过掌握SPIN，开发者和验证工程师能够更有效地预防和发现并发系统中的潜在错误，提高软件的质量和可靠性。《Spin Model Checker： Primer and Reference Manual》为读者提供了丰富的资源，帮助他们成为SPIN工具的专家，能够在实践中设计、验证复杂的并发系统模型，并解决高级的软件验证挑战。

[ Team LiB ]

Book Structure

SPIN can be used to thoroughly check high-level models of concurrent systems. This means that we first have to

explain how one can conveniently model the behavior of a concurrent system in such a way that SPIN can check it.

Next, we have to show how to define correctness properties for the detailed checks, and how to design abstraction

methods that can be used to render seemingly complex verification problems tractable. We do all this in the first part

of this book, Chapters 1 to 5.

The second part, Chapters 6 to 10, provides a treatment of the theory behind software model checking, and a

detailed explanation of the fundamental algorithms that are used in SPIN.

The third part of the book, Chapters 11 to 15, contains more targeted help in getting started with the practical

application of the tool. In this part of the book we discuss the command line interface to SPIN, the graphical user

interface XSPIN, and also a closely related graphical tool that can be used for an intuitive specification of correctness

properties, the Timeline editor. This part is concluded with a discussion of the application of SPIN to a range of

standard problems in distributed systems design.

Chapters 16 to 19, the fourth and last part of the book, include a complete set of reference materials for SPIN and

its input language, information that was so far only available in scattered form in books, tutorials, papers, and Web

pages. This part contains a full set of manual pages for every language construct and every tool option available in the

most recent versions of SPIN and XSPIN.

The Web site http://spinroot.com/spin/Doc/Book_extras/ contains online versions of all examples used in this book,

some lecture materials, and an up to date list of errata.

For courses in model checking techniques, the material included here can provide both a thorough understanding of

the theory of logic model checking and hands-on training with the practical application of a well-known model

checking system. For a more targeted use that is focused directly on the practical application of SPIN, the more

foundational part of the book can be skipped.

A first version of this text was used for several courses in formal verification techniques that I taught at Princeton

University in New Jersey, at Columbia University in New York, and at the Royal Institute of Technology in

Stockholm, Sweden, in the early nineties. I am most grateful to everyone who gave feedback, caught errors, and

made suggestions for improvements, as well as to all dedicated SPIN users who have graciously done this throughout

the years, and who fortunately continue to do so.

I especially would like to thank Dragan Bosnacki, from Eindhoven University in The Netherlands, who read multiple

drafts for this book with an unusually keen eye for spotting inconsistencies, and intercepting flaws. I would also like to

thank Al Aho, Rajeev Alur, Jon Bentley, Ramesh Bharadwaj, Ed Brinksma, Marsha Chechik, Costas Courcoubetis,

Dennis Dams, Matt Dwyer, Vic Du, Kousha Etessami, Michael Ferguson, Rob Gerth, Patrice Godefroid, Jan Hajek,

John Hatcliff, Klaus Havelund, Leszek Holenderski, Brian Kernighan, Orna Kupferman, Bob Kurshan, Pedro

Merino, Alice Miller, Doug McIlroy, Anna Beate Oestreicher, Doron Peled, Rob Pike, Amir Pnueli, Anuj Puri,

Norman Ramsey, Jim Reeds, Dennis Ritchie, Willem-Paul de Roever, Judi Romijn, Theo Ruys, Ravi Sethi, Margaret

Smith, Heikki Tauriainen, Ken Thompson, Howard Trickey, Moshe Vardi, Phil Winterbottom, Pierre Wolper,

Mihalis Yannakakis, and Ozan Yigit, for their often profound influence that helped to shape the tool, and this book.

Gerard J. Holzmann

gholzmann@acm.org

[ Team LiB ]

Chapter 1. Finding Bugs in Concurrent Systems

"For we can get some idea of a whole from a part, but never knowledge or exact opinion."

—(Polybius, ca. 150 B.C., Histories, Book I:4)

SPIN can be used to verify correctness requirements for systems of concurrently executing processes. The tool

works by thoroughly checking either hand-built or mechanically generated models that capture the essential elements

of a distributed systems design. If a requirement is not satisfied, SPIN can produce a sample execution of the model

to demonstrate this.

There are two basic ways of working with SPIN in systems design. The first method, and the primary focus of this

book, is to use the tool to construct verification models that can be shown to have all the required system properties.

Once the basic design of a system has been shown to be logically sound, it can be implemented with confidence. A

second, less direct, method is to start from an implementation and to convert critical parts of that implementation

mechanically into verification models that are then analyzed with SPIN. Automated model extraction tools have been

built to convert programs written in mainstream programming languages such as Java and C into SPIN models. A

discussion of the latter approach to software verification is given in Chapter 10, and the constructs in SPIN that

directly support model extraction techniques are discussed in Chapter 17.

We begin by considering in a little more detail what makes it so hard to test concurrent software systems, and why

there is a need for tools such as SPIN.

It is worth noting up front that the difficulty we encounter when trying to reason about concurrent systems is not

restricted to software design. Almost everything of interest that happens in our world involves concurrency and access

to shared resources. In the supermarket, customers compete for shared resources, both consumable ones (such as

food items) and non-consumable ones (such as checkout clerks). Customers follow simple, and very ancient,

protocols for breaking ties and resolving conflicts. On the road, cars compete for access to road intersections and

parking spots. In telephone systems, similarly, large numbers of simultaneous users compete for shared resources, this

time with the unique feature that the users themselves are among the resources being shared. Problems of interaction

occur in all these cases, and any new and untried set of rules that we may come up with to solve these problems can

backfire in unexpected, sometimes amusing, and sometimes disastrous, ways.

[ Team LiB ]

Circular Blocking

As a simple example, we can look at the protocol rules that regulate the movements of cars across intersections.

There is no unique solution, or even a best solution to this problem, as testified by the widely different standards that

have been adopted in different countries around the world. In the U.S., when two roads intersect, one direction of

traffic always explicitly has priority over the other direction, as indicated by markings on the pavement and by

roadsigns. At traffic circles, however, an implicit rule applies, rarely explicitly indicated, giving priority to traffic inside

the circle. The implicit rule for circles is sensible, since it gives priority to cars leaving the circle over cars trying to

enter it, which can avoid congestion problems.

In some European countries, the implicit and explicit rules are reversed. In the Netherlands, for instance, an implicit

rule states that at otherwise unmarked intersections cars approaching from one's right have the right of way. The rule

for traffic circles is explicitly marked to override this rule, again giving priority to traffic inside the circle. The implicit

rule for unmarked intersections is simple and effective. But this rule can have unexpected consequences under heavy

traffic conditions, as illustrated in Figure 1.1. It is not even true that we could avoid this problem with traffic lights that

regularly reverse priority rules. One visit to a sufficiently large city will suffice to make it clear that this cannot prevent

the problem. A fixed priority rule is not preferable either, since it will allow one direction of traffic to deny access to

the other direction for any length of time. On the road, the occurrence of these conditions is typically accepted as just

another fact of life. When they occur, they can often only be resolved by breaking the otherwise agreed upon rules. It

will be clear that in software systems we cannot rely on such resolutions: The rules must cover all conceivable cases,

and unfortunately, they must also cover all the humanly inconceivable ones.

Figure 1.1. Circular Blocking

[ Team LiB ]

Deadly Embrace

As another everyday example, to make a person-to-person call, a user must secure exclusive access to at least two

shared resources in the telephone system: the line of the calling party and the line of the called party. The resources

are allocated in a fixed order. Access is always first granted to the calling party's line and only then to the called

party's line. Normally this causes no hardship, but when two subscribers A and B simultaneously attempt to establish

a connection to each other, the access rules will prevent this. If both parties repeatedly pick up the receiver

simultaneously to dial the connection, and refuse to give up until access is granted, they will repeatedly fail. This is

especially curious because the two requests do not actually conflict: both subscribers desire the connection.

A very similar problem is encountered in the management of shared resources in operating systems. Virtually every

textbook on operating systems contains a description of the problem. In the example used there, the shared resources

are typically a line printer (A) and a card reader (B); the example is indeed that old. Two user processes then

compete for exclusive access to these resources, both of which may be needed simultaneously, for instance to print a

deck of punchcards. A deadly embrace is entered when both processes succeed in obtaining access to one of the two

resources and then decide to wait indefinitely for the other. Of course it will not do to just require the processes to

yield resources back to the operating system while waiting for more resources to become available.

The generic sequence of steps leading into the deadly embrace is illustrated in Figure 1.2. The solid arrows indicate

the control-flow order in the two user processes. Once the two dashed states are reached simultaneously, there is no

way to proceed. The dotted arrows indicate the dependency relations that prevent progress. Before device B can be

obtained by the first process, it must first be released by the second process, and before device A can be obtained by

the second process, it must first be released by the first. The circular dependencies illustrate the deadly embrace.

Figure 1.2. Deadly Embrace

[ Team LiB ]

Mismatched Assumptions

It is a trusted premise of systems engineering that large systems should be built from smaller components, each of

which can be designed and tested with a high degree of confidence. Ideally, the final system is then only assembled

when all the smaller pieces have been proven correct. Some design problems, though, only become evident at the

system level, and the absence of reliable methods for testing system level problems can sometimes take us by surprise.

Decisions that are perfectly legitimate at the component level can have unexpected, and sometimes dramatic

consequences at the system level.

A good illustration of this phenomenon is what happened September 14, 1993 on the runway at Warsaw airport in

Poland.[1] A Lufthansa Airbus A320-200 with 72 people on board was landing in heavy rain. The plane was not

getting much traction from the wheels in the landing gear on the wet runway, but the pilots knew that they could count

on the thrust reversers on the main engines to bring the plane to a stop. As it happened, the thrust reversers failed to

deploy in time, and the plane overshot the end of the runway.

[1] A description of this accident can be found on the Web site www.crashdatabase.com.

A thrust reverser should, of course, never be activated when a plane is in flight. Most planes, therefore, have

elaborate protection built-in to prevent this from happening. This includes, for instance, that the thrust reversers cannot

be deployed unless three conditions are met: the landing gear must be down, the wheels must be turning, and the

weight of the plane must be carried on the wheels. In this case the landing gear was down, but the wheels were

hydroplaning, and an unexpected tailwind provided enough lift on the wings that the control software did not decide

until nine seconds after touchdown that the plane had landed. Two people lost their lives when the plane went off the

end of the runway.

The most fascinating aspect of an accident like this is that no one really made any mistakes in the design or operation

of this plane. All components were designed in a very sensible manner. The control software for the thrust reversers,

though, was not designed to cope with the unexpected combination of events that occurred. This software formed one

component in a complex system with many other interacting parts, including the dominant weather conditions that can

affect a plane's operation.

When complex systems fail, the scenarios that trigger the failures usually could not easily have been imagined by any

sensible human designer. For every one failure scenario that is considered, there are a million others that may be

overlooked. In cases like this, it is invaluable to have design tools that can hunt down the potential error scenarios

automatically, working from a sober description of the individual piece parts that together form a more complex

integrated system. Automated tools have no trouble constructing the bizarre scenarios that no sane human could

image—just the type of scenario that causes real-life systems to crash.

"The most pernicious and subtle bugs are system bugs arising from mismatched assumptions made by the authors of

various components."

(Fred Brooks, The Mythical Man-Month, p.142)

[ Team LiB ]

剩余689页未读，继续阅读

陈新

粉丝: 0
资源: 6

SPIN模型检查器：并发系统缺陷检测工具

模型检测器SPIN图形化工具的研究与应用

并发系统的Promela语言建模与SPIN模型检测

Spin Model Checker, The Primer and Reference Manual

Henzinger-模型检查手册

spin516.tar.gz

The Spin Model Checker_Primer and Reference Manual (PDF格式)

NJ指令基准手册算法优化：提升指令执行效率的6大方法

Go语言并发编程实战手册：sync包WaitGroup与互斥锁深入剖析

国民经济行业分类与国际标准行业分类（ISIC+Rev.4）的对照和匹配（供参考）.docx

网络助手工具(亲测好用)

最新资源