实时嵌入式系统模型校验技术

启动)泵。虽然这个示例非常简单，但可以很容易地扩展为控制多个源水槽和接 收水槽的复杂泵管线网络控制器，如应用在水处理系统或化工厂中的控制器。

表1：SMV模型描述和需求清单。

MODULE main

VAR

level_a : {Empty, ok, Full}; -- lower tank

level_b : {Empty, ok, Full}; -- upper tank

pump : {on, off};

ASSIGN

next(level_a) := case

level_a = Empty : {Empty, ok};

level_a = ok pump = off : {ok, Full};

level_a = ok pump = on : {ok, Empty, Full};

level_a = Full pump = off : Full;

level_a = Full pump = on : {ok, Full};

1 : {ok, Empty, Full};

esac;

next(level_b) := case

level_b = Empty pump = off : Empty;

level_b = Empty pump = on : {Empty, ok};

level_b = ok pump = off : {ok, Empty};

level_b = ok pump = on : {ok, Empty, Full};

level_b = Full pump = off : {ok, Full};

level_b = Full pump = on : {ok, Full};

1 : {ok, Empty, Full};

esac;

next(pump) := case

pump = off (level_a = ok | level_a = Full)

(level_b = Empty | level_b = ok) : on;

pump = on (level_a = Empty | level_b = Full) : off;

1 : pump; -- keep pump status as it is

esac;

INIT

(pump = off)

SPEC

-- pump if always off if ground tank is Empty or up tank is Full

-- AG AF (pump = off -> (level_a = Empty | level_b = Full))

-- it is always possible to reach a state when the up tank is ok or Full

AG (EF (level_b = ok | level_b = Full))

该系统的模型的SMV建模如表1所示。起始的VAR部分定义了系统的3个状态变量，变量level_a和level_b分别记录了上层水槽(upper tank)和下层水槽(lower

图3：泵控系统执行树的初始部分。

tank)的当前水位;在每个“时刻”，这两个变量都将分别赋值，取值范围为Empty、ok或Full。变量pump表征了泵的启动(on)和停止(off)。

系 统状态就可用上述3个变量的不同取值来表示。例如(level_a=Empty, level_b=ok, pump=off)和l (level_a=Empty, level_b=Full, pump=on)就可以表示系统状态。在靠近结尾的INIT部分，定义了这些变量的初始值(这里，最初假定pump的初始值为off，而其他两个变量则可 取任意值)。

ASSIGN部分定义了系统如何从一个状态迁移到另一个状态。每个next语句都规定了特定变量的取值变化。所 有这些赋值语句都假定可以并行执行;next语句定义为在该部分执行所有赋值语句后的最终结果。下层水槽的状态可以从Empty状态迁移到Empty或 ok状态;从ok状态迁移到Empty或Full状态，或保持为ok状态(如果pump的状态为on);从ok状态迁移到ok或Full状态(如果 pump的状态为off);如果pump状态为off，那么下层水槽在Full状态无法发生状态迁移;如果泵状态为on，则可迁移到ok或Full状态。 上层水槽也可规定类似的操作。

在系统内部，大多数模型校验工具通常会将输入模型扩展为具有Kripke结构的动态系统。扩展 过程包括在EFSM中除去分层结构、并行成分以及状态迁移时的告警和操作。Kripke结构中的每个状态实际上都可用每个状态均赋值的元组(tuple) 来表示。Kripke结构中的状态迁移表征了一个或多个状态变量取值的变化;而且还可以比较通过扩展给定模型而得到的Kripke结构，对指定的系统属性 进行校验。然而，为了更好地理解每条属性语句的含义，Kripke结构还必须进一步扩展为无限树形结构，其中树形结构的每个分支都表征了系统可能的执行操 作或行为。路径和属性规范

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

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

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