产品分类 更多>>
模拟仿真能够测试系统模型实现了我们所期望的功能，但并不能系统满足安全性要求。以电梯设计为例，“电梯在运行过程中门必须是关着的”就是安全性要求之一。由于测试的局限性，我们不可能通过模拟仿真来完全这样的安全性，对于复杂的逻辑控制系统来说尤是如此。形式验证这一功能弥补了这一局限性。
详尽的形式验证，不需要借助测试用例，就可以检验SCADE模型达到安全性。只需在SCADE中描述安全性要求，并设置一个“特性观察器”，用户按一个键就可验证SCADE模型的安全性。如果模型是安全的，它能给出一个安全的证明；如果模型是不安全的，它能给出一个反例帮助我们进行错误定位。形式验证很大程度上了目标系统的安全性。
SCADE同时还内置了两个形式验证的应用功能：除零检查和溢出检查，可以帮助用户快速定位可能的除零隐患和溢出危险。
公司网址：http://www.passiontechinc.com
