FDR 4.2 使用手册：牛津大学CSP验证工具

需积分: 10 64 浏览量更新于2024-07-17 收藏 2.74MB PDF 举报

"fdr 4.2文档是牛津大学开发的CSP验证工具FDR的使用手册，主要介绍了如何操作和利用FDR进行形式验证。这份文档详细阐述了FDR的各项功能，包括用户界面、命令行接口、CSPM语言特性、与其他工具的集成以及性能优化等方面。" 《FDR 4.2文档》是牛津大学发布的一份详尽指南，用于指导用户使用FDR 4.2这一CSP（Communicating Sequential Processes）验证工具。CSP是一种形式化的方法，用于描述并发系统的通信和行为。该文档旨在帮助开发者和研究人员理解并有效地运用FDR进行系统验证。文档首先简要介绍了FDR的基本信息，并指出在引用FDR时的引用方式。接着，它深入探讨了FDR的用户界面，包括： 1. **Getting Started**：这部分为新用户提供了一个快速入门的向导，帮助他们了解如何启动和配置FDR环境。 2. **Session Window**：这是用户与FDR交互的主要界面，用于输入和执行CSP公式及命令。 3. **Debug Viewer**：用于查看和分析验证过程中产生的调试信息。 4. **Process Graph Viewer**：展示进程图，直观地表示出CSP过程的结构和相互关系。 5. **Probe**：允许用户检查和修改模型的内部状态。 6. **Node Inspector**：提供对单个节点详细信息的查看。 7. **Communication Graph Viewer**：显示进程间的通信模式和结构。 8. **Machine Structure Viewer**：呈现系统的结构和组件。 9. **Options**：配置FDR的行为和设置，以满足特定需求。此外，文档还详细介绍了FDR的命令行接口，包括不同参数的使用方法、示例、集群使用以及机器可读格式的生成。在CSPM部分，文档涵盖了： - **定义**：CSPM中的基本概念和语法规则。 - **功能语法**：详细描述了CSPM的语法结构和表达方式。 - **定义过程**：如何定义和操作CSP过程。 - **类型系统**：解释了FDR中的类型检查和类型系统，以确保程序的正确性。 - **内置定义**：提供了预定义的CSP元素和函数。 - **性能分析（Proﬁling）**：如何利用FDR进行性能分析，找出潜在的效率问题。 FDR还可以与其他工具集成，文档的第五部分展示了如何使用FDRAPI以及API的实例应用。第六部分讨论了优化技巧，包括压缩技术，以提高验证速度和效率。在实现笔记章节，文档提到了FDR的内部工作原理，如语义模型、编译过程、精炼检查和类型检查。最后，发布注记部分记录了每个版本的更新和改进，提供了版本历史信息。总体来说，《FDR 4.2文档》是学习和使用FDR进行CSP验证的宝贵参考资料，无论你是初学者还是经验丰富的专家，都能从中受益。通过深入阅读和实践，你将能够充分利用FDR的强大功能来验证并发系统的设计和行为。

FDR Manual, Release 4.2.3

2.2.2 The Assertion List

The top-right of the session window, illustrated to the right, displays the list of assertions that have been deﬁned.

This includes all assertions deﬁned in the source ﬁle, together with all of those deﬁned in the session, in the order of

deﬁnition. An assertion may be run by clicking the appropriate Check button. Alternatively, the Run All button may be

clicked, which will run all of the un-checked assertions, in parallel. If an assertion has been run and fails, the Debug

button may be pressed, which will launch the Debug Viewer.

Whilst an assertion is being checked, the progress of the check is displayed inline, just below the title of the assertion.

The status of the assertion is indicated by the small circle next to the title of each assertion. The colours indicate the

following:

Blue The assertion has not yet been run.

Yellow The assertion is currently being checked.

Red The assertion has been checked and has failed.

Green The assertion has been checked and passed.

Clicking the info button (with a question mark) on an individual assertion displays a window that with various perfor-

mance statistics about the reﬁnement check. For example:

12 Chapter 2. The FDR User Interface

FDR Manual, Release 4.2.3

This window displays, in descending order of display:

Compilation Time The time taken to compile the assertion.

Storage Requirements The number of uncompressed bytes to store each node pair encountered during the check.

The total amount of storage required is therefore proportional to the number of visited states times this ﬁgure,

multiplied by the average achieved compression ratio (see below).

Visited States The number of states visited, and the current ply of the breadth-ﬁrst search.

Number of Workers The number of workers used in the parallel breadth-ﬁrst search (this can be conﬁgured using

refinement.bfs.workers).

Ply Sizes The relative size of each of the plys in the breadth-ﬁrst search is indicated by the width of the bars. The

absolute size of a ply can be viewed by hovering over a particular ply in the search. The current ply of the search

is drawn in blue.

Storage Statistics The total amount of memory, allocated for each type of block-level storage in the search. The

cache ﬁgure is the amount of memory used to store uncompressed blocks in memory. Compressed refers to the

amount of memory allocated for storing compressed blocks whilst raw indicates the amount of memory that

would have been required to store the blocks uncompressed. Finally, the achieved compression ratio is given.

Storage statistics are provided for each of the main block stores. Done is the store used to store blocks used

by the set of visited states. Current level is the store used to store blocks used by the set of states to visit

on the current ply of the search. Next level is the store used to store block that will be visited on the next

ply whilst history is the store used to store blocks that indicate how node pairs were reached (for purposes of

counterexample reconstruction). Blocks is the number of memory blocks allocated to store data (note that they

are of a ﬁxed size). Total is simply the sum of the above ﬁgures.

Thus, the total amount of block-level storage required is equal to the total cache size plus the total size of the

2.2. Session Window 13

FDR Manual, Release 4.2.3

2.3 Debug Viewer

The debug viewer, as shown below, allows a counterexample to a reﬁnement assertion to be viewed. In

particular, it attempts to explain how the implementation evolved into a state where it could perform a be-

haviour that was prohibited by the speciﬁcation. Conceptually, the debug viewer is a table where the rows

represent behaviours of particular machines whilst the columns represent events that are synchronised.

The above counterexample, which we use as an example throughout this section, is to the ﬁrst assertion of an edited

version of Dining Philosophers where N = 3 (for ease of exposition).

Warning: Note that the counterexample that is displayed will be picked somewhat non-deterministically. See

Counterexamples for further details.

2.3.1 Behaviours

The individual rows within the counterexample represent the behaviour of a machine. A behaviour of a particular

machine is a sequence of states that the machine transitioned through, along with the events that it performed. In the

default view of a counterexample, the ﬁrst row represents the behaviour of the speciﬁcation machine, whilst the second

row represents the behaviour of the implementation.

On the left of a behaviour row, two

items of information are displayed, as shown to the right. The ﬁrst is the operator that the machine represents, whilst

the second is the name of the machine, if one was given to it in the script. Note that the operator is only displayed if

the machine is a high-level or a compressed machine. Hovering over the operator will reveal the operator type and its

arguments. For example, hovering over the operator in the image to the right displays the following.

Alphabetised parallel with process alphabets:

1: {thinks.0, sits.0, eats.0, getsup.0, picks.0.0, picks.0.1,

picks.2.0, putsdown.0.0, putsdown.0.1, putsdown.2.0}

2: {thinks.1, sits.1, eats.1, getsup.1, picks.0.1, picks.1.1,

picks.1.2, putsdown.0.1, putsdown.1.1, putsdown.1.2}

3: {thinks.2, sits.2, eats.2, getsup.2, picks.1.2, picks.2.0,

picks.2.2, putsdown.1.2, putsdown.2.0, putsdown.2.2}

which indicates that the operator in question is an alphabetised parallel operator with 3 processes, each of which has

the corresponding alphabet.

Hovering over the machine name will display extra information in the right pane that includes the full name (if it

had to be abbreviated), a scrollable view of the trace (which is particularly useful if the trace is long), and a textual

representation of the behaviour, if the row represents an error. For example, hovering over the SYSTEM name in the

above displays the following:

2.3. Debug Viewer 15

FDR Manual, Release 4.2.3

This indicates the trace that SYSTEM performed and the fact it accepted {} at the end of trace, violating the speciﬁca-

tion.

The second component, which is the main section, shows the trace that this machine performed:

Each of the circles represents a state that the machine reaches. The edges between the states are labelled by the events

that the machine performs. Named states are drawn in blue and, when hovering over a state, identical states of the

machine are highlighted in red. A dashed edge indicates that the machine performed no event. Green edges indicate

that the machine was restarted by the event (e.g. consider P = X ; P).

Clicking on a state will reveal several items of information about it including: the state name (if any); the available

events of the state; the minimal acceptances of the state. It also allows Probe to be launched to inspect the state’s

transitions and, providing the machine does not have too many states, allows the Process Graph Viewer to be launched

on the state. If the graph view is launched, then in addition to displaying the usual graph of the machine, the behaviour

in the selected row will be highlighted (see Behaviours for more information).

Clicking on an edge will display several extra pieces of information in the right pane. In particular, if the event is a tau

that resulting from a hiding it will reveal what the inner event is. Further, it will detail what events the leaf processes

perform in order to perform the overall event. For example, hovering over the last event in the above counterexample

(i.e. picks.1.1) in the row labelled Implementation will display the following in the right pane:

This indicates that FORK(2) and PHIL(2) both performed picks.2.2 in order to produce the overall

picks.2.2 event.

The third and rightmost component of a behaviour indicates how this machine contributes to the prohibited behaviour

of the speciﬁcation. For example, consider the following script:

16 Chapter 2. The FDR User Interface

剩余175页未读，继续阅读

筑梦之路

粉丝: 5w+
资源: 250

FDR 4.2 使用手册：牛津大学CSP验证工具

Fragstats4.2

fragstats4.2及官方帮助文档

F8图纸 F8R笔记本

R语言FDR校正代码

matlab做FDR矫正

使用MATLAB进行上述FDR校正

R语言如何做FDR矫正

ATAC peaks 和FDR校验

spm怎么把fdr调出来

matlab实现FDR校正

最新资源