形式化语言

Prover 提供了三种不同的语言，用于创建和表示形式化的需求规范和配置数据，即PiSPEC、HLL 和 LCF语言。 PiSPEC 是 Prover Trident 流程和 Prover iLock 工具中用于通用应用程序（设计、测试和安全要求）的语言，HLL 是一种更通用的建模和验证语言，是 PSL 和 Prover 认证器的输入语言，而 LCF 用于配置数据。

除了具有精确定义的语法和语义外，这些语言还经过精心设计，可以轻松表达信号要求和配置数据，还可以简化人工审核任务。后者对于 LCF 语言尤其重要，因为配置数据的审查，尤其是安全苛求数据，是许多铁路控制项目中的一项重要而常见的任务。 LCF 数据可由 Prover iLock 导入和导出，并转换为 HLL 形式以用于符合 CENELEC EN50128 的验证流程。