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

1580 Journal of Software 软件学报 Vol.32, No.6, June 2021

《基于锁增广分段图的多线程程序死锁检测》对已有的锁图和分段图模型进行改进,提出一种新的死锁检
测方法,该方法能有效消除各种误报,提高死锁检测的准确率.
《基于污染变量关系图的 Android 应用污点分析工具》提出了一种基于污染变量关系图的污点分析方法,
并描述了基于该方法所实现的工具 FastDroid 的架构、模块及算法细节.
《以太坊中间语言的可执行语义》对以太坊中间语言 Yul 进行形式化,利用 Isabelle/HOL 证明辅助工具给
出了其类型系统和小步操作语义的形式化定义,为智能合约正确性、安全性验证奠定了基础.
《个体交互行为的平滑干预模型》提出一种基于个体交互行为系统平滑干预模型,能够很好地引导用户行
为平滑变化,且产生足够的区分性使得行为伪装异常检测场景下模型的准确性显著提高.
《支持乱序执行的 Raft 协议》使用 TLA+为分布式共识协议 ParallelRaft 提供严格的形式化规约,并证明
了在参与者数量较小的情形下算法的正确性.
《面向 CPS 时空性质验证的混成 AADL 建模与模型转换方法》提出了面向 CPS 时空性质验证的混成
AADL 建模与模型转换方法,并通过一个飞机避撞系统实例验证该方法的有效性.
《芯片开发功能验证的形式化方法》提出了一种新型验证设计模型和生成代码一致性的方法.该方法利用
MSVL 语言进行系统建模,通过统一模型检测的原理,验证模型是否满足性质的有效性.
《面向数据流的 ROS2 数据分发服务形式建模与分析》采用概率模型检验的方法,分析、验证机器人操作
系统 ROS2 系统数据分发机制的实时性和可靠性.
《Ptolemy 离散事件模型形式化验证方法》提出了一种基于形式模型转换的方法来验证离散事件模型的
正确性,通过在 Ptolemy 环境中实现一个插件,可以自动将离散事件模型转换为时间自动机模型,并通过调用
Uppaal 验证内核完成验证.
《面向 MSVL 的智能合约形式化验证》介绍了如何使用建模、仿真与验证语言(MSVL)和命题投影时序
逻辑(PPTL)对智能合约进行建模和验证.
《面向 ROS 的差分模糊测试方法》提出了一种差分模糊测试方法对机器人操作系统 ROS 不同版本的功
能包进行测试,找出其中的漏洞.
《基于 Coq 的分块矩阵运算的形式化》完善了基于 Coq 记录类型的矩阵形式化方法,其中包括提出新的
矩阵等价定义、并证明了一组新的引理,最终实现了矩阵与分块矩阵形式化的不同类型的基础库.
本专题重点关注形式化基础方法、技术、支持工具以及领域交叉应用,反映了我国学者在该领域的最新研
究进展.感谢《软件学报》编委会、CCF 形式化方法专委会对专题工作的指导和帮助,感谢编辑部各位老师从
征稿启示发布、审稿专家邀请至评审意见汇总、论文修改、定稿及出版所付出的辛勤工作,感谢专题全体评审
专家及时、耐心、细致的评审工作,感谢踊跃投稿的所有作者对《软件学报》的信任.希望本专题能够对形式
化方法的科研工作有所促进.

田聪(1981－),女,博士,西安电子科技大学 姜宇(1989－),男,博士,清华大学软件学院
计算机科学与技术学院教授,博士生导 副教授,博士生导师,CCF 会员,主要研究
师,CCF 杰出会员,主要研究领域为形式化 领域为 形式化 方法 , 程 序分析 , 嵌入式
方法,程序验证,等. 软件,等.

邓玉欣(1978－),男,博士,华东师范大学软
件工程学院教授,博士生导师,CCF 高级会
员 , 主要 研究 领域 为 形 式 化方法 , 程序
理论,等.