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

詹乃军1,  王  戟2,  李宣东3
1(中国科学院软件研究所 计算机科学国家重点实验室,北京 100190)
2(国防科学技术大学 计算机学院,湖南 长沙  410073)
3(南京大学 计算机软件新技术国家重点实验室,江苏 南京  210046)
通讯作者: 李宣东, E-mail: lxd@nju.edu.cn

中文引用格式: 詹乃军,王戟,李宣东.软件形式化方法与应用专刊前言.软件学报,2016,27(3):495-496. http://www.jos.org.cn/1000-9825/4990.htm

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专刊收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.

《几何代数的高阶逻辑形式化》提出了一种基于高阶逻辑定理证明器HOL-Light的几何代数建模和验证方法,在高阶逻辑证明工具HOL-Light中建立了几何代数系统的形式化模型和相关性质定理的逻辑推理证明,并给出了三维欧氏空间中刚体运动的建模与验证实例.

《有界闭连通域上的非线性循环终止性分析》研究了非线性单分支循环程序的终止性问题,将该问题归结为是否存在不动点,并基于Groebner基给出了程序非终止输入集合的可行算法.

《城市交通网络信号控制系统的实时演算模型》基于实时演算理论为两类城市交通网络的定时和自适应信号控制系统建立了统一模型,给出了基于最小加代数计算交通拥塞系数的方法.

《一种基于变量访问序模式的中断数据竞争检测方法》面向中断驱动型嵌入式软件,提出一种基于变量访问序模式的中断数据竞争检测方法.

《安全苛刻系统测试语言中的测试设备协同语句》针对安全苛刻系统测试中测试设备协同任务的特点,通过给出测试语言中测试设备协同相关类型、设备协同表达式,定义测试设备协同语句,并通过设备协同表达式求值定义设备协同语句的操作语义规则.

《基于模拟关系的精化检测方法》针对精化检测应用中遇到的状态空间爆炸问题,提出了基于模拟关系的stable failures 和failures-divergence精化检测方法,并应用到时间自动机的验证中.

《面向条件判定覆盖的线性拟合制导测试生成》针对条件判断覆盖准则(C/DC)测试用例自动生成问题,提出了一种线性拟合的测试生成方法,把程序中的条件判定利用分段线性函数来模拟,以解决条件判定中出现非线性函数导致求解器无法求解的问题.

《基于同步语言的时间可预测多线程代码生成方法》基于同步语言SIGNAL研究如何生成时间可预测的多线程代码的方法,并基于AADL建模语言进行扩展,以构造时间可预测多核体系结构模型,使得所生成的多线程代码可以在该体系结构下满足时间可预测性的要求.

《一个面向方面设计中干涉问题的分析工具》针对方面与基础程序之间的干涉检测问题,以基础程序和方面的规约和不变式为起点,通过不发生干涉条件的定义自动转换为PVS定理,从而将干涉检测问题转换为PVS定理证明问题.

《运用栅栏函数验证连续系统在有界时间内的安全性》通过栅栏函数研究系统在有界时间的安全性,通过潜在的指数函数栅栏计算多项式栅栏函数组合,给出了一个有界时间内的栅栏函数充分条件.

《不确定条件下基于价格时间自动机的智能大厦空调系统调度策略评估》研究智能大厦空调通风系统的控制管理模型,综合考虑智能大厦所处的环境具有许多不确定因素来制订空调系统调度策略,提出了一种基于价格时间自动机的调度策略评估方法.

《SAT-PPTLSL:二维逻辑PPTLSL的可满足性检查》基于范式和范式图,为可满足性检查建立了基础条件,从而实现了PPTLSL公式的可满足性判定过程,为指针程序的分析验证提供了一种有理论依据的检查工具.

《面向无穷数据的形式模型综述》对面向无穷数据的形式模型进行了较为详尽的综述,在对无穷数据模型的分类上采取了根据自动机进行分类的方式,并讨论了与自动机模型相关的逻辑模型.

本专刊面向形式化方法与工具、软件工程、计算机系统工程、嵌入式软件系统及其相关领域的研究人员和专业工程师等,审稿过程历经4个月,20余名相关领域的专家和学者参与审稿工作,审稿过程中还选择了部分投稿论文在中国计算机学会形式化方法专业学组成立大会上交流,经过初审、复审和终审等多道严格程序最终确定收录以上13篇论文.在此我们感谢相关领域学者的踊跃投稿,感谢审稿专家和学报编辑部的辛勤工作.

詹乃军(1971－),男,博士,中国科学院软件研究所研究员,博士生导师.研究工作主要涉及嵌入式和混成系统设计理论,程序验证,并发计算模型,形式语义,模态和时序逻辑等.
王戟(1969－),男,博士,国防科学技术大学教授,博士生导师,主要从事高可信软件,并行与分布处理方面的研究工作.
李宣东(1963－),男,博士,南京大学教授,博士生导师.CCF会士.教学、研究工作主要涉及软件工程与形式化方法,重点包括软件建模与分析,软件测试与验证.