微信服务号
微信订阅号
2023年第7期专题优先出版：形式化方法与应用(董云卫,刘关俊,毛晓光)
- 分享：
形式化方法与应用专题前言
董云卫1, 刘关俊2, 毛晓光3
1(西北工业大学 计算机学院,陕西 西安 710129)
2(同济大学 计算机科学系,上海 201804)
3(国防科技大学 计算机学院,湖南 长沙 410073)
通讯作者: 董云卫, E-mail: yunweidong@nwpu.edu.cn
中文引用格式: 董云卫, 刘关俊, 毛晓光.形式化方法与应用专题前言.软件学报,2023,34(7).http://www.jos.org.cn/1000-9825/6864.htm
形式化方法是采用数理逻辑方法，对计算机软件建立严格语法与语义规范的系统设计与验证方法，常用于复杂动态系统的需求规约、模型设计和属性验证,在计算机硬件设计、软件系统构造、控制系统的设计与分析、通信系统协议验证和程序代码合成等方面得到成功应用.近年来,在深度学习、区块链、量子计算、物理信息融合系统等新兴领域,形式化方法也逐步应用和适配,对提升系统的安全性和可靠性起到极大的促进作用.
本专题公开征文,共收到41篇稿件.每篇稿件邀请2-3位专家进行评审,每位专家最多评审2篇论文.稿件经初审、复审、中国软件大会 ChinaSoft 2022 会议宣读以及终审4个阶段, 历时5个月,最终有9篇优秀论文入选本专题.
《安全的混成系统神经网络控制器生成与验证》面向混成系统的安全控制,提出一种以栅栏函数作为安全保证、以形式化验证提供的安全反例为反馈、由学习模块和验证模块组成的安全神经网络控制器生成方法,论文通过实验证明了该方法的有效性和可扩展性.
《自动驾驶交叉路口测试场景建模及验证方法》提出了一种面向自动驾驶的交叉路口测试场景的Petri网建模方法,给出了场景模型的交规属性和系统需求的一致性的验证方法,为自动驾驶汽车测试用例的生成提供了方法和技术支撑.
《一种基于LLVM Pass的复杂嵌套循环自动并行化框架》针对非平凡的复杂嵌套循环,提出了一种循环结构树表示模型以及基于此模型的循环程序自动并行化方法,有效处理LLVM Polly无法优化的复杂嵌套循环问题,增强了LLVM的并行编译优化能力.
《一种目标导向的多线程程序UAF漏洞预测方法》综合伴生Petri网模型、Petri网反向展开以及向量时钟等建模与分析方法,对UAF漏洞进行筛选,提高了现有缺陷预测方法的检测效率和准确性.
《基于约束依赖图的并发程序模型检测工具》针对现有的独立性分析方法会显著增加待探索的等价类路径数的问题,通过依赖约束图细化线程迁移依赖性,从而减少待探索的等价类路径数，进而减少并发程序验证的时空开销,开发了相关工具，实验展示了它的有效性.
《基于SMT的区域控制器同步反应式模型的形式化验证》针对工业级安全关键软件的形式化验证问题,提出一种针对程序综合的同步数据流模型，并基于SMT的验证方法,该方法融合了系统的环境输入、安全状态机和数据流模型,通过应用于轨交列控安全软件的验证试例,展示了本文验证方法的有效性.
《智能规划中面向简单偏好的高效求解方法》提出了一种求解简单偏好的规划方法，通过SMT求解器对简单偏好集合进行约简,并将简单偏好编码为经典规划模型, 并利用现有经典规划器进行求解,有效提升规划解的质量。
《面向未解释程序的合作验证方法》针对批量相似的未解释程序验证问题,提出了合作验证框架,通过复用中间验证结果来避免重复验证,同时对基于等价的路径抽象方法进行了改进,提高了验证效率.
《前馈神经网络和循环神经网络的鲁棒性验证综述》调研了大量前馈神经网络与循环神经网络的鲁棒性验证算法，对它们进行了梳理和分类，分析了鲁棒性验证方法之间的内在联系，总结了当前在这一研究方向上的技术挑战以及未来的研究方向。
本专题主要面向形式化方法相软件设计方法、验证支撑工具、工业应用等领域的研究人员和工程人员,反映了我国学者在形式化方法与应用领域最新的研究进展.感谢《软件学报》和CCF形式化方法、软件工程、系统软件等三个专委会对专题工作的指导和帮助,感谢本专题的全体评审专家及时、耐心、细致的评审工作, 感谢踊跃投稿的所有作者.希望本专题能够对形式化方法与应用相关领域的研究工作有所促进.
董云卫(1968－),男,博士,教授,博士生导师,CCF杰出会员,主要研究领域为模型驱动的软件开发方法、软件智能合成理论与方法、智能系统测试等.
刘关俊(1978－),男,博士,教授,博士生导师,CCF会员,主要研究领域为Petri网理论、模型检测、物理信息融合系统、基于强化学习的无人机协同等.
毛晓光(1970－), 男,博士,教授,博士生导师,CCF杰出会员,软件学报编委,主要研究领域为软件工程、可信软件、软件缺陷定位与自动修复等.
发布日期:2022-12-30浏览次数:
联系方式
- 《软件学报 》
- 主办单位：中国科学院软件研究所
中国计算机学会 - 邮编：100190
- 电话：010-62562563
- 电子邮箱：jos@iscas.ac.cn
- 网址：https://www.jos.org.cn
- 刊号：ISSN 1000-9825
- CN 11-2560/TP
- 国内定价：70元
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司
