在Engee中的形式化验证

*形式化验证*是一种数学分析方法，可以完全调查模型相对于指定属性的所有可能行为。

与仅执行单个场景的常规模拟不同，形式化验证允许我们证明模型的某个属性始终得到满足，或者识别反例。

形式化验证很好地补充了Engee中面向模型的方法：相同的模型可用于仿真，代码生成和行为验证。

在工程中的实际实施

在*Engee*环境中，通过Promela语言的形式化模型的生成及其使用自旋系统的自动验证来实现形式化验证。

Promela（过程元语言）是一种用于规范需求模型或程序的语言。
Spin（简单的Promela解释器）--一个允许:
1. 用Promela语言解释模型描述（模拟模式模型);
2. 从Promela语言的模型描述生成并规格由公式指定零担, C验证程序允许对规范进行自动形式化验证，特别是:
  - 检查规范中指定的不变量;
  - 如果不变量不满足，请查找反例。

在文章中阅读有关Promela generation in*Engee*的更多信息在Engee中生成Promela.

Engee中的形式化验证是基于对模型行为进行完整研究的思想。

例如，在创建模型时状态机(在块 Chart），其可视化图本身无法自动检查。因此，在启动Spin之前，模型被转化为Promela语言中严格定义的形式描述。

正是通过这种形式表示，Spin才起作用：它以数学方式分析模型，迭代可能的过渡序列，并验证指定的属性（LTL公式）是否满足。

这种方法是指*形式化方法*--基于系统行为的精确数学描述的方法。与传统测试不同的是，正式方法允许您完全探索模型，而无需选择输入数据，也无需手动分析转换。

结果，Engee模型成为一个数学严谨的对象：所有状态，变量和转换都被记录为Promela代码，Spin检查这个正式模型的整个状态空间并确定是否满足指定的属性。

在*Engee*中，在Promela上生成代码时会自动创建正式模型。此模型描述:

形式模型应该是*明确的*：语法和语义不允许有歧义的解释。得益于此，自旋工具可以精确地在数学上探索模型，并对属性进行严格的验证。

在构造形式化模型之后，执行*形式化分析*，这是一个以数学方式验证模型是否满足指定属性和要求的过程。

*形式分析*是验证与模型执行选项的完整搜索。在分析过程中，调查所有可能的状态和转换，提供对指定属性的确认或反驳的保证。

形式化分析中的属性是模型的可验证要求。每个属性被制定为单独的验证案例（例如，以LTL公式的形式）。确定完整的属性集并验证其实现，可以确保模型的行为等同于规定的要求。:

基于模型的设计和形式验证自然是相辅相成的。在可视环境中创建的模型（例如，使用*Chart*块）已经是系统行为的机器可读描述。

这允许您直接对其应用正式方法，而无需手动创建单独的正式规范。

当从Engee模型生成Promela时，使用块，状态和转换的现有结构，因此形式验证成为通常建模过程的延续。这种方法的优点: