软件系统的更新是不可避免的。通常这些更新是通过离线方式完成的。离线更新需要先关闭系统,在安装新版本后,重启系统,因此离线更新会给系统带来较长时间的干扰和中断。在例如金融事务处理系统等关键性场景中,服务是不能被长时间中断的。因此,离线更新不适用于这些场景。同时离线更新在日常应用程序系统如Windows中带来的频繁干扰也是很恼人的。所以,我们需要一种在运行时刻更新软件系统的技术,即软件动态更新。因为软件动态更新需要将运行中的旧版本系统状态映射到新版本中,即使是新旧版本都正确的情况下,它仍可能会导致离线更新不会引发的错误,所以它并没有被广泛应用。形式化方法是保证软件动态更新正确性的一种主流方法。但是已有的形式化方法有一些不足,有的只考虑了模型本身的信息而没有考虑用户提供的规约,这样太过于宽松以至于不能保证正确性；有的方法把系统看作白盒,对系统内部实现的状态迁移进行规约,带来过度规约的问题；还有的工作仅仅考虑了静态分析的信息,虽然能够保证软件动态更新的正确性,但是太过于保守。为了解决这些问题,本文做了如下工作：1.提出一个软件动态更新的形式化框架。这个框架的与以往工作不同之处在于该框架使用了显式化的环境模型以及基于事件的角度。这两个特点可以使得我们在一个更加抽象的层面来定义软件动态更新及其正确性。这样可以避免过度规约的问题,允许更加灵活的软件动态更新。2.基于上述框架,我们提出一个基于运行时刻监视器的乐观软件动态更新方法。不同于以往的仅仅使用静态信息的保守悲观软件动态更新,我们结合运行时刻的监视器获得的运行时刻的信息与静态分析的结果,提出了一个乐观的方法,使得在保证正确性的前提下,提高软件动态更新的时效性。进一步,我们给出了一个自动合成该监视器的算法。3.对软件动态更新的平滑性进行了初步研究。我们不仅想要保证软件动态更新的正确性,更希望能够软件动态更新能够有更高的质量,保留已有的适用于新版本的计算结果。这样可以使得在更新之后,不需要在重做或者补偿上面付出额外的开销。