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

　　首 先，让我们考察一下如何利用模型校验工具验证简单的嵌入式系统特性。为此，我们采用Carnegie-Mellon大学开发的符号模型验证器 (symbolic model verifier,SMV)作为模型校验工具。当然，我们也可以采用其他的模型校验工具描述该模型。文章结束部分列出了可选的模型校验工具及获取方式。

　　如 图2所示，一个简单的泵控系统通过泵P将源水槽A中的水传送至接收水槽B。每个水槽都具有两级刻度线：一个用来检测水位是否为空(Empty)，而另一个 用来检测水位是否已满(Full)。如果水槽的水位既不为空也不为满，那么水槽刻度线设定为ok;换言之，即水位高于空刻度线但低于满刻度线。

　　最 初，两个水槽均为空。一旦水槽A的水位值为ok(从空开始)，启动泵并假定水槽B尚未为满。只要水槽A不为空且水槽B不为满，泵将持续工作。一旦水槽A为 空或水槽B为满，泵将停止工作。一旦泵启动(或停止)，系统将不会尝试停止(或启动)泵。虽然这个示例非常简单，但可以很容易地扩展为控制多个源水槽和接 收水槽的复杂泵管线网络控制器，如应用在水处理系统或化工厂中的控制器。

　　表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结构还必须进一步扩展为无限树形结构，其中树形结构的每个分支都表征了系统可能的执行操 作或行为。