作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2011, Vol. 37 ›› Issue (01): 65-68. doi: 10.3969/j.issn.1000-3428.2011.01.023

• 软件技术与数据库 • 上一篇    下一篇

基于形式化监控的可信软件构造模型

陈建明1,刘 松2,李志蜀2,丁革建1   

  1. (1. 浙江师范大学数理与信息工程学院,浙江 金华 321004;2. 四川大学计算机学院,成都 610064)
  • 出版日期:2011-01-05 发布日期:2010-12-31
  • 作者简介:陈建明(1957-),男,副教授,主研方向:软件理论, 信息安全;刘 松,硕士;李志蜀,教授、博士生导师;丁革建,硕士
  • 基金资助:
    浙江省科技厅计划基金资助项目“高可信软件测评关键技术研究和测评工具开发”(2009C31118)

Trusted Software Programming Model Based on Formal Monitoring

CHEN Jian-ming 1, LIU Song 2, LI Zhi-shu 2, DING Ge-jian 1   

  1. (1. College of Mathematics Physics and Information Engineering, Zhejiang Normal University, Jinhua 321004, China; 2. School of Computer Science, Sichuan University, Chengdu 610064, China)
  • Online:2011-01-05 Published:2010-12-31

摘要: 传统的形式化方法和软件运行时监控都是提高软件可信性的有效途径,但存在监控需求表达能力不强及代码分散等问题。针对该问题,提出基于形式化监控的可信软件构造技术FM-TSPM,将形式化方法和运行时监控相结合,实现跨领域的方法融合。用形式化方法描述监控约束,根据监控约束生成方面监控代码,解决代码分散问题。采用AOP编织器将方面代码编织到目标系统中,构造出带监控能力的可信软件。

关键词: 运行时监控, 确定有限自动机, 面向方面编程

Abstract: Formal methods and runtime monitoring both are very effective way to improve the software reliability, but have many limitations like weak ability of expressing requirements and code scattering. Aiming at these problems, Formal Monitoring-based Trusted Software Programming Model(FM-TSPM) is proposed in the paper, which combines the advantage of the formal method and the runtime monitoring, achieving the integration of Interdisciplinary approaches. System requirements are expressed using formal specifications. Efficient monitoring code is automatically generated according to the specifications, solving the code scattering problem. It weaves the monitoring code and the source code together, so as to inject monitoring ability to the software.

Key words: runtime monitoring, DFA, Aspect-Oriented Programming(AOP)

中图分类号: