面向方面设计中干涉问题的分析工具

来源：软件学报杂志2016年第3期北京时间：

作者：陈鑫,黄超,张一帆,梅一鸣

单位：陈鑫，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学计算机科学与技术系, 江苏 南京 21002311,黄超，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学计算机科学与技术系, 江苏 南京 21002302,张一帆，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学计算机科学与技术系, 江苏 南京 21002303,梅一鸣，计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023;南京大学计算机科学与技术系, 江苏 南京 21002304

摘要：干涉问题是指基础程序和方面之间或者方面之间发生不需要的相互作用,导致最终程序中产生不想要的功能,危害程序的正确性.很难检测和修正在面向方面设计中存在的干涉,已经成为推广面向方面技术的阻碍.受到技术自身可扩展能力的局限,现有的基于模型验证技术的工作不能有效地处理功能干涉问题.设计开发了基于推理验证技术直接检查和去除面向方面设计中功能干涉的工具,它可以根据类和方面的功能规约自动产生确保不发生干涉的条件,并引入交互式证明工具PVS来提高证明过程的自动化程度.证明可以确认设计中无干涉存在或者为修正干涉问题提供线索.

关键词：面向方面的设计;功能干涉;推理验证;设计演算

基金资助：国家自然科学基金(91318301,61561146394);国家重点基础研究发展计划(973)(2014CB340703);教育部高等学校博士学科点专项科研基金(20110091120058);江苏省产学研项目(BY2014126-03)