面向运行时监控的软件设计与验证理论研究

由于软件自身及其环境的复杂性，软件故障难以完全避免。因此，在软件运行过程中实施有效监控，尽早发现可能问题并及时采取修正措施，对提高软件可靠性与安全性具有重要意义。本课题将首先从航天、武器装备等领域中关键软件的特点和监控需求出发，探索其失效模式特征与分类，研究支持多维监控属性描述的形式化规约技术与监控性质模版；然后结合统一建模语言UML、Aspect软件设计、设计模式等软件工程主流技术以及软件形式建模与设计验证理论的最新进展，研究面向运行时监控的软件设计与验证理论以及针对典型监控属性的设计模式；进一步以软件运行时验证理论为基础，结合程序分析、软件故障诊断与隔离等技术，研究运行时主动监控理论框架与关键技术，使监控能对软件运行进行一定程度的预测，及时发现故障趋势，并通过对软件运行过程的调整和干涉来避免故障实际产生；最终建立自动化程度高、与主流软件工程环境相结合的软件运行时监控设计与验证工具环境。

对于各种关键领域的软件，即使在开发过程中采用非常严格的设计和验证方法，也无法避免软件部署后存在遗留缺陷，从而在运行过程中发生背离期望性质的行为。因此，在软件运行过程中进行动态监控非常重要。但现有监控方法，例如运行时验证技术等，只能被动的观察软件系统执行，当发现对关键性质的违背时，往往意味着软件失效已经发生。对此，基于预测和预防的思想，本项目提出了软件主动监控的概念，并对其理论基础和关键技术进行了深入研究。主动监控的目标不局限在软件失效发生后采用相关技术修复失效，而是希望能够尽早预测失效的可能发生，然后产生相应的调控动作，以避免软件运行实际到达失效状态。本项目的主要研究成果包括：. （1）结合闭环反馈的控制理论，提出了基于预测语义的软件主动监控理论和相应的实现框架。该方法针对时序逻辑性质生成基于预测语义的监控器，对可能到来的、违背性质的行为进行预测，并按照部分系统模型生成必要的干涉动作对系统进行调控，以规避实际导致缺陷产生的执行路径。实例研究表明，该方法能适用于safety-critical系统（如嵌入式控制软件）和security-critical系统（如信息系统软件）。. （2）在软件主动监控理论框架下，研究相适应的监控属性规约技术，以对功能属性、时序属性、参数化属性、周期性等复杂性质进行描述，并设计了能表达控制流与数据流关系的事件序列选择语言。. （3）为了优化带有监控需求的软件结构、减少监控机制对软件的影响，研究了面向运行时监控的软件设计方法，包括基于UML和Aspect的软件监控设计方法、混成系统的运行监控方法、嵌入式操作系统的运行监控方法、监控设计的一致性检测方法等。. （4）为了提高监控器的生成和运行效率，对监控器自动生成、优化和部署方法进行了研究，包括提出了一种能适用于更复杂时序性质的高效预测监控器生成方法；为了提高预测能力以及减少运行时监控开销，研究了结合静态分析的预测监控优化方法，并研究了多对象、多监控器的协同技术。. 本项目根据上述研究成果设计实现了软件主动监控工具原型，对汽车控制系统、火车交通控制、嵌入式操作系统、安全操作系统、部分开源软件等进行了实验验证，取得良好的效果。