超级计算机监控系统的停机性验证

摘要

监控系统是保障超级计算机系统高可靠、高可用、高可维的关键组成部分.监控软件的可靠性直接关系到整个监控系统的可靠性.而通过对监控软件源代码进行形式化验证能够保证监控软件的正确性,从而进一步保障可靠性.停机性是软件正确运行需要保证的重要性质,结合不变式生成和线性秩函数模板,利用Farkas引理来生成约束系统,借助线性约束求解工具来得到合理的秩函数,从而验证软件的停机性.实验表明,某超级计算机监控软件中的绝大部分代码都能够通过停机性验证,为监控系统的可靠运行提供了保障.