证明嵌入式系统设计的ＵＭＬ－Ｂ规约|证明(AB)*=B*A*

　　Jean P. Mermet, KeesDA S.A., France 　　(Ed.) 　　UML-B Specification for 　　Proven Embedded Systems
　　Design
　　2004, 300pp.
　　Hardcover $ 129.00
　　ISBN 1-4020-2866-0
　　Kluwer Academic Publishers
　　
　　本书介绍了贯穿整个模块系统设计方法论的系统性质形式证法。该方法论将子系统的共同验证与虚拟系统部件的系统精化和复用性相结合，通过规约的形式与非形式方法相结合，由UML和B语言来完成。这样就允许通过经证明的子系统的合成来验证系统规约（对于接口则给予某些特别的注意，符合VSIA/SLIF方法）。将B语言与C、VHDL和SystemC语言相连，将通过构造校正设计的过程扩展到较低的单片系统开发阶段。因此证明嵌入式软件产品是与证明硬件产品相配套的。书中开发了用于从UML和B语言产生代码的原型工具，现有的B语言验证工具被拓展成支持IP的再使用，这都是根据VSIA的推荐。书中所涉及的方法论及工具是通过开发三个工业应用来验证的，即无线移动终端、建立在HIPERLAN/2协议基础上的电信单片系统、以及汽车的防碰撞组件。
　　全书共有17章。第1章形式方法介绍：它们是怎样应用于嵌入式系统设计的？第2章使用UML、B和SystemC的形式统一系统规约环境；第3章使用PUSSEE方法设计嵌入式系统；第4章借助事件B的系统层次建模与精化；第5章用于UML中形式系统建模的UML-B简况；第6章U2B―用于从UML-B模型转换到B语言的工具；第7章BHDL硬件描述语言；第8章用于UML对硬件描述语言映射的概念性框架；第9章B语言中基于接口的合成精化；第10章借助互补模型检验的有限状态机的精化；第11章适应漫游控制实例研究设计实验；第12章适就漫游控制器实例的研究；第13章使用事件B的电子线路形式建模；第14章回送注销单元实例研究；第15章可移动设计系统实验结果；第16章UML-B规约与汉明编码器/解码器的硬件实现；第17章实践中的PUSSEE方法。书后的附录A1：嵌入式系统设计方法的评估标准。
　　本书描述的问题有一定的难度，所获得的成果证明了该项目研究的成功，且视野广阔，因此受到欧洲专家的肯定。本书公布的形式方法现在已经能够应对工业中有难度的问题，便于设计工程师、大学教师和研究人员使用。
　　胡光华，高级软件工程师
　　(原中国科学院物理学研究所)
　　
　　Hu Guanghua, Senior Software Engineer
　　(Former Institute of Physics,the Chinese Academy of Sciences)