2022年第8期专题优先出版:形式化方法与应用(陈立前,孙猛)
  • 分享:
  • 0

形式化方法与应用专刊前言

陈立前1  2

1(国防科技大学 计算机学院,湖南 长沙  410073)

2(北京大学 数学科学学院,北京  100871)

通讯作者: 陈立前, E-mail: lqchen@nudt.edu.cn

中文引用格式: 陈立前,孙猛. 形式化方法与应用专刊前言.软件学报,2022,33(8). http://www.jos.org.cn/1000-9825/6611.htm

形式化方法基于严格的数学方法来规约、设计、构建、验证、演进计算系统,是改善和保障计算系统可信性的重要方法。形式化方法相关基础理论、技术和工具已成功应用于各种软硬件系统的设计与验证。近年来,在区块链、深度学习、量子计算等新兴领域,形式化方法也逐步应用适配,提升新兴领域计算系统的可信性。

本专刊公开征文,共收到投稿40.特约编辑先后邀请了 20多位专家参与审稿工作,每篇投稿至少邀请2位专家进行评审.稿件经初审、复审、中国软件大会ChinaSoft 2021会议宣读和终审4个阶段,历时7个月,最终有15篇论文入选本专刊,其中,

面向SQLite3数据库API调用序列的并行运行时验证方法》针对SQLite3数据库API调用序列提出了一种基于多核系统的并行运行时验证方法,能够有效发挥多核系统的硬件能力,提高验证效率.

《一种利用非确定规划的LTL合成方法》提出了一种利用非确定规划求解LTL合成问题的方法,证明了方法的正确性和完备性,通过实验表明了该方法在解质量方面具有优势,能够获得规模较小的合成策略.

基于基本并行进程的异步通讯程序的验证方法与实现》改进了一类为异步通讯程序建模的Actor通讯系统,将其归约至基本并行进程,并实现了相应的模型检测工具.

运用时间分类树的确定单时钟时间自动机学习》针对确定性单时钟时间自动机学习的效率问题,提出了一种改进的学习算法,使用逻辑时间分类树作为学习算法的内部数据结构,有效地减少了成员查询次数,降低了算法的空间复杂度.

面向CPS时空约束的资源建模及其安全性验证方法》针对信息物理空间中CPS资源安全性验证问题,基于时间通信顺序进程TCSP,提出了一种面向CPS时空约束的资源建模及其安全性验证方法.

基于消息传递关系网络的布尔可满足性预测》提出将SAT问题转化为一种多关系异构图,基于关系消息传递网络提出了一种预测精度更高、泛化能力更好的布尔可满足性预测方法.

基于Sys ML的机载软件分层精化建模与验证方法》提出了一种基于SysML状态机图子集的机载软件分层精化建模与验证方法,并以自动飞行控制软件为例验证了方法的有效性.

智能合约的时间约束模式及其形式化验证》分析总结出智能合约的五种时间约束模式,定义了Solidity智能合约到时间自动机的转换规则并实现其到实时模型检测工具UPPAAL入口模型的转换,然后利用UPPAAL验证合约的时间相关性质.

TSO内存模型下限界可线性化的可判定性研究》研究了k-限界TSO-to-TSO可线性化、k-限界TSO-to-SC可线性化和k-限界TSO可线性化的可判定问题,证明了TSO内存模型下可线性化的这三种限界版本都是可判定的.

基于深度学习和反例制导的循环程序秩函数生成》针对非线性循环程序,提出了一种基于反例制导的神经网络型秩函数的构造方法,采用了学习组件和验证组件交互的迭代框架.

基于正时态测试器的实时分支时态逻辑符号化模型检测针对一种实时分支时态逻辑RTCTL*的高效模型检测问题,提出了一种 RTCTL*正时态测试器构造方法以及相关符号化模型检测算法,并开发了基于该算法的模型检测工具.

模拟多核多任务实时系统的点区间优先级时间Petri网与TCTL模型检测》针对传统优先级时间Petri网对实时系统建模能力不足的问题,提出了一种点区间优先级时间Petri,以模拟多核多任务实时系统,并设计了相应的模型检测算法,开发了相应的模型检测器.

一种面向抽象解释框架的函数内联过程间分析的优化方法》针对函数内联过程间分析方法存在的不足, 在基于抽象解释的程序分析场景下,提出了一种面向内联函数块的程序环境降维优化方法,以降低分析过程的时空开销.

基于锁耦合遍历算法的文件系统终止性验证》构建了一个终止性证明框架CRL_T,并验证了文件系统AtomFS中保证了任何一个接口在公平调度的条件下都能返回,Coq相关证明进行了形式化。

软硬件综合AADL可靠性建模及分析方法》综合考虑软、硬件错误发生失效后对系统可靠性的影响,提出了一种面向系统架构级别的软硬件综合可靠性分析方法.

本专刊主要面向形式化方法相关理论研究、支撑工具、工业应用等领域的研究人员和工程人员,反映了我国学者在形式化方法与应用领域最新的研究进展.感谢《软件学报》编委会和CCF软件工程、系统软件、形式化方法专委会对专刊工作的指导和帮助,感谢专刊全体评审专家及时、耐心、细致的评审工作,感谢踊跃投稿的所有作者.希望本专刊能够对形式化方法与应用相关领域的研究工作有所促进.

 

陈立前(1982),,博士,国防科技大学副教授,CCF高级会员,主要研究领域为程序分析与验证,抽象解释.

孙猛(1978-),,博士,北京大学教授,CCF高级会员,主要研究领域为程序理论、软件形式化方法.

发布日期:2022-02-17浏览次数:

当期目录


文章目录

过刊浏览

年份

刊期

联系方式
  • 《软件学报 》
  • 主办单位:中国科学院软件研究所
                     中国计算机学会
  • 邮编: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
技术支持:北京勤云科技发展有限公司

京公网安备 11040202500063号