《证实嵌入式系统设计的ＵＭＬ－Ｂ规约-证实(AB)-=B-A-》由会员分享，可在线阅读，更多相关《证实嵌入式系统设计的ＵＭＬ－Ｂ规约-证实(AB)-=B-A-（2页珍藏版）》请在金锄头文库上搜索。
1、证实嵌入式系统设计的规约|证实(AB)*=B*A* Jean P. Mermet, KeesDA , France UML-B Specification for Proven Embedded SystemsDesign2021, 300pp.Hardcover $ISBN 1-4020-2866-0Kluwer Academic Publishers本书介绍了贯穿整个模块系统设计方法论的系统性质形式证法。该方法论将子系统的共同验证和虚拟系统部件的系统精化和复用性相结合，经过规约的形式和非形式方法相结合，由UML和B语言来完成。这么就许可经过经证实的子系统的合成来验证系统规约。将B语言和C、
2、VHDL和SystemC语言相连，将经过结构校正设计的过程扩展到较低的单片系统开发阶段。所以证实嵌入式软件产品是和证实硬件产品相配套的。书中开发了用于从UML和B语言产生代码的原型工具，现有的B语言验证工具被拓展成支持IP的再使用，这全部是依据VSIA的推荐。书中所包括的方法论及工具是经过开发三个工业应用来验证的，即无线移动终端、建立在HIPERLAN/2协议基础上的电信单片系统、和汽车的防碰撞组件。全书共有17章。第1章形式方法介绍：它们是怎样应用于嵌入式系统设计的？第2章使用UML、B和SystemC的形式统一系统规约环境；第3章使用PUSSEE方法设计嵌入式系统；第4章借助事件B的系统层
3、次建模和精化；第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
