超级计算机监控系统的停机性验证
监控系统是保障超级计算机系统高可靠、高可用、高可维的关键组成部分.监控软件的可靠性直接关系到整个监控系统的可靠性.而通过对监控软件源代码进行形式化验证能够保证监控软件的正确性,从而进一步保障可靠性.停机性是软件正确运行需要保证的重要性质,结合不变式生成和线性秩函数模板,利用Farkas引理来生成约束系统,借助线性约束求解工具来得到合理的秩函数,从而验证软件的停机性.实验表明,某超级计算机监控软件中的绝大部分代码都能够通过停机性验证,为监控系统的可靠运行提供了保障.
监控软件 源代码 停机性验证 运行可靠性
邢建英 孙言强 张晓明 田宝华
湖南省长沙市国防科技大学计算机学院 410073
国内会议
贵阳
中文
665-670
2014-07-31（万方平台首次上网日期，不代表论文的发表时间）