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

发布时间：2021-08-27 19:28:43 浏览数：次

　Jean P. Mermet, KeesDA S.A., France

　 (Ed.)

　 UML-B Specification for

　 Proven Embedded Systems

　Design

　2004, 300pp.

　Hardcover $ 1200

　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)

相关热词搜索：证明规约 嵌入式系统