Prover Studio

形式化规范的集成开发环境

关于 Prover Studio

Prover Trident 流程的一个关键要素是通用应用程序，它使用 PiSPEC 和 LCF 语言，将铁路控制应用程序的信号要求形式化。 Prover Studio 是与 Prover iLock 工具集成的开发环境，可帮助您管理、开发和维护这些形式化规范。

prover studio

优势

Prover Studio基于 Visual Studio Code，提供了所有预期的功能，例如语法突出显示、自动完成、语法和语义错误报告以及查找定义和引用的快捷方式。 Prover Studio用于在开发通用应用程序时编辑和跟踪 PiSPEC 及 LCF 源文件，同时 Prover iLock 用于测试和验证特定应用程序配置的规范，支持灵活和测试驱动的开发过程。