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)

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

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

CLC Number: 

• TP311