自旋验证和规范模式
从*Engee*环境生成Promela语言的形式化模型后，用户可以使用自旋工具验证其正确性。
自旋程序支持多种操作模式，允许您研究模型的行为，执行其模拟，并执行指定属性的形式化验证。
本文介绍了主要的自旋模式：模拟和验证，以及添加LTL规范、生成验证器、分析结果和搜索反例的过程。
旋转的主要操作模式和验证从Engee生成的模型的实际步骤如下所述。
Spin:模拟模式
*模拟模式*允许您以交互方式运行模型并观察系统的行为，而无需检查正式属性。
对于接收到的路径 代码生成从Promela文件的*Engee*模型中，您可以立即使用Spin运行模型的模拟:
spin <имя-файла.pml>如果您尝试使用直接从*Engee*代码生成器获取的Promela文件执行此操作，则会导致无休止的执行。 旋转，由于生成的Promela模型包含无限循环。
与此同时，这种启动模式 旋转 它可以通过在Promela的源代码中添加不变量来研究模型的属性（assertions)和用于生成输入数据值的运算符。
Spin:验证模式
使用自旋程序最有用的模式是生成验证程序。 *验证模式*用于严格验证模型的逻辑属性（LTL规范）和搜索可能的错误或矛盾 *Verifier*是一个C程序，其生命周期包括补充Promela中的模型文本。 按规格, 生成和编译验证程序，以及测试程序 发射及 分析用户的消息。
插入规格
将规范的逻辑公式传输到Spin程序的最简单方法是将它们以一个或多个Promela语言运算符的形式添加到Promela模型文件的末尾。 零担:
...
описание модели
...
ltl spec_name_1 { ... текст формулы ... }
ltl spec_name_2 { ... текст формулы ... }
...
ltl spec_name_3 { ... текст формулы ... }|
为了简洁和清晰 逻辑公式在它们的列表前面，放置定义简单标识符的c预处理器指令可能是有用的-其中使用的缩写。 例如，公式 可以改写为 |
|
定义预处理器宏时，应注意不要重新定义文本后面使用的标识符。 上面的例子不应该从定义一个名称为宏开始 |
生成并运行验证器
使用自旋程序生成和运行验证器有两种主要方法：组合和分离。
在这两种情况下，成功执行验证程序的一个常见先决条件是存在支持ISO C99或更高标准的已安装C编译器。
验证器的联合生成和启动
自旋实用程序可以作为一个外壳，:
-
皈依者
.pml,pml-Promela模型文件到c语言的中间文件; -
调用编译器将中间C文件转换为名为的二进制可执行验证程序文件
潘并在模型验证模式下运行。
命令行 
对于组合生成和启动模式，它必须包含参数 -跑. 命令示例:
spin -run <путь-к-файлу-модели.pml>如果Promela模型文件只包含一个语句 零担，那么这个命令行就足以运行运算符中指定的公式的验证 零担.
如果Promela模型文件包含多个运算符 零担，则在运行此命令行时，将验证按顺序排列的第一个运算符的公式。
选择在启动时将验证哪些公式 自旋跑，您应该另外指定参数 -零担 与运营商的名称 零担.
例如，如果Promela模型文件具有路径 ./模型。pml,pml 并以一组运算符结束。:
ltl spec1 { []a }
ltl spec2 { <>b }这是一个挑战:
spin -run ./model.pml生成并执行公式验证器 []一 有一个名字 规格1. 并为公式生成和执行验证器 <>b 有一个名字 规格2，你需要打电话:
spin -run -ltl spec2 ./model.pml在组合生成和启动模式下，Spin不会将中间文件保存在C中。成功执行程序后，会自动在当前目录中创建一个名为"可执行验证程序"的文件。 潘 （在类UNIX系统上）。 此文件可用于重复 验证程序运行，例如，检查尚未验证的公式。
独立生成和启动验证器
当Spin程序在单独生成和启动验证器的模式下使用时，其主要任务是将Promela模型转换为C验证器的源代码。 假设用户将自己编译中间C文件并运行生成的验证程序。
单独的验证器生成
用于生成C验证器源代码的典型命令行:
spin -a <имя модели.pml>Spin不遵循操作系统返回代码的通常约定，因此您只能通过分析输出到控制台的程序文本来确定Spin是否已成功完成或出现错误。
作为成功生成的结果，Spin创建或复盖具有名称的文件 潘。c, 潘。h, 潘。b, 潘。m 和 潘。t （这些名称是固定的，没有旋转设置来更改它们）。 其中至少有两个 — 潘。c 和 潘。h -必要的下一步。
编译验证器
为了进一步翻译上一步中收到的文件，需要一个支持ISO C99标准或更高标准的c编译器。 编译的命令行可能如下所示:
cc pan.c -o <результирующий-файл>或者，如果验证的公式包含下一个运算符（有关详细信息，请参阅 自旋中的线性时间逻辑(LTL):
cc -DNXT -DNOREDUCE pan.c -o <результирующий-файл>启动验证程序
要启动验证会话，在验证程序的命令行中指定参数就足够了。 -一个.
验证程序可执行文件具有名称时的命令行示例 潘:
./pan -a如果Promela模型文件不包含此命令行的参数就足够了 运营商 零担 或者它只包含一个这样的运算符。
如果运营商 零担 如果有几个公式，那么您需要选择我们要验证的唯一公式。 为此，您需要指定参数 -N 与运营商的名称 零担.
例如，如果Promela模型文件包含运算符 ltl spec1{… }，然后使用命令进行验证:
./pan -a -N spec1分析验证器消息
如果验证者验证了规范的LTL公式，那么应该在验证者向控制台发出的消息中找到有关验证成功或错误的信息，并从该行开始:
<имя-исполняемого-файла-верификатора>: ltl formula <имя-оператора-ltl>验证成功
在验证成功的情况下，如果验证程序可执行文件具有默认名称 潘，而运营商正在验证 零担 有一个名字 规格1，那么验证成功的结果如下所示:
pan: ltl formula spec1
...
State-vector ... byte, depth reached ..., errors: 0
...以上，你应该注意的消息 错误：n，在哪里 n 在验证成功的情况下，它是零。
验证错误
如果验证失败，则控制台的输出如下所示:
<имя-верификатора>: ltl formula <имя-оператора-ltl>
<имя-верификатора>:1: assertion violated ... (at depth ...)
<имя-верификатора>: wrote <имя-файла-модели>.trail
State-vector ... byte, depth reached ..., errors: 1例如，如果模型文件名是 — 模特。pml 验证程序可执行文件具有默认名称 潘，而运营商正在验证 零担 有一个名字 规格2:
ltl spec2 { []a }验证错误的结果可能如下所示:
pan: ltl formula spec2
pan:1: assertion violated !( !(a)) (at depth 0)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 5, errors: 1
...低内存错误
此外，在大型模型的情况下使用大量变量和/或"宽"类型的变量。 短 或 int型 作为状态空间增长的结果，验证器可能没有足够的内存提供给它。 在这种情况下，错误可能会通过以下消息发出信号:
pan: out of memory或
error: max search depth too small如果后者可以在某些情况下通过使用参数来规避 -m N 例如:
spin -run -m10000000 model.pml第一个通常表示模型需要粗化，因为它的状态空间太大，无法使用 旋转.
找到一个反例
在上述验证不成功的示例中，验证程序的控制台输出包含以下行:
pan: wrote model.pml.trail此行表示在验证期间创建了跟踪文件。 模特。的pml。径.
使用Spin实用程序，可以从跟踪文件中提取信息以构建反例，该反例明确驳斥了规范的经过验证的LTL公式。
用于路由分析的最小自旋命令行:
spin -t -p -g -l -k <имя-файла-трассы.trail> <имя-файла-модели.pml>例如，模型文件 模特。pml,pml 包含简单模型的文本:
bool a = true; /* объявление глобальной логической переменной "a",
* инициализированной значением "true"
*/
active proctype fsm() { /* объявление типа процесса "fsm" и его немедленный запуск */
do /* оператор недетерминированного бесконечного цикла */
:: a = true; /* первая возможная ветка цикла */
:: a = false; /* вторая возможная ветка цикла */
od /* окончание оператора цикла */
}
ltl spec1 { []a } /* LTL-формула: "a" истинно всегда */Promela语言中上述示例的语义：全局变量 a 用值初始化 真的 然后它的值随机变化为 错误 或 真的.
与此同时，操作员 零担规格1 断言价值 a 在变量的整个生命周期中必须为true。 a.
挑战 旋转 对于这种情况下的联合生成和验证，它可能如下所示:
spin -run -a model.pml因此，您可以在旋转控制台输出中找到文本。:
pan:1: assertion violated !( !(a)) (at depth 2)
pan: wrote model.pml.trail
...
State-vector 20 byte, depth reached 2, errors: 1
...第一行表示名称 规格1 操作员 零担，其验证导致错误。 第三行包含路由文件的名称 模特。的pml。径，可用于进一步生成反例:
spin -t -k model.pml.trail model.pmlltl spec1: [] (a)
starting claim 1
Never claim moves to line 4 [(1)]
2: proc 0 (fsm:1) model.pml:7 (state 2) [a = 0]
a = 0
spin: _spin_nvr.tmp:3, Error: assertion violated
spin: text of failed assertion: assert(!(!(a)))
Never claim moves to line 3 [assert(!(!(a)))]
spin: trail ends after 3 steps
#processes: 1
a = 0
3: proc 0 (fsm:1) model.pml:5 (state 3)
3: proc - (spec1:1) _spin_nvr.tmp:2 (state 6)
1 processes created在这里，有关反例的基本信息包含在行中:
2: proc 0 (fsm:1) model.pml:7 (state 2) [a = 0]
a = 0
spin: _spin_nvr.tmp:3, Error: assertion violated显示变量 a 获得意义 错误 在文件的第7行 模特。pml,pml. 这是一个建设性的证明，该模型是在其可实现的部分，其中值 a 成了谎言，要求相反的零担公式相互矛盾。 为了消除这种矛盾，有必要修改模型或其规范（运算符 零担规格1).