基于有限状态机的嵌入式系统模型校验技术

路径和属性规范

最开始，系统可以处于9个状态中的任意一个，其中对于A和B的水位没有任何限制，而pump的初始状态假定为off。这样，我们就可以利用有序元组

这 些状态可以无限执行(或运算)树状结构的形式进行排列。如图3所示，树根为我们所选的初始状态，任意状态的分支均表示下一个可能的状态，而每个系统执行都 是执行树状结构的一条路径。总体上，系统可以具有无限多个这样的执行路径。模型校验的目标就是检验执行树状结构是否满足用户指定的属性要求。

现 在的问题在于，我们究竟该如何描述执行树状结构路径(及路径上的状态)的属性。从技术的角度看，运算树逻辑(Computation tree logic, CTL)是时序逻辑(time temporal logic, TTL)的一个分支，其简单性和直观性非常适合于本例。CTL是常用的布尔命题逻辑(Boolean propositional logic, BPL)的扩展，除了支持包括"和(and)"、"或(or)"、"否(not)"、"蕴涵(implies)"在内的BPL逻辑连接操作外，还支持辅助 的时序连接操作。表2所示为 CTL 中的某些连接操作。

表1和图4说明了CTL中一些基本时序连接操作的直观意义。一般地，E(就某个路径而言)和A(就所有的路径而言)表示从某个状态开始的路径数目。F(就某个状态而言)和G(就所有状态而言)表示某个路径中的状态数目。

图4：状态s0处满足CTL公式的直觉推导。

对 于指定的属性以及对应于系统模型的运算树T(可以是无限运算树)，模型校验算法可以通过校验T判断T是否满足该属性。例如，考虑指定的属性AF g，其中g表示与任何CTL连接无关的命题公式。图4b给出了运算树T的一个示例。如果属性AF g在根状态s0的值设定为true(即如果T中的每条路径中有状态开始于s0以使公式g为true)，那么对于该运算树TAF g的值为true。如果g在s0为true，那么就实现了预定目标，因为s0将会出现在从s0开始的每条路径中。但如果g在s0状态下不为true，由于 从s0开始的路径要么是s0的左分支，要么是s0的右分支，因此如果在运算树T中s0的两个分支都为true(通过递归校验)，那么该属性在s0处也为 true。

图4b显示，g在左分支根部为true(球体填充为黄色)。因此从s0到左分支单元的所有路径以及整个左分支树都 满足该属性。现在假定g在s0的右分支根部不为true;因此对于所有的子单元都将递归检验该属性。图4b显示，对于s0右分支的所有子单元，g都为 true(球体填充为黄色)，因此对于s0的右分支树该属性为true。这样，对于s0的所有子分支树该属性为true，从而s0也为true。

图4 归纳了类似的其他属性(例如EG g和AG g)校验原理。当然，实际应用中的模型校验算法远比这复杂;这些算法利用一些巧妙的简化手段对状态空间进行精简，从而避免了对那些确保为true的属性进 行校验。一些设计良好的模型校验器可用来校验状态数高达1,040个的状态空间的属性。在SMV中，待验证的属性可由SPEC部分的用户指定。逻辑连接 "否"、"或"、"和"和"if-then"可以分别用!、|、&和 ->表示。CTL时序连接则表示为AF、AG、EF、EG等。属性AF(pump=on)表示对于每条开始于初始状态的路径，路径中有一个pump =on的状态。在初始状态，该属性显然为false，因为从初始状态开始有一条路径pump的值始终为off(例如，当水槽A永远保持为空时)。如果希望 在SPEC部分中描述该属性，那么SMV将为该属性生成如下反例。循环表征了开始于初始状态的无限状态序列(换言之，即路径)，这样水槽B在该路径下的每 个状态均为Full，因此pump=off。
与严格的规范化语言相结合，可以下列执行序列表示：

state 1.1:
level_a = Full
level_b = Full
pump = off
state 1.2:

属性AF(pump=off)具有两重含义，表征的是对于每条开始于初始状态的路径，路径中有一个状态中pump=off。该属性当然在初始状态为true，因为初始状态本身(所有路径均包含初始状态)pump=off就成立。

表2：CTL中的一些时序连接。

时 序连接和逻辑连接相结合，可以得到一些有趣的复杂属性。属性AG((pump=off) -> AF (pump=on))表示如果pump=off，那么最终pump=on这种情形总会发生。初始状态，该属性显然为false。属性AG AF (pump=off -> (level_a=Empty " level_b=Full))表示如果底层水槽为Empty或上层水槽为Full，那么pump将总是为off。属性AG (EF (level_b= ok|level_b=Full))表示总是会出现上层水槽为ok或Full的情形。

　　实际应用中的模型校验

模型校验已被证明是对各类系统(尤其是硬件系统、实时嵌入式系统和安全临界系统)进行需求和设计验证的有效工具。例如，SPIN模型校验器曾用于验证NASA的深空1发射方案中的多线程规划执行模型并成功地发现了5个先前未知的并发缺陷。然而，实际使用模型校验时还需要注意下面一些主要问题：

1. 每种模型校验工具都采用特有的建模语言，这些建模语言一般都无法将不规范的需求描述自动转化为规范化语言。这样的转化显然需要手工完成，因此很难检验模型 是否正确地表示了建模系统。实际上，指定的建模表示法往往很难甚至根本不可能对部分系统需求进行建模。2. 专用工具属性规范表示法也存在类似的问题，属性表示法通常可以是CTL、CTL*或命题线性时序逻辑(PLTL)的变形。某些需要验证的属性很难甚至根本 不可能用该表示法进行描述。3. 模型系统中的状态数量也可能极为庞大。尽管模型校验算法可以利用一些技巧减小状态空间的复杂度，但模型校验器仍然需要很长的时间才能验证一个指定的属性或 者决定"放弃"验证该属性。这时，用户将不得不投入更大的精力，独立验证模型的各部分或者通过减小变量的取值范围以达到简化状态空间的目的。

尽管如此，模型校验仍被证明是无与伦比的系统需求或设计验证工具。该工具能在需求或设计的早期阶段发现瑕疵，因此能极大地节省后续的开发时间。