推荐国家自然科学奖项目公示项目名称程序验证的基础理论研究.pdf

推荐国家自然科学奖项目公示 项目名称 程序验证的基础理论研究 推荐单位 教育部 推荐单位意见： 我单位认真审阅了该项目公示材料，确认全部材料真实有效，相关栏目均符合国 家自然科学奖材料的填写要求。 该项目建立了投影时序逻辑的模型理论和公理系统；提出了多核并发程序形式化 模型，即柱面计算模型；解决了命题区间时序逻辑的判定难题；建立了基于区间的时 序逻辑的复杂性和表达性理论。提出了集建模、仿真和验证为一体的并行程序设计语 言MSVL的形式化语义，包括模型、操作和公理语义；建立了基于MSVL的统一验证理 论，并开发了相应的支持工具。提出了高效的抽象模型检测、针对网络系统的状态空 间缩减理论和分布式网络的验证算法，有效缓解了网络系统模型检测中的状态空间爆 炸问题，提高了验证效率。项目成果得到了国内外同行专家的引用和好评，获得2015 年度教育部自然科学一等奖。 该项目选题准确，理论上有创新，有重要的学术价值和理论意义，对学科建设和 经济社会发展有重要的指导作用。 对照国家自然科学奖授奖条件，推荐该项目申报 2017年国家自然科学奖一等奖。 项目简介： 如何保障软件系统的正确性和可靠性是计算机软件领域面临的重要挑战。图灵奖 获得者 Clarke 等人提出的模型检测方法是迄今为止最成功的自动化程序验证方法之 一。程序性质的描述、模型的提取以及检测算法是模型检测的三要素，但是在这三方 面均存在一些亟待解决的问题：（1）性质描述语言表达能力不足；（2）系统模型难以 提取；（3）状态空间爆炸。针对这些问题，本项目提出了一套基于时序逻辑的程序验 证理论：用命题投影时序逻辑（PPTL）描述系统的性质，用投影时序逻辑统一验证技 术使得系统和模型的描述在同一逻辑体系，用高效的抽象模型检测方法缩减状态空间， 从三个方面克服程序验证的三个问题。具体创新点如下： 1、建立了投影时序逻辑 PTL 的模型理论，严格定义了 PTL 和 PPTL 的语法和语 义，提出并证明了该逻辑的 182个定理和 536个逻辑规则；建立了 PTL和 PPTL的公 理系统，并证明了其合理性和完备性；解决了 PPTL和基于区间的命题时序逻辑 PITL 的判定问题；证明了基于区间的时序逻辑的非初等复杂性及 PPTL 的完全正则表达能 力；提出了多核并发程序形式化模型，即柱面计算模型。 2、提出了以投影时序逻辑 PTL可执行子集为基础的集建模、仿真和验证为一体的 并行程序设计语言MSVL，给出了MSVL的最小模型、操作和公理语义；解决了时序 逻辑面向实际程序设计中的框架难题；建立了基于 MSVL的统一验证理论，使得程序 模型和性质的描述在同一逻辑体系，避免了程序验证中模型提取的困难。 3、提出了多项式抽象模型精化算法，避免了图灵奖获得者 Clarke等人提出的精化 方法中的指数爆炸；提出了线性虚假路径检测算法，缩减了图灵奖获得者 Clarke 等人 提出的虚假反例路径检测的时间复杂度；提出了高效的网络系统模型状态空间缩减方 法和分布式网络的验证算法，有效缓解了网络系统模型检测中的状态空间爆炸问题， 提高了验证效率。 客观评价： 英国 Kent大学著名学者 Bowman和 Thompson教授、加拿大滑铁卢大学 Peter R. King和 Helen Cameron教授对项目关于投影时序逻辑方面的贡献做了大段评论，他们 指出段在以下方面发展了 ITL：（1）提出了过去操作，（2）定义了新的投影操作符，（3） 研究了框架技术，（4）引入了无穷模型，（5）实现了并发和通信原语。项目在区间时 序逻辑（ITL）理论方面所做的工作，得到了 ITL的创始人 Ben Moszkowski的引用好 评。他指出本项目提出了命题投影时序逻辑在无穷区间的判定过程，研究了命题时序 逻辑的理论和应用，它是 ITL的扩展，有时序粒度和框架操作符。图灵奖获得者 Pnueli 曾指出现有的时序逻辑因仅限于全局的、非模块化的和非组合的系统验证而倍受指责。 而 Moszkowski 指出本项目提出的投影时序逻辑支持过去操作，因此可以支持 Pnueli 期望的模块化分析方法。美国科学院院士Moshe Y. Vardi等人指出段等人提出了 PPTL 的范式和范式图，其中 PPTL 是 LTL 的超集；他们给出了可用于 PPTL模型检测和可 满足性检测的判定过程。西班牙巴斯克大学 Jose Gaintzarain和 Paqui Lucio指出段等人 将 Tempura 方法扩展到框架 Tempura 和投影时序逻辑程序设计。德国马克斯普朗克计 算机科学研究所 Katja Hose 和挪威科技大学 Akrivi Vlachou