技术中心
 
 

抽象解释检查软件错误

   日期: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的质量要求,同时得到政府机构的认可。
抽象解释方案根据分…如图1
 
  
  
  
  
 
更多>同类技术
 
全年征稿 / 资讯合作