Page 5 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1579−1580 [doi: 10.13328/j.cnki.jos.006256] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
形式化方法与应用专题前言

3
2
1
田 聪 , 邓玉欣 , 姜 宇
1
(西安电子科技大学 计算机学院,陕西 西安 710071)
2 (华东师范大学 软件学院,上海 200062)
3 (清华大学 软件学院,北京 100084)
通讯作者: 田聪, 邓玉欣, 姜宇, E-mail: ctian@mail.xidian.edu.cn, yxdeng@sei.ecnu.edu.cn, jiangyu198964@126.com

中文引用格式: 田聪,邓玉欣,姜宇.形式化方法与应用专题前言.软件学报,2021,32(6):1579−1580. http://www.jos.org.cn/1000-
9825/6256.htm

计算机科学的发展主要涉及硬件和软件的发展,而软、硬件发展的核心问题之一是如何保证它们是安全可
靠的.如今,硬件性能变得越来越高,运算速度也越来越快,体系结构、软件的功能也更加复杂,如何开发可靠的
软、硬件系统,是计算机科学发展面临的巨大挑战.特别是现在计算机系统广泛应用于许多安全攸关系统中,如
高速列车控制系统、航空航天控制系统、医疗设备控制系统等等,这些系统中的错误可能导致灾难性后果.
形式化方法己经成功应用于各种硬件设计,特别是芯片的设计.各大硬件制造商都有一个非常强大的形式
化方法团队为保障系统的可靠性提供技术支持,例如 IBM、AMD 等等.近年来,随着形式验证技术和工具的发展,
特别是在程序验证中的成功应用,形式化方法在处理软件开发复杂性和提高软件可靠性方面已显示出无可取
代的潜力.各个著名的研究机构都投入了大量人力和物力从事这方面的研究.例如,美国宇航局(NASA)拥有的
形式化方法研究团队在保证美国航天器控制软件正确性方面发挥了巨大作用,在研发“好奇号”火星探测器时,
为了提高控制软件的可靠性和生产率,广泛使用了形式化方法.在新兴领域,如区块链及人工智能等领域,形式
化方法也逐步得到应用,提升系统的整体安全可控.
本专题公开征文,共征得投稿 27 篇.特约编辑先后邀请了国内外在该领域比较活跃的学者参与审稿工作,
每篇投稿至少邀请 2 位专家进行初审.大部分稿件经过初审和复审两轮评审,部分稿件经过了两轮复审.通过初
审的稿件还在 FMAC 2020 大会上进行了现场报告,作者现场回答了与会者的问题,并听取了与会者的修改建
议.最终有 18 篇论文入选本专题.
《C2P:基于 Pi 演算的协议 C 代码形式化抽象方法和工具》提出一种检测安全协议代码语义逻辑错误的形
式化验证方法,通过将协议 C 源码自动化抽象为 Pi 演算模型,基于 Pi 演算模型对协议安全属性进行形式化验证.
《大粒度 Pull Request 描述自动生成》利用图神经网络和强化学习的技术,提出一种为 GitHub 平台中大粒
度 Pull Request 自动生成描述的方法.
《Petri 网的反向展开及其在程序数据竞争检测的应用》针对安全 Petri 网的可覆盖性判定问题提出一种
目标导向的反向展开算法,并应用于并发程序中数据竞争检测问题的形式化验证.
《面向 SPARC 处理器架构的操作系统异常管理验证》提出了基于 Hoare-logic 的验证框架,用于证明面向
SPARC 处理器架构操作系统异常管理的正确性,基于该框架验证了我国北斗三号在轨实际应用的航天器嵌入
式实时操作系统 SpaceOS 异常管理功能的正确性.
《基于分支标记的数据流模型的代码生成方法》针对具有复杂分支组合的数据流模型提出了基于分支调
度标记的代码生成方法.
《面向 AADL 模型的存储资源约束可调度性分析》提出一种面向软件架构级别、基于抢占调度序列的缓
存相关抢占延迟计算方法,用来分析缓存相关抢占延迟约束下 AADL(架构分析和设计语言)模型的可调度性.

收稿时间: 2021-01-30