一、简介

      Scavel PLC 工具(简称)，是系统可信性自动验证国家地方联合工程实验室在系统可信性验证相关理论与技术方面积累大量原创性研究成果的基础上，开发的以形式化和自动推理为核心技术的自主可控工具。

二、功能

      (1)验证 PLC程序中结构化文本(ST)程序;

      (2)验证数组越界、数据溢出、除数为零、非数字等问题;

三、特点

      在不修改、不运行源程序的情况下，以静态方式验证程序运行时错误(Run-Time Errors)对比基于静态分析的测试工具其优势是源代码中的变量动态变化,对比动态测试工具的优势是不需要搭建测试环境、运行源码和构建测试例，并保证遍历所有可能执行路径以证明源代码的正确性。

四、适用性

      (1)IEC61131-3 标准基于 ST的 PLC 程序;

      (2)支持 GE、Simens、Infoteam OpenPCS 等平台。