微信服务号

微信订阅号

2025年8月4日 20:24 星期一
首页 > 过刊浏览>2011年第22卷第6期 >1224-1235. DOI:10.3724/SP.J.1001.2011.04016
PDF HTML阅读 XML下载 导出引用 引用提醒
基于AOP 的运行时验证中的冲突检测
作者:
基金项目:

国家自然科学基金(60970035, 91018013, 90818024, 60803042)


Conflicts Detection in Runtime Verification Based on AOP
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [19]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    现有的形式化验证方法除了在模型层面对系统进行验证以外,越来越倾向于直接针对系统的实际代码和具体运行.运行时验证技术验证的对象是具体程序,它试图把形式化验证技术部署到程序的实际运行过程中.然而在把形式化技术部署到实际运行过程中会出现一系列在模型层面验证通常不会出现的问题,对这些问题中的冲突现象进行了研究,定义了运行时验证技术中存在的两种冲突,并给出了相应的检测算法.最后,对这些算法进行了实现和实例研究,结果表明了该方法的有用性.

    Abstract:

    Nowadays, instead of only verifying systems at the model level, current state-of-the-art verification techniques tend to focus on real code and real system’s execution. Runtime verification checks the system’s execution and tries to bridge the gap between formal verification techniques and real systems. However, this brings about some problems which usually do not appear in model-level verification. This paper analyses the problem in runtime verification. It defines two kinds of conflicts and lists their corresponding detection algorithms. These algorithms are implemented based on an open source runtime verification tool and some real cases are examined. The results demonstrate the effectiveness of the proposed method.

    参考文献
    [1] Bauer A, Leucker M, Schallhart C. Runtime verification for LTL and TLTL. ACM Trans. on Software and Methodology (TOSEM), upcoming. 2010.
    [2] Dwyer MB, Avrunin GS, Corbett JC. Property specification patterns for finite-state verification. In: Proc. of the 2nd Workshop on Formal Methods in Software Practice (FMSP’98). New York: ACM Press, 1998. 7?15. [doi: 10.1145/298595.298598]
    [3] Kiczales G, Lamping J, Mendhekar A, Maeda C, Lopes C, Loingtier JM, Irwin J. Aspect-Oriented programming. In: Proc. of the European Conf. on Object-Oriented Programming. LNCS 1241, Springer-Verlag, 1997. 220?242.
    [4] Kiczales G, Hilsdale E, Hugunin J, Kersten M, Palm J, Griswold WG. An overview of AspectJ. In: Proc. of the ECOOP 2001. London: Springer-Verlag, 2001. 327?353.
    [5] Kim MZ, Viswanathan M, Kannan S, Lee I, Sokolsky O. Java-MaC: A run-time assurance approach for Java programs. Formal Methods in System Design, 2004,24(2):129?155. [doi: 10.1023/B:FORM.0000017719.43755.7c]
    [6] Allan C, Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták O, de Moor O, Sereni D, Sittampalam G, Tibble J. Adding trace matching with free variables to AspectJ. In: Proc. of the OOPSLA 2005. New York: ACM Press, 2005. 345?364.
    [7] Chen F, Jin DY, Meredith P, Rosu G. Monitoring oriented programming—A project overview. In: Proc of the ICICIS 2009. New York: ACM Press, 2009. 72?77.
    [8] Colombo C, Pace GJ, Schneider G. LARVA—Safer monitoring of real-time Java programs. In: Proc. of the 7th IEEE Int’l Conf. on Software Engineering and Formal Methods (SEFM). Hanoi: IEEE Computer Society, 2009. 33?37. [doi: 10.1109/SEFM.2009.13]
    [9] Jones M, Hamlen KW. Disambiguating aspect-oriented security policies. In: Proc of the AOSD 2010. New York: ACM Press, 2010. 193?204. [doi: 10.1145/1739230.1739253]
    [10] Li XD, Qiu XK, Wang LZ, Lei B, Wang WE. UML state machine diagram driven runtime verification of Java programs for message interaction consistency. In: Proc. of the 2008 ACM Symp. on Applied Computing (SAC 2008). New York: ACM Press, 2008. 384?389. [doi: 10.1145/1363686.1363781]
    [11] Palm J, Wu PC, Lieberherr K. Understanding aspects through call graph enumeration and pointcut satisfiability. Technical Report, NU-CCIS-04-01, Boston: Northeastern University, 2004.
    [12] Lieberherr KJ, Palm J, Sundaram R. Expressiveness and complexity of crosscut languages. In: Proc. of the Workshop on the Foundations of Aspect Oriented Programming Languages (AOSD 2005). Chicago, 2005.
    [13] Avgustinov P, Christensen AS, Hendren L, Kuzins S, Lhoták J, de Moor O, Sereni D, Sittampalam G, Tibble J. abc: An extensible AspectJ compiler. In: Proc. of the Trans. on Aspect-Oriented Software Development I. LNCS 3880, Heidelberg: Springer-Verlag, 2006. 293?334. [doi: 10.1007/11687061_9]
    [14] Bauer L, Ligatti J, Walker D. Composing expressive runtime security policies. ACM Trans. on Software Engineering Methodology, 2009,18(3):1?43. [doi: 10.1145/1525880.1525882]
    [15] Malakuti S, Bockisch C, Aksit M. A rule set to detect interference of runtime enforcement mechanisms. In: Proc. of the 20th Annual Int’l Symp. on Software Reliability Engineering (ISSRE 2009). Mysore: IEEE Computer Society Press. 2009. 16?19.
    [16] Katz E, Katz S. Incremental analysis of interference among aspects. In: Proc. of the 7th Workshop on Foundations of Aspect-Oriented Languages (FOAL 2008). New York: ACM Press, 2008. 29?38. [doi: 10.1145/1394496.1394500]
    [17] Aksit M, Rensink A, Staijen T. A graph-transformation-based simulation approach for analysing aspect interference on shared join points. In: Proc. of the 8th ACM Int’l Conf. on Aspect-Oriented Software Development (AOSD 2009). New York: ACM Press, 2009. 39?50. [doi: 10.1145/1509239.1509247]
    [18] Kniesel G. Detection and resolution of weaving interactions. In: Proc. of the Trans. on Aspect-Oriented Software Development V. Heidelberg: Springer-Verlag, 2009. 135?186. [doi: 10.1007/978-3-642-02059-9_5]
    [19] Bodden E. Specifying and exploiting advice-execution ordering using dependency state machines. In: Proc. of the Int’l Workshop on the Foundations of Aspect-Oriented Languages (FOAL). 2010.
    引证文献
引用本文

张献,董威,齐治昌.基于AOP 的运行时验证中的冲突检测.软件学报,2011,22(6):1224-1235

复制
相关视频

分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2010-07-10
  • 最后修改日期:2011-03-29
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号