可在www.sciencedirect.com在线获取理论计算机科学电子笔记294（2013）12-23www.elsevier.com/locate/entcs动态软件更新行为正确性的形式化与验证张敏、绪方和弘、二次幸吉软件验证日本科学技术高等研究所（JAIST）Asahidai 1-1，Nomi，Ishikawa，Japan摘要动态软件更新（DSU）是一种对正在运行的软件系统进行实时更新的技术。虽然有一些关于动态更新正确性的研究，但它们集中在如何在代码级正确部署更新，例如， 如果过程引用了正确类型的数据。 然而，很少有人注意到在行为级别上支付动态更新的正确性，例如，系统在更新后是否按预期运行，以及是否永远不会发生意外行为。我们提出了一个代数方法，指定动态更新和验证其行为的正确性，使用的货架定理证明和模型检查工具。通过定理证明，我们可以证明系统更新后确实满足其期望的性质，并通过模型检查，我们可以检测到潜在的错误。 我们的方法具有一般性，因为：（1）它可以应用于目前DSU系统中主要使用的三种更新模型;(2)它不限于对某些编程模型的动态更新关键词：动态软件更新，代数规范，验证，行为性质1引言动态软件更新（DSU）是一种很有前途的软件维护技术，它可以在不引起停机的情况下更新运行中的软件系统。就像修复一台全速运行的机器一样，动态更新必须具有高度可靠性，以保证系统在更新后的行为符合预期。这是因为需要动态更新的目标系统通常是关键任务系统.他们需要提供24x7的服务，如交通控制系统和金融交易系统。因此，保证动态更新是正确的并且可以正确地对目标系统执行是重要的虽然已经对动态软件更新的正确性进行了一些研究，但大多数都考虑了代码级的正确性[9，22，16]，1电子邮件：{zhangmin，ogata，futatsugi}@ jaist.ac.jp1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2013.02.013M. Zhang等人/理论计算机科学电子笔记294（2013）1213即如何正确部署动态更新，例如，更新的程序是否保持类型安全[9，22]或版本一致[22，16]。动态更新的类型安全 例如，假设数据类型A更新为A更新后，f应该引用新类型A版本一致性意味着新旧版本的过程之间没有错误的调用在过程之间可能有这样的调用，它既不发生在旧版本中，也不发生在新版本中。例如，假设存在过程f（）{g（）;h（）;}，g（）{.} ，并且h（）{...} 在一个老节目中。f和g更新为f（）{g（）;}和g（）{h（）;}。假设更新发生在调用g之前的旧f中。 更新后，新 G被称为。 新的G叫H g返回后，h被老f调用。这样的呼吁应该 在更新时避免。虽然代码级的正确性对动态更新是必要的，但我们认为系统行为级的正确性即使在代码级别正确实现了更新，例如类型安全和版本一致，在执行更新之后，它可能不会使系统表现得像预期的那样。第2节中的动态更新就是这样一个例子，其中运行非法互斥协议的系统被动态更新为正确的系统。在被更新之后，系统应该满足两个期望的性质，即，相互排斥和自由的僵局。然而，更新后的系统满足互斥属性，但可能会导致死锁。这样的更新被认为是不正确的行为。我们提出了一种代数方法来指定动态更新和验证其行为属性。动态更新被建模为观测转换系统（OTS），一种用于以代数方式指定计算机系统的抽象状态机[19]。OTS可以被指定为方程理论和重写理论，分别用于定理证明和模型检查[8，7]。通过定理证明，我们可以证明更新后的系统确实满足了期望的行为特性，通过模型检查，我们为那些不成立的特性找到了反例。反例可以帮助我们更好地理解更新系统的行为，检测动态更新的错误，并最终设计正确的系统。我们的方法从以下两个角度来看是通用的。首先，它可以用来形式化三个主要的动态更新模型，即，中断模型、入话模型和松弛一致性模型（详见2.1节），这些模型在当前的动态软件更新系统中得到了广泛的应用。我们可以在方法中形式化符合三个模型之一的动态更新。其次，我们形式化的设计动态更新，而不是代码，这是不同于其他现有的方法，如，在[12]和[13]中的类C程序中的动态更新的形式化因此，我们的形式主义并不限于在某些程序模型中开发的动态更新本文的其余部分组织如下。第二部分介绍了软件的动态更新.第3节描述了形式化动态更新的方法14M. Zhang等人/理论计算机科学电子笔记294（2013）12第4节描述了行为正确性的验证。第五节讨论了相关的工作，第六节总结了本文。2动态软件更新2.1动态更新模型动态软件更新不同于静态软件更新。后者是一种通过停止运行系统、应用更新然后再次重新启动系统来将软件演化为更新版本的跨平台方法。但是，动态更新支持对正在运行的系统进行即时更新，而无需关闭它们。已经设计并实现了许多系统来支持动态更新软件系统，例如Podus [10]、OPUS[1]、Ginseng [17]、POLUS [6]。它们专门用于对某些类别的软件系统进行动态更新。例如，Ginseng支持对单线程系统的动态更新，而PO-LUS支持对多线程系统的动态更新。两者都只支持对用C语言开发的系统进行时间中断模型旧系统中断更新符合条件的简历新系统更新Replike模型重新链接和转换状态旧系统通知呼叫更新返回新系统更新重新链接和转换状态松弛一致性模型更新线程旧系统中断符合条件的简历新系统更新. ..旧系统重连和转换状态Fig. 1. 三种动态更新模型在动态更新系统的背后是更新模型，它决定了系统可以支持哪些类型的动态更新。Hicks等人根据应用更新的时间将动态更新模型分为两组[14]。一个称为中断模型，另一个称为调用模型，如图1的第一和第二部分所示。在中断模型中，系统的更新可以在系统执行期间的任何时刻开始。系统首先在某个点中断。然后原子地执行更新，最后恢复系统。执行更新的原子性意味着更新不能与程序执行并行执行。更新不一定在中断时执行。它们可能会被推迟，直到满足某些条件。例如，一些动态更新系统禁止更新活动代码（堆栈上的代码）[5]。一些系统延迟了M. Zhang等人/理论计算机科学电子笔记294（2013）1215更新到活动代码，直到它们不活动[21]。然而，向新系统的演进总是在系统恢复之后立即发生。一些动态更新系统是基于中断模型的，例如Podus [10]，Ginseng [17]以及[5，21，20]中的那些与中断模型不同，调用模型需要在系统中静态指定更新点。在更新点，可以调用特殊的更新过程来执行更新。首先通知运行中的系统它应该执行更新。它在到达更新点时调用更新过程，然后执行相应的更新。更新过程重新开始后，系统将从原来的位置继续运行. Replike模型非常适合多线程系统的更新。一个典型的例子是Erlang，它支持基于调用模型的动态更新[3]。松弛一致性模型是中断模型的扩展，如图1中的第三部分所示。它支持多线程系统的动态更新。不同之处在于，松弛一致性模型允许新旧系统的并发活动以及新旧系统状态的共存。在执行更新并恢复运行的多线程系统之后，每个线程可能不会立即执行新代码相反，它可能会继续执行旧代码，并在某个特定的点上进化到新代码。当所有线程都发展到新代码时，更新完成。在POLUS [6]中实现了松弛一致性模型。2.2DSU的行为正确性行为正确性是指系统在更新后的行为必须是正确的。形式上，动态更新是行为正确的，如果系统在被它更新后满足其期望的属性。这些性质依赖于具体的系统，通常描述新旧系统之间的差异。例如，vsftpdFTP服务器的1.1.2版引入了一个限制来自单个主机的连接数量的功能。如果我们将一个运行中的vsftpd服务器从早期版本更新到1.1.2版本，更新后的服务器的一个理想属性是来自单个主机的连接数永远不会超过最大连接数。与代码级正确性相比，行为级正确性同样重要。行为级正确性关注的是如何通过更新来检查待更新系统的行为，而代码级正确性关注的是更新的实现。显然，行为级的正确性依赖于代码级的正确性，而代码级的正确性并不足以保证行为级的正确性。也就是说，即使将更新正确应用于正在运行的系统（没有代码级错误），更新后的系统也可能无法按预期运行。在本节的其余部分，我们将给出一个示例来展示动态更新的行为级正确性。我们考虑一个动态更新的系统运行一个非法的互斥协议（称为协议A的方便）与正确的（协议B）。更新后，系统执行正确的协议。我们设计了一种更新方法，并在松弛一致性模型下实现。16M. Zhang等人/理论计算机科学电子笔记294（2013）12协议A和B的基本思想是，有一个共享的布尔变量锁定指示临界区是否可用。每个进程都在前临界区（ps）等待进入临界区（cs），直到locked变为false。它将locked设置为true，并进入临界区。它在离开临界区时将locked设置为false。不同之处在于，在协议A中，检查locked的值和设置lockedtrue是两个独立的操作，而在协议B中，它们被视为原子操作。众所周知，协议A不满足互斥性质。我们考虑一个动态更新来强制一个运行协议A的系统来执行B协议如图2所示，在松弛一致性模型中执行更新。在旧系统中有多个进程执行协议A。在某个时刻，系统被中断，并执行更新。在发生中断的状态下，协议B中的锁定值（由锁定B表示）被分配有协议A中的锁定值（由锁定A然后，系统恢复。如果进程位于协议A的剩余部分rsA，则它停止执行协议A，而是从开始的rsB开始执行协议B。否则，进程将继续执行协议A，直到它返回到剩余部分。在所有流程演进之后，更新完成。此后，所有进程都运行协议B。从那一刻起，系统被假定满足互斥性质。在第4节中，我们将证明该财产确实有效。然而，我们也发现了一个反例，表明系统更新后可能会导致死锁。从这个意义上说，更新不能被视为行为正确。3动态更新在形式化方法中，软件系统通常被形式化为变迁系统，由状态集S和变迁的二元关系→S×S组成。观测跃迁系统（OTS）是跃迁系统的一种代数形式。一个OTSS是一个三重的O，I，T，O，由一组O个观察者，I个初始状态和T个转换组成。 每个状态由O中每个观察者返回的值标识。如果两个观测器返回相同的值，则两个状态1，2相等。OTS中的状态是归纳定义的。假设a是a时间中断没有更新恢复旧的进程新工艺更新锁定A图二、从协议A到B的动态更新条件输入一个退出A演化PSAPSA设置锁定BpsAcsArsA退出A进化进入BCSACSAcsArsArsB进入B退出BrsA...rsArsArsBcsBM. Zhang等人/理论计算机科学电子笔记294（2013）1217状态对于每一个t∈ T，t（t，. . ）也是一个国家，其中... 表示其他参数。关于OTS的定义和应用的更多细节可以参考[19]。我们把运行系统的动态更新看作是从旧的运行系统向新的目标系统演化的过程。进化可以分为分为三个步骤。在中断模型和松弛一致性模型中，三个步骤是：中断旧系统，当条件满足时更新，恢复系统。在调用模型中，它们是通知调用更新，调用更新过程，并从调用返回。一般来说，我们认为它们是准备，更新和完成。这三个步骤将新旧体制的演进分为四个阶段，即：预更新、等待更新、更新和后更新，如图2所示3 .第三章。在预更新阶段，执行旧系统。在调用模型中，它在等待阶段继续运行，但在其他两个模型中停止。在等待阶段满足某些条件时执行更新。在被更新之后，演化进行到更新阶段，在该阶段中，系统等待被恢复（在中断和松弛一致性模型中），或者等待从更新过程返回（在调用模型中）。然后，系统进入更新后阶段，其中可能执行一些延迟的更新。最后，系统向新的方向发展我们声明了一个观察者来表示这四个阶段，并通过三个过渡形式化了这三个步骤设U是四个阶段名称的集合，即，{预更新，等待，更新，后更新}。我们声明了一个观察者阶段，它返回给定状态下的演化阶段。这三个步骤由准备、更新和完成三个转换定义。我们以准备的定义为例。 在一个状态下，准备发生的一个条件是，处于预更新阶段，即，phase（phase）=预更新。准备工作完成后，进化进入等待阶段。也就是说，prepare（准备）中的phase的值是等待。动态更新可以通过两个OTS的联合来形式化，这两个OTS表示具有三个转换和观测器的旧系统和新系统。假设新旧系统分别由两个OTSSO和Sn形式化，使得SO=<$Oo，Io，To <$，Sn=<$On，In，Tn<$.从So到Sn的更新可以形式化为Su=Ou，Iu，Tu，其中：• Ou Oo On {phase}• Iu{0|{0∈ I0{0}=预更新}• Tu To Tn {prepare，update，finish}时间行动准备更新完成旧制度新制度正在运行正在运行相预更新后更新图3.第三章。四相系统的动态更新演化中断否则磨合等待语音模式更新18M. Zhang等人/理论计算机科学电子笔记294（2013）12出口A，ppcA[p]：pspcA[p]：rs等待A，p输入A，ppcA[p]：cs准备准备准备phase：waitinglockedA：falsephase：waitinglockedA：false权限更新更新phase：waitinglockedA：true更新lockedB：falselockedB：false阶段：更新阶段：更新完成阶段：更新后pcA[p]：ps完成锁定B：true阶段：更新完成输入A，p出口A，p阶段：更新后pcA[p]：cs阶段：更新后pcA[p]：rsevolvepcB[p]：rsB出口输入Bpc[p]：csB我们假设OoOn=且ToTn=。这个假设可以通过重命名观察者和转换来实现，如果它们的交集不是空的。To中的跃迁可以发生在更新前和更新后阶段，而Tn中的跃迁只发生在更新后阶段.Tn中的过渡从旧系统演化的状态开始。我们考虑协议A到B的动态更新的形式化作为一个例子。OTS的一部分如图4所示。每个圆圈代表一个国家。在每个状态下，由转换引起的值在圆圈旁边给出。例如，（pcA[p]：rs）表示在状态下进程p位于协议A中的剩余部分每个箭头表示一个带有转换名称和适当参数的转换例如，（enterA，p）表示进程p进入临界区。OTS是分别形式化协议A和B的两个OTS的联合。它包括形式化更新过程的三个过渡和形式化更新后阶段中每个过程的演变的过渡演变。4规范和验证我们可以通过现有的代数语言和验证系统来指定OTS并验证其所需的属性。CafeOBJ就是这样一种语言，其中OTS被定制为指定的[19]。CafeOBJ也是一个强大的重写系统，经常被用作证明助手[8]。 我们还可以将OTS的CafeOBJ规范转换为Maude [23]，Maude是CafeOBJ的兄弟代数语言，但支持模型检查[7]。我们可以用生成的Maude规范对OTS的期望属性进行模型检查。图四、从协议A到B动态更新的图形OTSM. Zhang等人/理论计算机科学电子笔记294（2013）12194.1通过定理证明进行验证在CafeOBJ中，对象是按排序分类的。sort表示一种对象。例如，sortBool表示一类布尔值true和false，它们由Bool的两个常量true和false表示。在本文中，我们使用Sys，Pid和Label来表示系统状态，进程和程序计数器的类，如rs，ps和cs（分别由常数rs，ps和cs表示观察者和转换由运算符表示例如，transition wait A由op wait-A：Sys Pid ->Sys声明，其中op是声明运算符的关键字。运算符的含义由方程定义我们以定义为wait-A和pc-A的方程为例。ceq pc-A（wait-A（S，I），J）=（如果I = J则ps elsepc-A（S，J）fi），如果c-wait-A（S，I）。S是Sys的变量;I和J是Pid的变量。关键字ceq用于声明条件等式。OTS的CafeOBJ规范用于通过证明分数证明不变属性[11]。我们首先指定要证明的属性，然后通过交互式地使用CafeOBJ作为证明助手来组成证明分数我们证明了系统在通过第2.2节中的方法更新后满足互斥性质，即，对于P中的任意两个过程p1，p2和P中的每个状态p1，p2，pcB（p1，p1）=cs和pcB（p1，p2）=cs，意味着p1=p2. 也就是说， 在任何状态下，如果在临界区有两个演化过程，它们必定是同一个。互斥属性可以由谓词mu表示，其声明和定义如下：操作：系统PID PID ->布尔等式mu（S，I，J）=（pc-B（S，I）= cs和pc-B（S，J）= cs）意味着I = J。我们通过CafeOBJ成功地证明了更新后的系统确实满足互斥特性。证明是基于结构归纳法。证明中需要三个引理。由于篇幅所限，我们省略了证明的细节。4.2通过模型检查进行然而，某些属性可能无法通过更新的系统来满足。在这种情况下，需要用这些性质的反例来反驳被验证的性质。我们可以在Maude中指定OTS作为重写理论，并使用所需的属性对其进行模型检查。在Maude中，OTS的状态由一组值指定。每个值都表示为一个分量，一组分量称为一个构造。例如，S1中的每个状态由锁定A和锁定B的布尔值、表示更新阶段的值、每个过程的pcA和pcB我们考虑一个具有两个过程p1和p2的系统的例子.p1和p2由两个常数p1和p2表示20M. Zhang等人/理论计算机科学电子笔记294（2013）12C1C3C5颈7p1 p1输入A更新退出AP2进化P1等准备恢复P1进化c0c2c 4c6c8的Pid。一个状态由一个模式的配置表示，（锁定-A：Q）（锁定-B：Q）（相位：Q）（pc-A[p1]：Q）（pc-A[p2]：Q）（pc-B[p1]：Q）（pc-B[p2]：Q）（演化[p1]：Q）（演化[p2]：Q），哪里每个Q保持在特定状态下的对应值，并且组件由空的关联和交换运算符连接。转换由重写规则表示例如，转换更新可以通过以下重写规则指定rl [update]（locked-A：B）（locked-B：B ' ）（ p h a s e ： w a i t i n g ） = > （ l o c k e d -A ： B ） （ l o c k e d - B ： B ） （ p h a s e ：u p d a t e d ） .关键字rl用于声明规则。rl之后是规则的名称。B和B左手边是一个图案。任何与模式匹配的配置或段（配置中组件的子集）都可以通过规则重写。右边是模式被重写的结果。其他转换也可以指定为重写规则。作为一个例子，我们使用Maude LTL（线性时序逻辑）模型检查器[7]验证系统从协议（A）更新到协议（B）时的无死锁特性。因为模型检查要求系统的状态空间如果是有限的，我们通过固定系统中进程的数量来使它有限。我们考虑系统中只有两个进程的情况，这在上一节中详细说明。我们首先将死锁自由属性指定为LTL公式。 两进程系统中的死锁是指两个进程在执行协议（B）时都处于剩余部分，但锁B的值为真。两者都不能进入临界区。 我们宣布两个命题为“否”？并锁定？. 给定一个进程I和一个配置，@rs？(I)为真，如果配置包含（pc-B[I]：rs），否则为false。锁上了？ 为真，如果configuration包含（locked-B：true），否则为false。无死锁属性由公式[]~@rs定义？(p1)/\@rs？(p2)/\locked？，其中[]对应于LTL中的全局算子G，〜，和〜。Maude返回了一个违反公式的反例反例如图5所示。每个圆圈代表一个配置，箭头表示所应用规则的名称我们只显示了规则改变的每个配置中的那些组件存在一条从由c0表示的初始状态到由c8表示的状态的路径，在该状态下发生死锁pc-A[p1]：ps locked-A：falselocked-A：true阶段：等待pc-A[p1]：cs阶段：更新后pc-A[p2]：rspc-B[p1]：rspc-A[p1]：rs locked-A：falsepc-A[p1]：cslocked-A：truelocked-B：真相位：已更新pc-A[p1]：rslocked-A：falsepc-B[p2]：rspc-B[p1]：rs图五、动态更新无死锁性的一个反例从反例中，我们可以了解为什么所需的属性失败，M. Zhang等人/理论计算机科学电子笔记294（2013）1221重新设计更新的可能解决方案。例如，上面的反例显示了死锁发生的原因是当更新发生时，lockedB的值被设置为true。有两种可能的解决办法。一种方法是设置一个更新点，其中lockedA为false，并在invoke模型中执行更新。另一种选择是强制锁B为假，而不管在中断模型中发生更新时锁A5相关工作在早期的研究中，Gupta等人将有效性的概念引入动态更新[12]。非正式地说，如果新系统中的可达状态最终可以从旧系统中发生更新的状态到达，则更新被称为有效。然而，有效性的定义，如海登等人所观察到的， 既有限制，又有宽容[13]。他们建议定义动态更新的正确性由具体动态更新的属性确定[13]。在我们的工作中，我们显式地将属性称为行为属性，以将它们与代码级属性区分开来。动态更新的形式化有多种方法。在[13]中，动态更新通过合并转换合并新旧版本的C程序来形式化。在[12]中，程序被视为状态机。然而，他们的方法仅限于具体的程序模型，如[13]中的模型。Bierman等人提出了一种用于形式化动态软件更新的更新演算[4].演算是可扩展的，并且独立于程序模型。然而，它们不提供基于其形式化的任何验证支持。Stoyle等人提出了Proteus，这是一种对动态软件更新进行建模的核心演算[22]。但他们用它来检查代码级的正确性。上述大多数形式主义，除了[4]只适用于单线程系统的更新，不适用于分布式系统的更新。Anderson为并发程序的行为属性提供了安全动态更新的定义[2]。然而，在定义中只考虑类型安全属性。在我们的方法中，我们专注于新旧系统和更新的设计，这使得我们的形式化方法更一般，但不限于某些编程模型。6结论和今后的工作我们引入了动态更新行为正确性的概念，并通过一个具体的例子说明了这种需求。如果在执行动态更新后必须发生预期行为，则动态更新称为行为正确。我们提出了一种代数方法来指定动态更新和验证其行为属性。该方法可应用于三种动态更新模型的形式化，这三种模型在动态软件更新系统中被广泛实现与大多数现有的形式化的动态更新，我们的方法并不限于在某些程序模型中开发的动态更新。通过我们的形式化方法，我们可以验证22M. Zhang等人/理论计算机科学电子笔记294（2013）12使用现成定理证明和模型检查工具的动态更新的行为特性。通过验证，我们可以证明所需的属性确实存在，或者检测动态更新的潜在错误并找到可能的解决方案。在正在进行的工作中，我们计划将我们的方法应用于更复杂的动态更新的验证一个候选者是从非法认证协议NSPK（Needham-Schroeder公钥协议）[18]到其修改版本NSLPK [15]的更新（已被验证为满足相互认证属性）。感兴趣的性质是，在被更新之后，系统应该满足相互认证性质。引用[1] Altekar，G.，I. 巴格拉克山口Burstein和A.Schultz，Opus：在线安全补丁和更新，在：第14届USENIX Security，2005年，第14页。287-302[2] 安德森，G。一、并发程序行为特性的动态软件更新，在：2011年，Grace Hopper庆祝计算机领域的女性[3] Armstrong，J.，R.维尔丁角Wikstr，M. Williams等人，“Concurrent programming in ERLANG,”Prentice Hall,[4] Bierman，G.，M. Hicks，P. Sewell和G. Stoyle，Formalizing dynamic software updating，in：2ndUSE，2003。[5] Boyapati角，B.利斯科夫湖Shrira等人，在持久对象存储中的惰性模块化升级，，38，ACM，2003，pp.403-417[6] 陈洪，J.Yu，C. Hang等人，使用松弛一致性模型的动态软件更新，IEEE软件工程学报（2011年），pp。679-694.[7] Cl avel，M.，F. 杜然等人， Alla boutMaude，LNCS4350，Springer（2007）.[8] 迪亚科内斯库河和K.Futatsugi，[9] Duggan，D.，运行模块的基于类型的热交换，，36（2001），pp.62比73[10] Frieder，O.和M. Segal，On dynamically updating a computer program：From concept to prototype，Journal of Systems and Software14（1991），pp.111-128[11] Futatsugi，K.，在IEEE 2006年的第21届ASE中，第2006页，三比十[12] Gupta，D.，Jalote和G. Barua，A formal framework for on-line software version change，IEEETransactions on Software Engineering22（1996），pp.120-131[13] 海登角，S. Magill，M.希克斯等人，验证和验证动态软件更新的正确性，在：第四VSTTE，LNCS 7151，2012，pp. 278-293。[14] 希克斯，M.和S.Nettles，Dynamic software updating，ACM TOPLAS27（2005），pp.1049-1096[15] Lowe，G.，对Needham-Schroeder公钥认证协议的攻击，信息处理信件56（1995），pp.131比133[16] 内姆丘岛M. Hicks，J. Foster等人，版本一致的动态软件更新和安全并发编程的上下文效应，43，ACM，2008年，pp. 37比49[17] 内姆丘岛M. W. Hicks，G. Stoyle等人，Practical dynamic software updating for c，in：PLDI（2006），pp. 72比83[18] 尼达姆河和M. Schroeder，Using encryption for authentication in large networks of computers，CACM21（1978），pp. 993-999[19] Ogata，K.和K.Futatsugi，OTS/CafeOBJ方法中的证明分数，FMOODS（2003），pp. 170-184.M. Zhang等人/理论计算机科学电子笔记294（2013）1223[20] 西 格 尔 ， M. 和 O. Frieder， On-the-Money Program Modification： Systems for Dynamic Updating，Software，IEEE10（1993），pp. 53比65[21] Soules，C.，J. Appavoo，K. Hui等人，在线重构的系统支持，见：2003年USENIX技术会议论文集，2003年，pp. 141-154。[22] Stoyle，G.，M. Hicks，G. Bierman等人，Mutatis mutandis：safe and predictable dynamic softwareupdating，ACM TOPLAS40（2005），pp.183-194.[23] 张 ， M. ， K. Ogata 和 M. Nakamura ， Translation of State Machines from Equational Theories intoRewrite Theories with Tool Support，IEICE Transactions on Information and Systems94-D（2011），pp. 976-988.
我的内容管理
展开
