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