Esterel Technologies>Products>SCADE Suite>SCADE Suite 的添加模块>SCADE Suite设计验证器

SCADE Suite设计验证器

SCADE设计验证器是SCADE工具中一个强大的形式化证明引擎。设计验证器(DV)使用的形式化方法使初学者也能感受到其高效率,这是因为形式化验证功能囊括在SCADE中,使用者无须学习新的语言或工具就可以使用这一尖端技术。

设计验证器用来验证SCADE的设计属性,它可以为你证明一项设计在满足它需求的情况下是安全的。DV可以证明“不好”永远不会发生,它在软件调试中起着指导性的作用。例如,它可以被验证在同样的需求下,两个设计是完全相同的。DV可以被用在一个完整的模型上,甚至还可以被用在简单的SCADE运算符上。这将使你在设计周期内尽早发现问题。全面的验证能力能帮助设计者找到那些其他测试方法不易被测试到的问题。

Report for a falsifiable property

验证属性出错

  • 最新模型验证技术的透明组合
  • 使用SCADE模块来验证安全、可信等其他属性:客户用SCADE节点做的设计在几秒中内即可被验证
  • 万一属性验证出错,将自动生成反例
  • 使用DV不需要理论背景

* 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

© 2012 Esterel Technologies, Inc. All rights reserved.