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