首先，让我们考察一下如何利用模型校验工具验证简单的嵌入式系统特性。为此，我们采用Carnegie-Mellon大学开发的符号模型验证器(symbolic model verifier,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))
参考文献
1. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA： MIT Press, 1999.
2. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification： Model-Checking Techniques and Tools, Berlin-Heidelberg： Springer Verlag, 2001.
3. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765.
4. Clarke, Edmund M., Orna Grumberg, and Doron A. Peled. Model Checking, Cambridge, MA： MIT Press, 1999.
5. Berard, Beatrice, Michel Bidoit, Alain Finkel, Francois Laroussinie, Antoine Petit, Laure Petrucci, Philippe Schnoebelen, and Pierre Mckenzie. Systems and Software Verification： Model-Checking Techniques and Tools, Berlin-Heidelberg： Springer Verlag, 2001.
6. Havelund, Klaus, Mike Lowry, and John Penix. "Formal Analysis of a Space-Craft Controller using SPIN," IEEE Transactions on Software Engineering, vol. 27, no. 8, Aug. 2001, pp. 749-765.
7. Harel, David, and Michal Politi. Modeling Reactive Systems with Statecharts—The Statemate Approach. New York, NY： McGraw-Hill, 1998.
