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