形式验证
什么是形式验证
形式验证是一种检查系统是否100％确定地满足所选属性的技术。例如，对于铁路信号系统，可以检查信号不能显示绿灯，除非某些道岔已在正确位置。
虽然大型系统的测试永远无法达到全面覆盖，但由于必须测试的变量组合数量众多，而形式验证可提供充分的确定性，因为它使用了无缝对接的数学证明。
现在，一些铁路系统运营商需要进行形式验证，以作为安全评估的一部分。即使不强制需要，供应商现在也会选择进行形式验证，因为安全性大大提高，并且可以通过自动化验证技术发现问题来减少测试负担。
Prover能为您提供什么
Prover在基于继电器的联锁，基于计算机的联锁（如Siemens Westrace，Ansaldo Microlok，Alstom iVPI，GE ElectroLogiXS，基于SCADE的设计等），CBTC系统，ETCS系统，微处理器，汽车嵌入式系统等等领域的形式化验证技术方面已有近30年的积累。
Prover提供产品，培训和支持，以便您建立自己的团队和流程进行形式验证。我们将在这个过程中为您提供支持，并且如果需要专家服务，我们将一直为您提供支持。
或者如果您愿意，我们的专业服务团队可以根据您的需求对您的系统进行量身定制的形式验证，然后会向您报告任何违反安全需求的行为以及原因。
Prover的产品
Prover的形式验证产品系列广泛且不断发展，已超越了行业标准。查看我们最新产品的以下列表，看看您有对那些产品和服务好奇：
- Prover iLock: 铁路联锁模拟器，文档和代码生成器，以及验证器
- Prover Certifier: CENELEC SIL-4可认证的安全证据生成器
- PSL: 能够形式验证大型工业系统的模型检验器
- Prover Extractor: 从Microstation图纸创建和验证数据库
- Prover Trident: 完整的工艺和工具套件，用于联锁设计自动化