证明嵌入式系统设计规约证明(AB)=BA Jean P. Mermet, KeesDA S.A., France (Ed.) UML-B Specification for Proven Embedded Systems Design 2021, 300pp. Hardcover $ 1200 ISBN 1-4020-2866-0 Kluwer Academic Publishers 本书介绍了贯穿整个模块系统设计方法论的系统性质形式证法。该方法论将子系统的共同验证与虚拟系统部件的系统精化和复用性相结合，通过规约的形式与非形式方法相结合，由 UML 和 B 语言来完成。这样就允许通过经证明的子系统的合成来验证系统规约（对于接口则给予某些特别的注意，符合 VSIA/SLIF 方法）。将 B 语言与 C、VHDL 和 SystemC 语言相连，将通过构造校正设计的过程扩展到较低的单片系统开发阶段。因此证明嵌入式软件产品是与证明硬件产品相配套的。书中开发了用于从 UML
