控制与信号应用的说明、编码、模拟及形式验证
Prover是一种基于PiSPEC 和 Prover iLock解决方案的程序。该程序涵盖控制和信号应用的说明、编码、模拟以及形式验证。下图说明了与传统的非形式程序相比，Prover程序在工程方面节约的程度。要想创建PiSPEC数据库，需要先期投入，但数据库创建完后，便可实现工程的高度自动化。结果：成本明显降低。
图表所示的直接成本来自于收集信号技术以及利用清晰、正式且经过验证的PiSPEC语言获取该技能的花费。这促使工程师将现有信号文件中信号的歧义和矛盾的问题一次性彻底解决。这反过来有助于节约宝贵的工程资源，确保要求清晰明确，并在适当的时候实现高度自动化应用。人会离去或退休，但PiSPEC数据库却得以保留，确保了新员工可以快速、熟练地应用。
下图概述了开发的过程，并将开发过程的每一步具体化。
第一步： 利用PiSPEC语言的安全和测试规范
- 改善运营商-供应商之间的沟通
- 明确、正式的形式设计要求
应用工程程序的第一步就是要说明要求。控制和信号系统有两类逻辑要求。
- 测试要求：根据输入及期望输出编制测试方案
- 安全要求：严禁或不安全的情况
在这些要求未被明确说明前，工程师不能设计优质应用。按照传统程序，这些要求可划为两类：明确的要求和含蓄的要求。其中，明确的要求可以通过多种非形式的自然语言文件获知。这些文件通常不一致，且含糊不清。含蓄的要求是不被归档的，是一个组织内局部的“群体知识”。 这些要求通常会因询问的对象不同而有所差异。结果：项目出现的结果不一致，成本超出预算，不能满足（不确定的）顾客预期。
该问题通过使用 PiSPEC创建一般测试和安全说明可以得到解决。 然后将一般测试和安全说明提供给负责应用设计的工程师，并确保设计程序从一开始就符合明确的要求。
第二步： 利用PiSPEC进行设计说明
- 通用的设计说明详情应明确并采用硬件独立格式。
- 参考说明可以确保应用实施的一致性。
PiSPEC也可在通用设计说明中详细说明设计和实施的具体细节。 该通用设计说明使供应商可自动进行编码。这反过来可以确保应用编码完全一致，免受个人系统、结构以及命名偏好的困扰。
第三步： 利用Prover iLock进行编码和模拟
- 较传统方法，可降低编码所用时间的95%以上。
- 编码完全一致 。
一旦编码规则为设计说明获知，就不必采用手工方式书写编码。 应用工程师可利用Prover iLock生成编码。该过程不但迅速，而且精确。所有的工程师只需利用Prover iLock绘制一个线路平面图，设定一些参数，该工具便可生成并模拟应用的编码。
第四步： 利用Prover iLock进行安全验证
- 并不是只有在测试场景中明确说明的应用才是安全的。相反，应用的每个可能环节都是安全的。
- 即便是CENELEC SIL-4 系统，那些不安全、高成本和耗时的安全测试，也全部被排除。
测试方法适用于创建符合预期操作场景的系统，但不适用于安全验证。该方法不完整，因此，很可能有定义错误的风险。另一方面，采用形式的安全验证方法，应用编码无论在哪个方案也不会出现不安全或禁止的现象。这排除了不安全的逻辑。鉴于此，权威机构（如CENELEC）强烈建议使用形式验证，几家主要运营商也要求使用该验证。
Prover iLock 验证器选出引起应用编码出现不安全/禁止现象的输入方案，并将其利用图像显现出来，从而确保您能够在收费服务前，检查并处理好可能会引起意外的逻辑问题。
