在Engee中生成Promela

形式化验证 Engee*中的基于*Spin*系统支持的*Promela（PROcess MEta LAnguage）中的形式化模型的自动生成。

Promela发生器转换有限自动机的图表（图表），输入和输出端口，以及虚拟子系统将*Engee*模型转换为文本形式规范 — .pml,pml-文件。

本规范以状态、转换和逻辑条件的形式描述了模型的行为，然后可以通过旋转工具根据指定的LTL公式对其进行检查。这种方法允许您使用现有的*Engee*模型，而无需手动将其重写为单独的正式符号。

运行代码生成器

从*Engee*模型文件在Promela中生成代码是通过访问*Engee*API来执行的，例如，从窗口命令行 img 41 1 2 :

engee.generate_code(source, destination, target="promela")

哪里

资料来源 --string，模型文件的路径。工程师;
目的地 --string，将放置生成文件的目录的路径。

API使用模型文件名作为生成文件的名称（后缀"。engee"排除在外），以新后缀"结尾。pml"。

例如，如果模型文件的路径为 资料来源 — "/user/models/large_model。工程师"，以及生成文件的目录 目的地 — "/用户/旋转"，然后用Promela语言生成的代码将被放置在一个文件中，其路径 — "/user/spin/large_model。pml".

工程师的正式核实程序

创建有限状态机模型（在块内 Chart）在*Engee*。
使用函数生成正式的Promela模型 generate_code 指定目标语言: 恩吉。generate_code(source,destination,target="promela").
以LTL公式的形式添加正式属性。
使用自旋工具检查模型。
结果分析：成功证明，反例，执行路径。

→

模型的局限性

如果模型包含不在列表中的块或类型，则调用API以生成Promela代码的尝试将失败。

不支持:

多重采样步骤;
*图表*块的时间运算符(t, 以前, 之后…);
图表块的操作符 计数 和 持续时间;
Julia库函数，如 战俘, 楼层, 齐尔… .

块支持

目前，Promela生成器的功能仅限于支持几种类型的模型块。:

数据类型支持

此外，仅支持由Promela中具有类似物的这些类型的元素组成的那些数据类型和数组。:

朱莉娅型	普罗梅拉型
`布尔`	`布尔` 或 `位`
`UInt8`	`查尔` 或 `字节`
`Int16`	`短`
`Int32`	`int型`

朱莉娅型

普罗梅拉型

布尔

布尔 或 位

UInt8

查尔 或 字节

Int16

短

Int32

int型

Julia语法支持

Promela代码生成器支持在*Chart*块的代码插入中找到的几乎所有Julia语法和支持C语言代码生成器。

许多设计在Promela中没有直接类似物，因此不支持。:

操作员 继续;
嵌套循环 为 （或具有复杂条件的循环）;
周期 为 以1以外的增量计算;
操作员 ,.

附加语法实现:

@后藤
@标签