抽象解释检查软件错误

英维思Triconex在其Trident TMR控制器系统中使用抽象解释方法，该系统为炼油厂、石化和化工厂以及其他工业过程中的安全关键单元提供连续控制。该公司表示，抽象解释已经节省了100万美元和长达一年的时间来验证过程制造应用程序中使用的容错控制器软件，这些应用程序需要高水平的可靠性和可用性。

Trident通过三模块冗余(TMR)架构提供容错能力，该架构集成了三个隔离的并行控制系统和广泛的诊断。每次新产品发布前都需要进行测试，对于一个系统来说，测试是一项具有挑战性的任务，例如，可能有大约70,000行C代码，140,000行Ada代码，并且在硬实时情况下以三份方式运行，因此如果超过指定的安全界限，它可以在几毫秒内关闭工厂。

Triconex表示，这里的挑战是检测运行时错误，如处理器停止，数据损坏，时间违规等。这样一个产品的完整“白盒”测试很容易需要4到5个人年的努力，分散在6到12个月的时间里，以满足英维思的质量要求并获得政府机构的认证。

抽象解释方法是根据被分析软件的动态特性对其进行抽象。Triconex使用PolySpace Technologies的验证器。这是一种抽象的解释工具，它根据代码的动态属性一次性评估代码，从而减少了计算负载。这种软件验证方法的优点是，它可以在使用传统验证方法测试代码所需的一小部分时间内自动检查100%的运行时错误。www.triconex.com和www.polyspace.com

• 三模块冗余控制器适用于安全，关键过程控制应用

• 设计承受恶劣的工业环境

• 允许在线维护而不干扰过程

• 针对具有小到中等点数的关键应用程序进行了优化

您是否具有本内容中提到的主题的经验和专业知识?您应该考虑为我们的CFE媒体编辑团队做出贡献，并获得您和您的公司应得的认可。点击在这里开始这个过程。