正式核实 AnyMath

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

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

形式验证很好地补充了基于模型的方法 AnyMath ：相同的模型可用于仿真、代码生成和行为属性验证。

在 AnyMath

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

*Promela(PROcess MEta LAnguage)--用于规范需求模型或程序的语言。

*Spin（简单的Promela解释器）--一个允许:

用Promela语言解释模型描述（模拟模式模型);
从Promela语言的模型描述生成并规格由公式指定零担, C验证程序允许对规范进行自动形式化验证，特别是:

检查规范中指定的不变量; 如果不变量不满足，请查找反例。

了解有关Promela generation的更多信息 AnyMath 阅读文章 Promela代在 AnyMath.

正式核实 AnyMath 基于对模型行为进行完整研究的想法。

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

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

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

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

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

可用变量（全局和局部）; *状态和过渡的结构; *激活条件和块操作逻辑*图表; *计算过程和模型元素的相互作用。

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

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

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

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

如果属性结果为*true，那么这可以保证它在模型的所有可能场景中都是真实的。; 如果发现属性为*false，则需要进行额外的检查-通常是对反例的分析。

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

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

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

*错误是在设计阶段检测到的，而不是在测试的最后阶段。; *确保模型，其行为和形式属性之间的可追溯性; *验证成本降低，因为分析是自动执行的，不需要准备额外的测试场景。