主页>产品介绍>SCADE Suite>设计验证

使用设计验证器可以确保设计的正确性*

SCADE验证器是SCADE工具附带的强大形式验证工具。设计验证器 Design Verifier (DV) 采用了形式化方法学,即使是初次使用者也能非常有效的使用它。因为SCADE自带了形式验证的功能,所以设计者无需为了掌握这一复杂而先进的技术再去学习一门新的语言或工具。

设计验证器用于证明SCADE设计的一些安全性特征,你可以证明设计和需求的一致性。DV对于软件调试来说是一个很大的帮助。例如, 它可以用于证明根据同一个需求完成的两个设计是否是一致的。具体选择使用DV的尺度掌握在用户手中,我们的目标可能是一个完整的模型,也可能是一个节点,甚至是节点的一部分。从而使用户在设计周期里可以较早的发现bug,其彻底的验证能力可以令设计者找到那些普通测试方法无法发现的bug

Report for a falsifiable property

验证结果为假

  • 最新的模型验证技术的完美结合
  • SCADE模块的安全性、可靠性、可信度以及其他特性进行验证:数秒内完成对大量SCADE节点的验证,真正实现的用户自己的设计
  • 不满足安全性特征时,自动生成反例
  • 使用形式验证不需要任何技术背景

* SCADE Design Verifier is based on the Prover Plug-In. Prover Plug-In is a trademark of Prover Technology AB in Sweden, the United States and in other countries.

Prover Plugged-in

© 1999–2008 Esterel Technologies, Inc. All rights reserved.