形式化方法与工具专刊前言
王 戟1, 李宣东2,3
1(国防科学技术大学 计算机学院 并行与分布处理国防科技重点实验室,湖南 长沙 410073)
2(计算机软件新技术国家重点实验室(南京大学),江苏 南京 210093)
3(南京大学 计算机科学与技术系,江苏 南京 210093)
Corresponding author: E-mail: lxd@nju.edu.cn
Wang J, Li XD. Preface to special issue on formal methods and tools. Journal of Software, 2011,22(6):1121-1122. http://www.jos.org.cn/1000-9825/4036.htm
形式化方法是指有严格数学基础的软件和系统开发方法,支持计算机系统及软件的规约、设计、验证与演化等活动.随着高可信软件的兴起,形式化方法作为重要的途径,关注度日益提高.其作用不仅深化了人们对计算系统规律的认识,而且支持了计算系统开发、运行和演化之工具、平台、环境的构建.本专刊收录的11篇论文反映了近年来我国学者在形式化方法与工具领域的部分研究成果.
论文《策略驱动的可靠嵌入式系统建模及分析方法》提出一种嵌入式系统建模与分析方法.该方法针对可靠性需求,基于Petri网对设备、计算与物理交互、组件及通信过程等要素建模,进而分析和评估相关可靠性保障策略.
论文《Java指针指向分析优化》针对Java程序提出一种上下文敏感的指针指向分析算法,并通过拓扑排序和环路检测与消除技术对算法进行了优化.
论文《Object-Z规格说明测试用例的自动生成器》提出一种测试用例生成方法并给出了工具实现.该方法支持从Object-Z规格说明中提取语义生成抽象测试用例.
论文《循环对称化简及在三值模型上的扩展》针对并发系统模型检验中的状态空间爆炸问题,提出一种状态空间对称化简方法,并将其应用于三值模型.
论文《场景驱动的服务行为调控》提出一种服务行为调控方法.该方法根据UML顺序图描述的场景需求,基于Petri网遍历目标服务的BPEL行为规约,通过监听、检查和过滤消息实现服务行为的调控.
论文《混合语义时间Petri网模型》提出一种时间Petri的混合语义模型.该模型通过适当调整可实施条件和设置强制实施点,来消除现有语义模型在调度分析上的缺陷.
论文《软件体系结构动态演化的条件超图文法及分析》采用条件超图文法描述软件体系结构演化过程,并给出相应演化一致性分析方法.
论文《基于AOP的运行时验证中的冲突检测》针对运行时验证中单个监控器内部的冲突和多个监控器之间的冲突问题,给出了相应的检测算法.
论文《基于自动机理论的分布式实时调度分析工具》提出一个分布式系统任务实时调度分析方法及工具原型.该工具用自动机分别描述任务的执行语义及其外部到达关系,通过自动机组合的可达性分析解决任务调度问题.
论文《AADL模型可靠性分析评估工具》给出一个AADL可靠性模型分析评估工具,通过将AADL可靠性模型转换为广义随机Petri网模型进行可靠性分析与评估.
论文《时变网络中国邮路问题的时间自动机模型》提出一种时变网络中国邮路问题的时间自动机模型,进而利用时间自动机模型检验工具进行问题求解.
王戟(1969-),男,博士,教授,博士生导师,国家杰出青年科学基金获得者,教育部长江学者特聘教授,CCF高级会员.主要从事高可信软件,软件工程与分布并行计算等领域的研究.
李宣东(1963-),男,博士,教授,博士生导师,国家杰出青年科学基金获得者,CCF高级会员.教学、研究工作主要涉及计算机软件工程,重点包括软件建模与分析、软件测试与验证.