没有合适的资源?快使用搜索试试~ 我知道了~
资源推荐
资源详情
资源评论
[ Team LiB ]
• Table of Contents
Spin Model Checker, The: Primer and Reference Manual
By Gerard J. Holzmann
Publisher: Addison Wesley
Pub Date: September 04, 2003
ISBN: 0-321-22862-6
Pages: 608
SPIN is the world's most popular, and arguably one of the world's most powerful, tools for detecting software defects
in concurrent system designs. Literally thousands of people have used SPIN since it was first introduced almost fifteen
years ago. The tool has been applied to everything from the verification of complex call processing software that is
used in telephone exchanges, to the validation of intricate control software for interplanetary spacecraft.
This is the most comprehensive reference guide to SPIN, written by the principal designer of the tool. It covers the
tool's specification language and theoretical foundation, and gives detailed advice on methods for tackling the most
complex software verification problems.
Design and verify both abstract and detailed verification models of complex systems software
Develop a solid understanding of the theory behind logic model checking
Become an expert user of the SPIN command line interface, the Xspin graphical user interface, and the
TimeLine editing tool
Learn the basic theory of omega automata, linear temporal logic, depth-first and breadth-first search, search
optimization, and model extraction from source code
The SPIN software was awarded the prestigious Software System Award by the Association for Computing
Machinery (ACM), which previously recognized systems such as UNIX, SmallTalk, TCP/IP, Tcl/Tk, and the World
Wide Web.
[ Team LiB ]
[ Team LiB ]
• Table of Contents
Spin Model Checker, The: Primer and Reference Manual
By Gerard J. Holzmann
Publisher: Addison Wesley
Pub Date: September 04, 2003
ISBN: 0-321-22862-6
Pages: 608
Copyright
Preface
Logic Model Checking
The SPIN Model Checker
Book Structure
Chapter 1. Finding Bugs in Concurrent Systems
Circular Blocking
Deadly Embrace
Mismatched Assumptions
Fundamental Problems of Concurrency
Chapter 2. Building Verification Models
SPIN
PROMELA
Examples
Hello World
Producers and Consumers
Extending the Example
Mutual Exclusion
Message Passing
In Summary
Bibliographic Notes
Chapter 3. An Overview of PROMELA
Types of Objects
Processes
Provided Clauses
Data Objects
Data Structures
Message Channels
Channel Poll Operations
Sorted Send And Random Receive
Rendezvous Communication
Rules For Executability
Assignments And Expressions
Control Flow: Compound Statements
Atomic Sequences
Deterministic Steps
Selection
Repetition
Escape Sequences
Inline Definitions
Reading Input
Special Features
Finding Out More
Chapter 4. Defining Correctness Claims
Stronger Proof
Basic Types of Claims
Basic Assertions
Meta Labels
Fair Cycles
Never Claims
The Link With LTL
Trace Assertions
Notrace
Predefined Variables and Functions
Remote Referencing
Path Quantification
Formalities
Finding Out More
Chapter 5. Using Design Abstraction
What Makes a Good Design Abstraction?
Data and Control
The Smallest Sufficient Model
Avoiding Redundancy
Counters
Sinks, Sources, and Filters
Simple Refutation Models
Pathfinder
A Disk-Head Scheduler
Controlling Complexity
Example
A Formal Basis for Reduction
Example – A File Server
In Summary
Bibliographic Notes
Chapter 6. Automata and Logic
Automata
Omega Acceptance
The Stutter Extension Rule
Finite States, Infinite Runs
Other Types of Acceptance
Logic
Temporal Logic
Recurrence and Stability
Using Temporal Logic
Valuation Sequences
Stutter Invariance
Fairness
From Logic To Automata
An Example
Omega-Regular Properties
Other Logics
Bibliographic Notes
Chapter 7. PROMELA Semantics
Transition Relation
Operational Model
Operational Model, Semantics Engine
Interpreting PROMELA Models
Three Examples
Verification
The Never Claim
Chapter 8. Search Algorithms
Depth-First Search
Checking Safety Properties
Depth-Limited Search
Trade-Offs
Breadth-First Search
Checking Liveness Properties
Adding Fairness
The SPIN Implementation
Complexity Revisited
Bibliographic Notes
Chapter 9. Search Optimization
Partial Order Reduction
Visibility
Statement Merging
State Compression
Collapse Compression
Minimized Automaton Representation
Bitstate Hashing
Bloom Filters
Hash-Compact
Bibliographic Notes
Chapter 10. Notes on Model Extraction
The Role of Abstraction
From ANSI-C to PROMELA
Embedded Assertions
A Framework for Abstraction
Sound and Complete Abstraction
Selective Data Hiding
Example
Bolder Abstractions
Dealing With False Negatives
Thorny Issues With Embedded C Code
The Model Extraction Process
The Halting Problem Revisited
Bibliographic Notes
Chapter 11. Using SPIN
SPIN Structure
Roadmap
Simulation
Random Simulation
Interactive Simulation
Guided Simulation
Verification
Generating a Verifier
Compiling the Verifier
Tuning a Verification Run
The Number of Reachable States
Search Depth
Cycle Detection
Inspecting Error Traces
Internal State Numbers
Special Cases
Disabling Partial Order Reduction
Boosting Performance
Separate Compilation
Lowering Verification Complexity
Chapter 12. Notes on XSPIN
Starting a Session With XSPIN
The File Menu
The Edit Menu
The Help Menu
The Run Menu
Syntax Check
Property-Based Slicing
Set Simulation Parameters
(Re)Run Simulation
Set Verification Parameters
(Re)Run Verification
LTL Property Manager
The Automaton View Option
In Summary
Chapter 13. The Timeline Editor
An Example
Types of Events
Defining Events
Matching a Timeline
Automata Definitions
Constraints
Variations on a Theme
Timelines With One Event
Timelines With Multiple Events
The Link With LTL
剩余689页未读,继续阅读
orzorz
- 粉丝: 48
- 资源: 13
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功
- 1
- 2
前往页