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

Trusted Software Programming Model Based on Formal Monitoring

作　　者：陈建明[1] 刘松[2] 李志蜀[2] 丁革建[1] 

机构地区：[1]浙江师范大学数理与信息工程学院,浙江金华321004 [2]四川大学计算机学院,成都610064

出　　处：《计算机工程》2011年第1期65-68,共4页Computer Engineering

基　　金：浙江省科技厅计划基金资助项目"高可信软件测评关键技术研究和测评工具开发"(2009C31118)

摘　　要：传统的形式化方法和软件运行时监控都是提高软件可信性的有效途径,但存在监控需求表达能力不强及代码分散等问题。针对该问题,提出基于形式化监控的可信软件构造技术FM-TSPM,将形式化方法和运行时监控相结合,实现跨领域的方法融合。用形式化方法描述监控约束,根据监控约束生成方面监控代码,解决代码分散问题。采用AOP编织器将方面代码编织到目标系统中。Formal methods and mntime monitoring both are very effective way to improve the software rehability, but have many hmltatlons 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.

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

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]