证明嵌入式系统设计的UML-B规约

本书介绍了贯穿整个模块系统设计方法论的系统性质形式证法。该方法沦将子系统的共同验证与虚拟系统部件的系统精化和复用性相结合，通过规约的形式与非形式方法相结合，由UML和B语言来完成。这样就允许通过经证明的子系统的合成来验证系统规约（对于接口则给予某些特别的注意，符合VSIA／SLIF方法）。将B语言与C、VHDL和SystemC语言相连。将通过构造校正设计的过程扩展到较低的单片系统开发阶段。因此证明嵌入式软件产品是与证明硬件产品相配套的。书中开发了用于从UML和B语言产生代码的原型工具，现有的B语言验证工具被拓展成支持IP的再使用，这部是根据VSIA的推荐。书中所涉及的方法论及工具是通过开发三个工业应用来验证的，即无线移动终端、建立在HIPERLAN／2协议基础上的电信单片系统、以及汽车的防碰撞组件。