现代社会中,计算机软件发挥越来越重要的作用。计算机软件随处可见,大到神舟七号航天器,小到个人电脑,都有软件的身影。然而,世上没有完美的软件,几乎所有的软件都有缺陷,所以需要对软件进行更新。软件更新是很常见的,一般的软件更新需要停止软件、更新软件、启动软件。但是有的大型系统需要提供不间断服务,不能因更新而中断,如银行服务器、门户网站、大型路由器上系统程序等。更新这类程序时,要在程序运行的过程中进行更新。这就提出了动态软件更新的需求。但是软件系统中,一个或多个模块更新时,新模块是否能提供旧模块所能提供的一切?更新后,系统中的其它模块是否会受到影响?整个系统是否能正常工作?这些问题都不得而知。本文用动态静态的工具分析“多模块软件系统中,新模块是否可以安全更新旧模块”的问题。在分析方法中,使用了“程序不变量”的概念。所谓“程序不变量”,就是程序中某一点上或某一些点上,程序变量具有的属性。常见的不变量,如,在程序的某点处,变量x和变量y都有效,且“y = 4 * x + 3”这个等式总是成立;在程序的另一点处,变量g有效,且变量g表示一个图,而且“g总是一个无环图”。这些都是不变量[2]。在本文中,软件更新的前提是:新旧模块具有一样的接口,而且正确的新模块能够提供旧模块所能提供的一切,新旧模块的效率可能不一样。软件系统中,根据模块更新与否,可以将所在模块分为两大类:不需要更新的模块,在文中我们称之为“非更新模块”,和需要更新的模块,在文中我们称之为“被更新模块”。我们分析方法也相应分为两种:对非更新模块的动态分析;对被更新模块的静态分析。首先,对于软件系统中的非更新模块,更新前后,这些模块中的不变量应该维持不变。我们用动态分析的方法来检查,更新后,系统非更新模块中的不变量是否仍然保持,以此来判断“更新是否成功”。其次,对于软件系统中被更新的模块,可以通过对新旧模块的不变量之间的应该满足某种关系进行逻辑推理,从而得到“更新是否可进行”的结论。对一个大型软件系统而言,更新很重要,而错误的更新带来的不良后果是很严重的。本文中的方法在“更新之前”得到“更新是否可进行”的结论,从而可从源头上有效的避免了错误更新带来的严重后果。本文的主要创新点有:1.从被更新模块和非更新模块两个方面分析“更新是否可进行”,对被更新模块使用静态分析,对非更新模块使用动态分析。这样会更全面,更多的反映出更新可能会带来的问题。2.对于软件系统中非更新模块,用“程序不变量”来分析“被更新模块的更新是否对系统中的非更新模块有影响”。在更新前,系统中的非更新模块中有很多的程序不变量。因为新旧“被更新模块”的接口和功能一样,模块的更新对于系统中非更新模块是透明的。更新后,系统中非更新模块中的程序不变量应该仍然成立。3.对于软件系统中的被更新模块,新模块要能做到“旧模块能做到的一切”,而且,更新后,系统中非更新模块的不变量不应被违背。文中通过推理新旧模块不变量的逻辑关系,来分析“更新是否可进行”;4. Daikon工具可以用来分析程序的不变量,但是Daikon工具得出的不变量不一定是正确的,文章中用ESC/Java静态工具对Daikon得出的不变量作验证,过滤Daikon得出的虚假不变量[6];5.程序不变量可以以JML注释的形式存在于Java代码中,而JMLC工具可以将Java代码中的JML注释编译为可执行代码中的assertion判断,然后使用JMLRAC工具在程序运行过程中检查assertion断言是否被违背,也就是检查不变量是否被违背。