现在,计算机和软件比以往任何时候都更加重要。在汽车、飞机和医疗设备等系统中,执行没有重大缺陷或“故障”(bug)的软件非常重要。据外媒报道,荷兰埃因霍温理工大学(Eindhoven University of Technology)在读博士生Thomas Neele基于模型检查法研发了三种技术,以更智能、更快速地检查软件故障。
Thomas Neele(图片来源:埃因霍温理工大学)
模型检查是最严格的软件检查技术之一,可以检查一个软件系统所能完成的所有事情,其能够处于的“状态”以及检查是否其能够按要求工作。软件常常由许多可以并行工作的部分组成,这可能导致需要检查的部分的数量激增,导致检查模型成本高昂,甚至可能最终导致无法进行管理。Neele探索了新方法,通过减少需要检查的部分的数量,以解决该问题。
Neele研发的三项技术有一个共同点:会考虑到软件系统状态的要求,这条额外的信息使其更容易了解到哪部分不需要检查。为了能够同时观察系统的行为和要求,Neele首先新研发了一种结构化的方法,以展示行为与要求相结合的信息。
第一项技术通过将相似的状态组在一起减少了所需要检查的状态的数量,甚至可以处理无穷数量的状态。第二项技术可以检查可以并行工作的软件部分是否有时在独立执行任务。在此种情况下,没有必要检查所有可能的状态。最后一种技术可以检查某些元素是否有相关性,如果不相关则将其删除。
未来,上述想法将有助于减少研发成本,缩短安全关键软件的上市时间,让高科技医疗服务更便宜,从而让更多人可以享受此种服务。此外,Neele的技术还可以帮助从飞机、汽车等系统中清除危险的故障。目前,应用Neele的想法和模型检查法需要大量的专业知识。为了让其技术得以大规模采用,有必要研发一种全自动化系统,以决定哪种方法最适用于某一特定应用。