基于模型检测的高可靠性软件动态更新的设计与验证

Almost any software needs to be updated in its life circle. The traditional updating approach is to first stop the running software, replace it by installing the new version, and start the new version from the beginning. In some safety-critical fields, such as financial transaction systems, traffic control systems, and space flight systems, software needs to provide continuous services. Any downtime of such systems may lead to big economic loss and potential safety hazard. Dynamic software updating is proposed and well-studied to solve this problem. It is a promising technique for updating running software without incurring any downtime. However, dynamic software updating needs to be guaranteed reliable, and should never cause any errors to running systems, like repairing a car which is running at full speed. It is a challenging problem to design a safe dynamic software update. Model checking a kind of technique that uses mathematical approaches to verify the reliability of software and hardware. This project aims at investigating how to use model checking approach to design highly reliable dynamic software updates, with significance from both theoretical and practical point of view.

对于大多数软件，更新在其生命周期中都是不可避免的。传统的更新方法是首先停止当前软件的运行，安装新的软件，然后重新启动。然而在一些安全攸关的领域，如金融系统，交通控制系统和航空系统，软件需要保证不间断的运行，片刻的中断都有可能造成重大的经济损失或带来致命的安全隐患。为解决这类软件的更新问题，软件动态更新技术被提出并得到深入的研究。软件动态更新可以在不中断软件运行的前提下实现软件的更新，是一种非常有前景的更新技术。然而动态更新软件如同在修理一辆高速行驶的汽车，对更新可靠性有很高的要求，保证在更新过程中不会导致系统错误。如何设计一个可靠的软件动态更新并验证其可靠性是当前软件动态更新技术中最主要的难点之一。模型检测是一种利用数学的方法验证计算机软件和硬件可靠性的技术。本课题拟研究如何利用模型检测的方法设计高可靠性的软件动态更新方法并对其可靠性进行形式化分析和验证，具有重要的理论和现实意义。

软件动态更新是一种在不中断软件运行的前提下实现软件的更新的技术，尤其对那些提供不间断服务的系统具有非常重要的应用。这类系统大多安全攸关，因此必须保证动态更新的安全性。由于动态更新直接作用于运行中的软件，传统的测试方法无法有效地发现更新中所有可能出现问题。..本项目旨在借助形式化的方法，通过形式化验证技术实现软件动态更新的正确性验证与分析，从而保证其安全性。我们提出一种通用的基于带标签Kripke模型的软件动态更新验证方法，该方法通过对旧系统和新系统定义成独立的模型，在此基础上定义从旧状态到新状态的迁移规则，实现了软件更新的形式化定义。再次，我们从两个方面定义了软件动态更新的正确性，分别是新状态的可达性与应用相关的时序性质。新状态的可达性保证了软件的更新一定会完成，与应用相关的时序性质则保证了系统在更新前后的行为正确性。最后，我们在现有针对带标签的Kripke结构的模型检测方法的基础上进行扩展，实现了软件动态更新的形式化验证，并针对Python程序的更新作为案例进行了研究，实验结果表明方法的可行性。..本研究在软件动态更新的建模，正确性定义，验证等方面提出了一套相对通用的建模与验证方法，并通过具体的案例研究说明了方法的有效性，为软件动态更新技术提供了严格的安全分析方法，可有效解决软件动态更新安全性分析技术瓶颈，进而促进这一实用技术在实际领域的应用。..基于以上研究成果，本项目共发表论文10篇（包括CCF-B类、SCI二区论文等期刊论文5篇，CCF-C类国际会议论文5篇），获得软件著作权1项，培养了4名硕士研究生和辅助培养了博士研究生1名。