摘要： 关键软件要求极高的可靠性和安全性，然而当前的技术途径尚不能完全消除软件故障——软件测试不能保证软件正确性，模型检查等形式化验证技术也存在着诸多局限。文章提出了基于监控程序运行途径来捕获软件故障和验证程序性质正确性，构建了基于程序运行形式化分析的软件故障监控(SFMRFA)模型，在监控逻辑表达、程序插桩、multi-agent 设计等关键技术的基础上开发计算机辅助工具来监控、分析和引导程序执行，使软件运行当中可测、可控，避免软件失效。

关键词: 软件故障；软件监控；形式化方法；插桩

Abstract: Critical software requires high reliability and safety, but current techniques can not remove all software fault: software testing does not provide correctness guarantees, formal verification methods as model checking have much limitation to become common practice. A method based on monitoring software at run time to identify fault and verify the correctness of software is presented. The model of SFMRFA is constructed, and a computer-aided tool to monitor, analyze and guide the program execution is designed based on many techniques including monitoring logic, program instrumentation, multi-agent design etc. That is helpful for testing and controlling software at run-time and it can avoid software failure.

Key words: Software fault; Software monitoring; Formal method; Instrumentation