抽象解释检查软件错误

发布时间：2005-02-26

　　Invensys Triconex的Trident TMR控制器
　　Invensys Triconex在其推出的TMR控制器系统内采用了抽象解释(abstract interpretation)方法。该系统能对炼油厂、石油化工厂、化工厂和其他工业生产过程中安全生产最至关重要的装置进行连续控制。据该公司介绍，他们在容错控制器软件验证中使用抽象解释方法长达一年时间，已节省了1百万美元，该软件用于对可靠性和可用性要求很高的过程应用。
　　Trident控制器是通过一个三重模块化冗余（TMR）结构提供容错的，它将3个孤立的并行控制系统集成在一起，开展诊断。新产品出厂前需要接受测试，这对一个系统来说是极具挑战性的任务。例如，该系统可能有大约 70,000 行C代码和 140,000 行Ada代码，而且在硬实时中按一式三份模式运行，因此如果特定的安全条件不符合要求时，它能很快使装置停止运行，反应时间是毫秒级。
　　Triconex公司介绍说，这当中的挑战是查出运行时出现的错误，例如处理器中断运行、数据遭到破坏、定时选择无法进行等。这样一个产品的一套完整的“白箱”测试能够毫不费力地花费4或5个人一年的工作量，时间跨度为6到12个月，才能满足Invensys的质量要求，同时得到政府机构的认可。

　　抽象解释方案根据分析软件的动态特性，对其进行抽象认证。Triconex使用的验证器是由PolySpace Technologies提供的。这是一种抽象解释工具，在某时根据代码的动态性对其进行评价，从而减少了计算负荷。这种方法对软件验证的好处是，它能百分之一百地自动发现运行时出现的错误，而且所花时间不多，并且取代了以往测试代码所用的传统验证方法。
　　www.triconex.com和www.polyspace.com
　　· 用于安全和关键过程控制应用的三重模块化冗余控制器
　　· 可用于恶劣的工业环境
　　· 允许在不干扰生产过程正常运行的情况下实现在线维护