期刊文献+

参数化运行时监控研究 被引量:1

Research on Parameterized Runtime Monitoring
下载PDF
导出
摘要 随着计算机软件广泛应用于各类安全关键系统以及软件日趋复杂,软件可靠性变得越来越重要。作为一种广泛使用于各种平台的软件解决方案,运行时监控是提高软件可靠性的最灵活的解决方案之一。但随着运行时监控技术以及软件技术的发展,人们希望通过运行时监控技术来验证系统的动态属性,从而提出参数化性质的运行时监控技术。由于其在面向对象系统中的适用性,参数化性质的运行时监控已经受到了越来越多的关注。综述了参数化运行时监控的研究进展,提出了参数化运行时监控的问题定义,介绍了这一领域的主要研究内容:参数化运行时监控方法、减少参数化监控开销的技术、多属性规约的参数化运行时监控。 With the wide application of software in all kinds of safety critical systems as well as the increasingly complexity,software reliability becomes more and more important.As a software solution widely used in various platforms,runtime monitoring is one of the most flexible solution to enhance the reliability of software.With the development of runtime monitoring and software technology,people want to verify the dynamic properties of system through runtime monitoring.So runtime monitoring of parametric properties was presented.Runtime monitoring of parametric properties have achieved more and more attention because of its applicability in the object-oriented system.This paper summarized the researches on parametric runtime verification,presented the problem definition of parametric runtime verification,and introduced the main research content of this field,including parametric runtime verification approaches,technologies of reducing parametric monitoring overhead and runtime monitoring of multiply parametric properties.
出处 《计算机科学》 CSCD 北大核心 2014年第11期146-151,174,共7页 Computer Science
基金 湖北省自然科学基金面向项目(2010CDB04001) 武汉大学计算机软件工程国家重点实验室开放基金项目(SKLSE 20080705) 华中师范大学基本科研业务基金项目(CCNU11A02007) 华中师范大学自制实验仪器设备与软件项目(201314)资助
关键词 运行时监控 参数化性质规约 参数化运行时监控 Runtime monitoring Parametric property specification Parametric runtime monitoring
  • 相关文献

参考文献31

  • 1Clarke E M,Wing J M. Formal methods: State of the art and fu ture directions[J]. ACM Computing Surveys, 1996,28 (4) : 626- 643. 被引量:1
  • 2Clarke E M, Grumberg O, Peled D A. Model Checking [M]. Massachusetts:The MIT Press,1999. 被引量:1
  • 3Gabbay D M, Hogger C J, Robinson J A, et al. Handbook of I.ogic in artificial Intelligence and Logic Programming[C]//Vo- lume2, Deduction Methodologies. London.-Oxford University Press, 1994. 被引量:1
  • 4Blum M, Kannan S. Designing programs that check their work [J]. Journal of the ACM, 1995,42 (1) : 269-291. 被引量:1
  • 5Bauer A, Leucker M, Schallhart C. Runtime Verification for LTL and TLTL[J]. ACM Transactions on Software Enginee:ring and Methodology, 2011,20(4) : 1-64. 被引量:1
  • 6Havelund K, Rosu G. Synthesizing Monitors for Safety Proper- ties[C] // Proceedings of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Sys- tems. London, UK, 2002 : 342 -356. 被引量:1
  • 7Bodden E, Hendren L, Lain P, etal. Collaborative runtime verifi- cation with tracematches[C]//Proceedings of the 7th interna- tional conference on Runtime Verification. Berlin, Germany, 2007 : 22-37. 被引量:1
  • 8Bodden E. A lightweight LTL runtime verification tool for Java [C] // Proceedings of the 9th Annual ACM SIGPLAN Confe- rence on Object-oriented Programming, Systems, Languages, and Applications. New York, USA, 2004 : 306-307. 被引量:1
  • 9Havelund K, Rosu G. Monitoring Java Program with Java Path Explorer [J]. Electronic Notes in Theoretical Computer Science, 2001,55 (2) : 200-217. 被引量:1
  • 10Kim M, Kannan S, Lee L, et al. Java-MaC: a run-time assurance approach for J]tva programs[J]. Formal Methods in System De- sign,2004,24 (2) : 129-155. 被引量:1

二级参考文献19

  • 1Stolz V. Temporal assertions for sequential and concurrent programs [Ph.D. Thesis]. Aachen: RWTH Aachen University, 2007. 被引量:1
  • 2Bauer A, Leucher M, Schallhart C. Runtime verification for LTL and PTLTL. Technical Report, TUM-I0724, Miinchen: Technische Universitat Munchen, 2007. 被引量:1
  • 3Bauer A, Leucker M. Monitoring of real-time properties. In: Kumar A, Seth A, eds. Proc. of the Foundations of Software Technology and Theoretical Computer Science (FSTCS). LNCS 2937, Heidelberg: Springer-Verlag, 2006.260-272. 被引量:1
  • 4Dong W, Leucker M, Schallhart C. Impartial anticipation in runtime verification. In: Kim M, Viswanathan M, eds. Proc. of the 6th Int'l Symp. on Automated Technology for Verification and Analysis (ATVA 2008). LNCS 5311, Heidelberg: Springer-Verlag, 2008. 386-396. 被引量:1
  • 5d'Amorim M, Rosu G. Efficient monitoring of ω-languages. In: Etessami K, Rajamani S, eds. Proc. of the 17th Int'l Conf. on Computer-Aided Verification (CAV 2005). LNCS 3576, Heidelberg: Springer-Verlag, 2005. 101-112. 被引量:1
  • 6Stolz V, Bodden E. Temporal assertions using AspectJ. Electronic Notes in Theoretical Computer Science, 2005,144(4): 109-124. 被引量:1
  • 7Stolz V. Temporal assertions with parametrised propositions. Journal of Logic and Computation, 2008. doi: 10.1007/978-3-540- 77395-5. 被引量:1
  • 8Havelund K, Rosu G. Monitoring programs using rewriting. In: Alexander P, Berry Y, eds. Proc. of the Int'l Conf. on Automated Software Engineering (ASE 2001). San Diego: ACM Press, 2001. 135-143. 被引量:1
  • 9Havelun K, Rosu G. Synthesizing monitors for safety properties. In: Ball T, Bouajjani A, eds. Proc. of the Tools and Algorithms for Construction and Analysis of Systems (TACAS 2002). LNCS 2280, Berlin: Springer-Verlag, 2002. 342-356. 被引量:1
  • 10Drusinsky D. The temporal rover and the ATG rover. In: Havelund K, Penix J, eds. Proc. of the SPIN Model Checking and Software Verification. LNCS 1885, Springer-Verlag, 2000. 323-330. 被引量:1

共引文献5

同被引文献2

引证文献1

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部