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

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.