形式化验证
什么是形式化验证
形式化验证是一种检查系统是否 100% 确定地满足选定属性的技术。例如，对一个铁路控制系统来说，我们需要检测并确保绿色信号灯不能随意开启，除非某些道岔已处于正确位置。
对于大型系统的测试永远无法达到完全覆盖，因为需要测试的组合数量过于庞大，而形式验证可提供充分的确定性，因为它使用了无缝对接的数学证明。
现在，一些铁路系统运营商需要进行形式化验证，以作为安全评估的一部分。即使这一过程并不被强制要求，现在许多供应商也会主动选择进行形式化验证，因为它可以大幅提高安全性，并且它还可以通过自动化验证技术发现问题，进而减少测试负担。
Prover能为您提供什么？
Prover的形式化验证技术已经在众多领域积累了将近30年的经验，这些领域包括基于继电器的联锁，基于计算机的联锁（如Siemens Westrace，Ansaldo Microlok，Alstom iVPI，GE ElectroLogiXS，基于SCADE的设计等），CBTC系统，ETCS系统，微处理器，汽车嵌入式系统等等。
Prover通过提供产品、培训和支持，协助您建立自己的团队和流程，以开展形式化验证。我们将从始至终为您服务，如果您需要专家支持，我们也将一直为您提供。
如果您需要，我们的专业服务团队可以根据您的需求，对您的系统设计量身定制的形式化验证，进而向您报告任何违反安全要求的行为以及原因。
Prover的产品
Prover的形式化验证产品系列广泛且持续发展，并且已经超越行业标准。查看我们的最新产品列表，看看您有对哪些产品和服务感兴趣：
- Prover iLock®：铁路联锁模拟器、文档和代码生成器，以及验证器
- Prover 认证器：符合CENELEC SIL-4 认证的安全证据生成器
- PSL：能够形式化验证大型工业系统的模型检查器
- Prover Extractor：从 Microstation 图纸创建和验证数据库
- Prover Trident®：用于联锁设计自动化的完整流程和工具链
SCADE FV：以CENELEC SIL-4 标准，形式化验证用 SCADE 构建的系统
- LCF：为信号工程量身定制的特定领域语言
- PiSPEC®：用于信号工程的形式化语言
- HLL：高级形式化语言，包括谓词逻辑并支持重要的常见编程功能，如数组和数字
关于形式化验证的更多内容
为什么进行形式验证-验证问题的解决方案
如果您已经阅读了本系列的前两部分，那么您将知道，验证联锁满足安全要求并不是一件容易的事。由于联锁的状态空间很大，因此手动方法和测试都无法助您一臂之力。
形式化验证Why系列之二：形式化验证的适用性
“形式化”其实就是指“数学”。因此，形式验证意味着将验证问题转化为数学问题。大家都知道一旦连结到数学领域，我们就可以获得数学所带来的严谨性和精确性。
形式化验证Why系列之一：铁路系统的安全需求
我将尝试解释为什么形式化验证是更好的选择。尤其是为什么在验证铁路系统的安全需求时使用形式化验证是一种好的做法。 为了做出令人信服的论证，我需要从头开始。
信号设计自动化论坛2019年会总结
11月6日，Prover在上海主办了2019年信号设计自动化论坛。 我们的主旨是召集铁路信号行业以及相关安全关键行业的专业人士，共享和讨论设计自动化的最新进展，使用软件技术实现铁路信号系统的自动化设计和验证，并特别地关注了通过形式验证保证安全。
保存日期 – SDA论坛将于2019年11月6日在北京举行
2017年，Prover Technology公司萌生了技术论坛的想法，我们希望创建一个分享经验和最佳实践以及相互沟通的论坛。 我们的目的是聚集来自世界各地领先的信号管理同行，并讨论自动化铁路信号系统的设计和验证中设计自动化和形式验证软件技术的最新发展，所以SDA论坛诞生了。 第一次会议由Prover公司于2017年5月15日在斯德哥尔摩主办。