Engee 文档

Promela语法

下面只介绍Promela语言的基本结构，这些结构用于生成Engee模型或用于分析生成的代码。 用于并行程序规范的*Promela*的语法不涉及*Engee*，并且在这里几乎不考虑。

一般（词汇）信息:

  • Promela中的标识符满足正则表达式 [a-zA-Z_][a-zA-Z_0-9]*;

  • 自 旋转 可用的C语言预处理器用作预处理器，支持ISO C99标准的多行和单行（未记录功能）注释。

Promela语言中源文件的结构

Promela语言的程序文本可以由三个主要部分组成:

  • 定义用户定义的数据类型和全局变量;

  • 流程定义;

  • 营办商 零担.

用户定义的数据类型和全局变量的定义

在Promela中，用户定义的数据类型和全局变量的定义可以穿插，但必须放在文件的开头-在进程和运算符的定义之前。 零担.

自定义数据类型

*Engee*中的Promela代码生成器只使用一个Promela构造，用于定义自定义数据类型。 — 打字,打字，用于定义数据结构的类型。

语法 打字,打字 由*工程师使用*:

"typedef" name "{" declaration_list "}" ";"

哪里 姓名 -不是的标识符 关键词Promela和语法 声明_列表 它有表格:

declaration_list ::= declaration ";" { declaration ";" }

declaration ::= type_name variable_name [ "[" array_size "]" ]

type_name ::= "bool" | "byte" | "short" | "int"

variable_name ::= name

array_size ::= constant_expression

常量表达式 -具有整数值的常量表达式。

例如，结构类型声明 S，其中包括:

  • 32位字段 i32 有符号整数类型;

  • 16位字段 我16 有符号整数类型;

  • 8位字段 u8 无符号整数类型;

  • 1位字段 b 无符号整数（逻辑）类型;

  • 阵列 a 的10个逻辑类型元素。

可谓

typedef S {
    int i32;
    short i16;
    byte u8;
    bool b;
    bool a[10];
};

随着语法的更详细的描述 打字,打字 可于 项目页Promela/纺.

全局变量

Promela中定义全局变量的语法如下所示:

global_variable_declaration ::=
    type_name variable_name [ "=" initializer_scalar ] ";"
|   type_name variable_name [ "[" array_size "]" ] [ "=" initializer_list ] ";"

initializer_scalar ::= constant_expression

initializer_list ::= "{" constant_expression [ "," constant_expression ]* "}"

语法 类型名称, 可变名称, array_size 和 常量表达式 如上所述。

可以定义标量变量、一维数组和变量结构。

例如，下面的代码定义了一个变量-一个由5个类型元素组成的数组 字节，用单位初始化:

byte x[5] = {1, 1, 1, 1, 1};

如果标量变量未显式初始化，则 旋转 将其初始值设置为零，如果它是数组或结构，则用零填充其元素。

定义流程

当用Promela语言生成模型时，Engee定义了一个单一类型的过程: fsm （来自"有限状态机"）。

active proctype fsm() { ... }

这意味着过程 fsm 它将在模式中的单个实例中运行 模拟。 如果使用模式 验证，然后是过程的描述 fsm，与LTL规范一起，转换为自动机，将由生成的验证器进行分析。

过程描述的主体由一系列运算符组成，例如局部变量的定义、赋值运算符和程序流控制运算符。

在Promela中，运算符在语义上分为阻塞运算符和非阻塞运算符，但在*Engee*生成器生成的Promela模型中，只使用非阻塞运算符。

局部变量的定义

定义Promela局部变量的语法与 语法全局变量的定义。

无论局部变量定义运算符放置在何处：在过程主体的开始处或在第一次使用之前，执行变量定义，就好像它位于过程主体的开始处一样。

这意味着您不能定义多个具有相同名称的局部变量。 例如:

{ int a; }
{ int a; }

在这种情况下，在声明变量的上下文中执行局部变量的初始化。 即示例中的代码:

int a = 1;
{
    a = 2;
    int b = a + 1;
}

语义上等同于代码:

int a = 1;
int b;
a = 2;
b = a + 1;

不是代码:

int a = 1;
int b = a + 1;
a = 2;

赋值运算符

在赋值运算符的左侧，可以使用标量变量、数组元素或结构的名称。

右侧是包含变量名，逻辑或整数常量的算术或逻辑表达式。

还支持增量运算符（++）和递减（--).

逻辑表达式

在生成Promela*Engee*模型时，可以使用逻辑捆绑包:

  • 否认 — !;

  • 连词（逻辑和） — &&;

  • 析取（逻辑或） — ||.

此外，可以使用比较运算符。 ==, !=, <, ⇐, > 和 >=.

逻辑运算符的参数可以是整数或逻辑类型的表达式。

算术表达式

以下整数算术运算在Promela代码生成器*Engee*中实现：一元 + 和 - 加减乘除模（%).

由于代码生成器使用Julia语言中的表达式作为源表达式，其中除法的结果是类型 浮子,浮子，并且除法运算符Promela中不支持浮点计算 / Promela模型代码生成器未实现。

执行流控制语句

Promela代码生成器可以使用三种类型的控制运算符语法：条件运算符 如果 和两个循环运算符 做 和 为.

条件运算符 如果

在Promela，运营商 如果 它是一种非确定性的 link:https://en.wikipedia.org/wiki/Guarded_Command_LanguageEdsger Dijkstra的[条件运算符]:

if_operator ::= "if" guarded_command_set "fi"

guarded_command_set ::= guarded_command { guarded_command }

guarded_command ::= guard "->" guarded_list

guard ::= boolean_expression | "else"

guarded_list ::= statement ";" { statement ";" }

哪里 声明 --任何Promela操作员，以及 布尔值_表达式 — 逻辑表达。

Promela模型的代码生成器不使用非确定性运算符编程的功能 如果 因此，每个这样的运算符看起来像这样:

if
:: <условие> -> <действие>
:: else -> <альтернативное_действие>
fi

如果没有替代操作，则将其替换为空运算符。 跳过.

一个分支 其他 即使在没有替代动作的情况下也有必要，否则模型可能会被阻止。

例如，操作员

if
:: false -> ...
fi

相当于永恒的等待。

循环运算符 做

在Promela，运营商 做 它是另一个非确定性算子的变体。 — link:https://en.wikipedia.org/wiki/Guarded_Command_LanguageEdsger Dijkstra的[循环运算符]具有类似的语法:

do_operator ::= "do" guarded_command_set "od"

哪里 guarded_command_set 描述的 上。

Promela模型的代码生成器使用循环的确定性版本 做，其中可以有两个分支:

do
:: <условие> -> <действие>
:: else -> break;
od

它相当于一个循环 而:

while (<условие>) {
    <действие>;
}

或一个分支:

do
:: true -> <действие>
od

其对应于无限循环。

循环运算符 为

Promela代码生成器使用三种语法选项之一 为:

for_operator ::= "for" "(" variable_name ":" integer_expression ".." integer_expression ")" "{" statement_list "}"

statement_list::=语句";" { statement ";" }

哪里 可变名称 -本地或全局变量的名称，以及 集成表达式 -具有整数或布尔值类型的表达式。

例如，运算符的语义如下:

for (i : a .. b) {
    x = x + i;
}

以下是表达式 a 和 b 在循环之前计算一次，如果 a⇐b，一个变量 i 始终如一地接受来自 a 以前 b 包容性。

如果 a>b，则不执行循环。

无条件过渡运算符 后藤

Promela支持语法标签:

label_definition ::= label ":"

和无条件过渡算子:

goto_operator ::= "goto" label ";"

哪里 标签 --标签的名称，任何有效的标识符，除了 关键词。

一些标签名称具有特殊的含义 旋转：这些是带有前缀的标签 接受, 完和 进展。 *Engee*中的Promela模型生成器不使用此类标签，建议避免不必要的标签。

不变量（断言）

除了LTL规范机制，Promela语言允许使用运算符进行验证 assert(<逻辑公式>) （有关详细信息，请参阅 断言）。

其语义类似于C/C++语言：如果运算符条件为false，则执行或验证失败。

操作员 断言 它很方便，因为它总是被检查，无论模式如何（模拟仿真 或 核实资料）和所选择的运算符 零担.

Promela关键词

不能用作标识符的保留字列表:

  • 活动

*断言

*原子

*未签名

*布尔

*休息

*字节

*陈

*做

*d_step

*其他

*空

*已启用

*eval

*错误

*fi

*为

*已满

*后藤

*隐藏

*如果

*在

*init

*int

*莱恩

*mtype

*nempty

*永远不会

*nfull

*np_

*od

*的

*pc_value

*打印

*优先级

*proctype

*提供

*运行

*选择

*短

*展示

*跳过

*超时

*追踪

*真实

*typedef

*除非

*xr

*xs

*位

操作员组 零担

Promela中的源文本可能以由运算符组成的块结尾 零担.

运算符语法 零担:

ltl_operator ::= "ltl" name "{" ltl_formula "}"

哪里 姓名 -规格名称(LTL公式），以及 ltl_formula -一个人 LTL线性时间逻辑规范。

有关使用规范的更详细说明，请参阅章节 插入规格及 验证器的生成和启动。

有用的连结

  1. 在Engee中的形式化验证

  2. 在Engee中生成Promela

  3. 自旋验证和规范模式

  4. 自旋中的线性时间逻辑(LTL)

  5. Engee中形式化验证的基本示例

  6. Engee中形式化验证的扩展示例