软件学报

作者：王淑灵，詹博华，盛欢欢，吴昊，易士程，王令泰，金翔宇，薛白，李静辉，向霜晴，向展，毛碧飞

单位：王淑灵，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004911,詹博华，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004902,盛欢欢，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004903,吴昊，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004904,易士程，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004905,王令泰，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004906,金翔宇，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004907,薛白，计算机科学国家重点实验室(中国科学院 软件研究所), 北京 100190;中国科学院大学, 北京 10004908,李静辉，华为技术有限公司 可信理论研究室, 广东 深圳 51812909,向霜晴，华为技术有限公司 可信理论研究室, 广东 深圳 518129010,向展，华为技术有限公司 可信理论研究室, 广东 深圳 518129011,毛碧飞，华为技术有限公司 可信理论研究室, 广东 深圳 518129012

关键词：可信系统;形式化方法;性质分类;验证方法和工具

基金：国家自然科学基金(61972385,62032024,61836005)

计算机系统被应用于各种重要领域,这些系统的失效可能会带来重大灾难.不同应用领域的系统对于可信性具有不同的要求,如何建立高质量的可信计算机系统,是这些领域共同面临的巨大挑战.近年来,具有严格数学基础的形式化方法已经被公认为开发高可靠软硬件系统的有效方法.目标是对形式化方法在不同系统的应用进行不同维度的分类,以更好地支撑可信软硬件系统的设计.首先从系统的特征出发,考虑6种系统特征:顺序系统、反应式系统、并发与通信系统、实时系统、概率随机系统以及混成系统.同时,这些系统又运行在众多应用场景,分别具有各自的需求.考虑4种应用场景:硬件系统、通信协议、信息流以及人工智能系统.对于以上的每个类别,介绍和总结其形式建模、性质描述以及验证方法与工具.这将允许形式化方法的使用者对不同的系统和应用场景,能够更准确地选择恰当的建模、验证技术与工具,帮助设计人员开发更加可靠的系统.

来源：2022年第7期

《软件学报》期刊编辑部

查看软件学报杂志2022年第7期