状态图扩展中的行为细化和兼容性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记295（2013）65-78www.elsevier.com/locate/entcsStatechart扩展的行为细化和兼容性Christian Prehofer1LMUMünchen和FraunhoferESKMünchen摘要我们比较了系统模型的细化和兼容性的概念及其被描述为状态图的变体兼容性，在可替代性的意义上，意味着一个系统可以在任何使用原始系统的地方使用。我们表明，现有的定义细化和兼容性是正交的，如果他们包括一个接口扩展。然后，我们关注扩展的兼容性，这意味着即使使用了新添加的功能，系统也会在一段时间后返回到兼容行为我们的新结果显示了在什么条件下使用新添加的功能保留行为。更具体地说，我们在跟踪级别上执行一种新的消除新添加的行为的方法。通过这种方式，即使新添加的功能使用现有的输入和输出事件，我们也可以实现扩展的兼容性，这对于现有的抽象和细化概念是不可能的关键词：状态图，行为细化，语义细化，兼容性，基于模型的开发1介绍在本文中，我们专注于系统模型的细化和兼容性及其表示为状态图的变体。这个想法是从一个基本模型开始，然后通过添加新的状态和转换来增量地添加小功能。状态图模型的这种迭代和模块化开发可以用于建模变化和可选功能，例如[10]中所讨论的这里解决的问题是这种扩展的兼容性，即在扩展系统时是否保留旧的行为。在语义细化方面有大量的工作，这是在保留原始模型行为的同时添加细节的过程。因此，保持行为意味着精化模块（的指定）隐含着原始模块。 在我们的设置中，我们考虑输入和输出行为的可观察的痕迹细化被建模为痕量包含。这意味着所有的痕迹（即，所有可能1电邮地址：Christian. esk.fraunhofer.de1571-0661 © 2013 Elsevier B. V.在CC BY-NC-ND许可下开放访问。http://dx.doi.org/10.1016/j.entcs.2013.04.00666C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65′′（）如果我们可以用A替换A在任何现有的实现上下文中，SetAl（x）/set（x）报警关闭报警设置AlOff/AlOff/DoAlarm TimerEvent（）/c：=0TimerEvent（）/c++Snooze（）/c++ if c3DoSnoozeFig. 1. 由Snooze行为）在原始系统中也必须是可能的。请注意，这与自动机的其他工作不同，例如模型检查，例如[9，5]，其中考虑了内部状态转换。从精炼中，我们也想得到一个相容性的概念如果A扩展到A，则A是相容的行为不会改变。 这也被称为替代性。例如，考虑经典堆栈的例子。假设我们有一个堆栈数据结构，其中我们添加了一个计数器，用于维护堆栈中当前元素的数量。这样的新特性显然是一种改进，因为它保留了行为，并且也是兼容的。通常，细化会添加内部实现细节，但也可能扩展输入/输出接口。后者意味着添加新的输入和新的输出事件。然后，抽象或隐藏被用于将细化与原始系统相关联。在大多数情况下，这些抽象只是删除这些新事件，参见例如[16][11][13][4]。在堆栈加计数器的例子中，这产生了兼容性。在接口扩展的情况下，我们将证明现有的细化和兼容性概念其他细化概念仅在不使用新特性时才意味着兼容性（其他一些情况不适用）。因此，我们详细比较了细化和相容的概念。然后，我们开发了新的概念和标准，使我们能够推理系统扩展的行为，即使在使用新添加的功能时。与现有的工作相比，我们不假设新的功能只使用新的，不同的输入和输出事件。例如，考虑一个闹钟，它被一个贪睡特性扩展，如图1所示。按照惯例，我们以粗体文本和粗线显示新特性的添加元素（这里是Snooze）。在闹钟的情况下，贪睡功能禁用闹钟，然后在短时间内重新启动闹钟。虽然这会局部修改行为，但不会影响未来的行为。请注意，新功能在DoSnooze状态下使用TimerEvent输入事件，该事件已在基本功能中使用。 因此，剥离o从观察到的痕迹中获得新事件（这里是“打盹”），就像在现有的细化关系中所做的那样，是不够的。在上面的示例中，Snooze扩展更改了状态图中的控件流，但很容易看出该扩展保留了原始行为。现有的工作基本上是通过不同的新事件来区分新旧行为。然而，这通常是有限的，如在这个例子中。在许多情况下，C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6567push（a）/s：=a：ss：=>eStackneStackpush（a）/s：=a：spop（）/联系我们_Englishpop（）/s：=lt;>]top（）/return（a），s：=a：s图二. Stack示例可能需要使用基本系统中的现有事件的输入，例如来自标准键盘的数字输入。类似地，假设用户应该总是具有通过“退出”键取消特征的选项。那么这个键也应该可以在新特性中使用，这意味着简单地将旧事件和新事件分开既不可取也不可能。对于这样的扩展，它使用旧的和新的事件，我们将显示当兼容性是可能的。我们开发了新的改进概念，通过从输入和输出行为中删除元素来消除新添加功能的影响。我们的主要结果是对这种消去的精确定义和一个新的结果，表明在这种消去下行为何时保持不变。即使一个新特性被使用了几次，我们也可以证明在使用之后行为会被保留。有趣的是，细化和兼容性的概念在几个现有的作品中都有涉及，这些作品来自不同的研究领域，使用类似的基于自动机的人工制品。这包括基于模型的开发[13][8][12]，模型检查和形式化方法[4][17]，对象生命周期建模[14]和UML建模[15][10][16]，包括面向方面的建模[17]。此外，接口自动机的工作考虑了两个自动机之间兼容性的不同概念[1，5，2]，重点是输入/输出兼容性。然而，上面的工作并没有捕捉到兼容性的概念和这里的结果。在下一节中，我们将介绍状态图的概念。然后，我们回顾并比较第3节中添加或修改行为的状态图的兼容性和细化概念。在第4节中，我们介绍了我们的新概念消除下的细化，其中新添加的功能可以在保留行为的同时使用。2状态图模型我们用状态图对软件系统进行建模，状态图描述了软件系统的可能行为。请注意，我们使用了一种非常简单的状态图形式，没有并行和分层状态。图2中的状态图就是一个例子，它描述了堆栈的基本功能。我们有两个状态，一个是空栈，另一个是非空栈。更准确地说，状态图包括(i) StatesSt，with some initial statesSti68C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65=∞∞=阿吉（）/[]输入i，输出o。如果s是初始状态，我们只写（i，o）∈S。（）●∶∶pop∶top（）产生输出return（4）∶return（ 5）。∶消除元素的在从我和O+我的工会不相交的集合。（）/（）∶（）∶（）∶′●类似地，（i，o，s）deno′tesh′在状态s处是用产生h的输入i来实现的(ii) 输入事件I(iii) 输出事件O(iv) 内部变量V，具有初始值(v) 一个过渡关系tr St，I，V，St，O，V我们使用事件动作条件表示转换。转换可以由外部事件启动，这里是event（）。它可能有一个条件，它可能有一个行动，它启动。此操作描述由转换触发的行为。请注意，所有三个标签都可以是空的。在触发事件被省略的情况下，我们有一个没有外部事件的内部跃迁，也称为自发跃迁。有关详细信息，请参阅[13][8]。我们的语义模型建立在[13][8][12]中的工作基础上，并采用了系统的外部黑盒视图。它基于触发转换的外部事件跟踪。只考虑观察到的输入和输出事件，而不考虑内部状态。一个可能的运行可以通过事件的跟踪和状态图的结果输出来指定。我们使用来自[ 13 ][ 8 ][ 12 ]的松散的跟踪集合包括状态图中指定的转换的任何可能的跟踪。此外，任何未指定的事件，例如在当前状态中没有定义转换的事件，都会使状态图处于混沌状态，并且在此之后允许任何行为请注意，我们的状态图模型允许一个非确定性的选择，如果几个转换是可能在一个状态，这只是一个特殊的情况下，松散的语义。形式上，我们假设迹（i，o）在I和O上的有限流和无限流上，记为IΩI和OΩO。对于状态图S，如果存在从状态开始的迹，则我们写（s，i，o）∈S输出o，以及（s，i，o，s），如果s可以从s到达，输入i和输出o。我们在流上使用以下符号：ss连接两个流，其中s被假设为有限。as通过附加流s从元素a创建流。此外，first s是流s的第一个元素。 例如，在图2的示例中，输入推5推 4顶我们假设一个具有即时反馈的语义[13]，这意味着发送到状态图本身的信号在从外部获取新信号之前立即被处理。对于不同状态图语义的全面处理，请参见[6]。状态图可能是非确定性的。我们称之为规格不足，这使得细节有待进一步的实施决策。例如，在图2中，没有指定eStack状态中的top事件会发生什么请注意，我们的语义是完全的，即它为任何输入指定了一些输出。Un-C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6569′i/In，o/On）<$（i，o）∈S}<$S.′（）下′{（′ ′ ′=′+′+′ ′′I和输出O。 假设一个规格S经由I和O扩展了I和O，与其他形式化一样，并不是某些输入的行为是未定义的或不允许输入。如果某个输入的行为在某个状态下没有在状态图中指定，则允许任何行为（即任何输入的任何输出）。在这种情况下，状态图保持这种状态。 这种语义特别适合于细化和逐步的系统开发-对于实际的实现，最终必须减少这种非确定性。3语义修饰与相容性在本节中，我们比较了细化和兼容性的概念。兼容性意味着一个新的、改进的系统可以在旧系统所在的任何地方使用，并以同样的方式运行。这里的兼容性不仅仅是语法接口的语法兼容性。对于状态图S，我们说S′是S的扩张，如果(i) 它扩展了输入和输出事件，(ii) 可以添加内部变量，(iii) 通过添加和删除状态和转换来修改行为通常，扩展添加或扩展一些功能，因此当我们提到添加的功能时，我们会提到扩展中的新功能。一般来说，我们允许移除转换，因为如果存在其他选项，它可以通过消除选项来减少非确定性。我们说状态图S′与S相容，如果(i) 接口兼容，(ii) 如果使用S而不是S，则S的行为相同（即，不使用可能添加的特征）。一般来说，如果原始行为在某种抽象或映射下被保留，则使用术语细化。以下定义通常用于痕迹的细化，稍后将进行扩展假设一个规范S以输入事件上的一组（i，o）对的形式分别I′I In，O′isO On。则S′是S的精化，如果基本上，这个定义从S的扩展轨迹中剥离了添加的输入和输出事件，这在S 中必须已 经是可能的。这个定义在现有文 献中使用类似， 例如[13][11][16]和[4]中的预测形式，并且[12]中没有消除新事件其他精化的概念明确地假设S中具有特定行为的每个i，o对都被精化，并且在S在我们的例子中，这是不需要的，因为行为是完全定义在任何输入上的。对于S的特定输入，可以有几个可能的输出，但至少有一个必须在S中保留或细化。这被认为是非决定论的简化。这种细化概念的一个例子是栈的扩展70C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65（）′push（a）/ s：=a：s，c++s：=零，c：=0eStackneStackpush（a）/ s：=a：s，c++size（）/pop（）/has_size（c） s：=>;c--[s=a：：>]pop（）/s：=lt;>] top（）/return（a）s=a：ssize（）/has_size（c）图三. 带计数器的如图3所示，通过计数器。计数器不会修改堆栈的行为，它只会在size事件发生时产生额外的输出。因此，这种改进也是兼容的。3.1优化VS兼容性根据以上定义，我们现在可以更详细地比较这两个概念。细化的概念意味着添加实现细节，这在理想情况下应该意味着兼容性。如果扩展不扩展接口（即输入和输出事件），则在上面的细化定义中反映了这一点由于我们的状态图是非确定性的，但对于任何输入都是完全定义的，因此细化可以删除选项，但不能对某些输入进行细化。因此，在相同接口的情况下，细化是简单的跟踪包含，这意味着在我们的设置中的兼容性。然而，在许多情况下，参见上面的示例，接口扩展是可取的，并且在文献中使用。这导致了两个属性是独立的情况。我们将在下面说明这一点。首先，考虑图1的示例。很容易看出扩展是兼容的，但它并没有被上面的兼容性定义所捕获。如果在现有上下文中使用，则不会发生Snooze事件，并且其行为与原始版本相同。该定义不适用的原因是在扩展中使用了旧事件。在使用Snooze特征的情况下，它可以使用TimerEvent事件，该事件不是新事件并且在上述S到S跟踪的减少中没有被消除。因此，上述细化的定义并不适用。其他形式化，例如[8][12]，简单地假设使用新特征（具有新事件）导致混沌状态（没有消除新事件）。因此，细化适用，但一旦使用了新的功能，就没有更多的属性。为此，我们将使用扩展兼容性的概念，它允许使用新功能。其次，我们应该注意到，上述细化概念并不意味着兼容性。扩展可以添加新事件的附加输出，即使新输入事件未被使用。因此，兼容性丢失，因为这些事件在原始版本中未被预期或未被定义一个简单的示例是日志记录特性，它不接受新的输入，但创建输出事件，如图4所示，作为堆栈的扩展。C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6571A a /aBC/′∶∶∶=∶s：=无push（a）/s：=a：seStackneStackpush（a）/s：=a：spop（）/log（s），s：=>[s=a：：>]pop（）/log（s），s：= lt;>] top（）/ return（a）s=a：：sb /b见图4。 通过日志记录a/ab /bd /d图五. 简单扩展3.2精化概念与非决定论下面我们讨论上述细化概念的另一个局限性。技术问题涉及到我们的方法在混沌语义。虽然混沌语义已经被证明是非常有价值的逐步细化作为减少非确定性[13][12]，如果状态图进入混沌状态，而遍历扩展功能会发生什么考虑图5中的示例。基本状态图实际上是确定性的，并且在输入a和b上完全定义。 考虑输入Ica cBX. 在在这种情况下，扩展状态图到达状态C，然后进入混沌状态，因此输出完全未知，所有跟踪都被允许。 另一方面，在一项研究中，如果我们从I c中消除新的输入事件c，我们得到b...得双曲余切值.基本自动机产生规则的预期结果。因此，上面的加细定义，类似于[4][13]中的定义，不足以在这里表达加细。类似的例子可以在没有混沌状态的情况下产生-例如。如果我们将图5中的例子中的d/d'转换修改为ba。然后，消除新的事件在IC产生的行为是从原来的一个不同的。一个可能的补救办法是假设扩展是完全定义的，并且是完全确定的。然而，这不允许连续的细化步骤。4消除扩展兼容性在下文中，我们将介绍一种新技术，通过在跟踪级别上消除新添加的行为来显示兼容性。通过这种方式，我们可以实现扩展的兼容性，并解决现有细化概念的局限性。正如上一节所讨论的，如果新添加的特性使用了一些现有的输入或输出消息，那么兼容性的定义就不够了。为此，我们使用扩展兼容性的概念，它被定义为具有附加前提的兼容性，即即使使用新功能，72C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65（）下一页在下面的例子中，我们用向量（I，O）来表示S，其中SetAl（x）/AskTimeTime（t）/SetTimerEvent（t）报警关闭报警设置AlOff/AlOff/DoAlarm TimerEvent（）/c：=0TimerEvent（）/ c++Snooze（）/AskTime; c++ if c3AskSnoozeSetTime（t）/SetTimerEvent（t）DoSnooze见图6。 通过Flex-Snooze系统在一段时间后返回到兼容行为。更准确地说，在跟踪方面，这意味着扩展状态图的跟踪，其中新的输入事件发生无限次，对应于新功能的使用。然后消除新的行为（定义如下）产生原始行为的痕迹。我们将在下面正式说明。扩展到具有事件（In，On）的状态图S。′这里我们假设一个新的特征是由一个新的事件（形式化为S-1）发起的下面触发），然后可以使用来自现有输入和输出I、O的事件。通常，一个新的功能需要从键盘输入，这会从现有的事件集合中创建一个事件。类似地，假设用户应该总是具有通过中止键取消特征的选项。 那么这个键也可以用于新的特性，这意味着简单地将新事件和旧事件分开是不可取的。这里的一个例子是警报加FlexSnooze。当闹钟响起时，用户可以按下贪睡按钮，然后通过键盘输入指定贪睡时间的长度。这在图6中示出。在本例中，新功能由新信号触发，但随后也使用现有信号。我们认为这是一个非常典型的情况下，如果典型的输入方法和信号被重用。例如，读取键盘输入（如参数）或标准输入方法（如取消或返回）。在这里，从新输入（这里是Snooze事件）中抽象出来是不够的，因为新功能还使用现有的输入。我们在下面提出了一种形式主义，以消除新添加的功能的行为，并进一步表明，当原始行为可以建立，即使在功能已经使用。虽然从上面的例子看起来很直观，可以建立这个属性，但在一般情况下，我们必须考虑以下几点：自动机在遍历扩展特征时可能会进入混沌状态。在上面的例子中，新状态AskSnoozeSet和DoSnooze中的未指定输入将导致这种混沌行为。● 自动机可能会在新的扩展功能中循环，并且可能不会返回。●C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6573●′′′∈（′）′（）∈假设一个S′触发的从S到S′的扩展。一个谓词el（i，o）over two==== ∶ ∈/（）下在S中兼容，如果所有从s和s的S中的状态是相同的。流i和o在以下前提下被称为消元：el（i，o）保持i，产生输出O。定义中的最后一项确保S不能去自动机可以是非确定性的，无论是在原始的和扩展的部分。关于第一项和第二项，我们观察到扩展功能是由一个新事件触发的，因此这可以被视为一种细化，因为之前没有指定然而，现有的细化定义只是从观察到的行为中排除了新的事件这对于这里考虑的情况是不够的在下文中，我们准备定义我们的新概念的消除。我们定义一个从S到S的扩展为S触发的，如果以下属性成立：(i) 仅添加新状态和这些状态上的新转换。(I.e.至少开始或结束是一个新的状态）。(ii) 从旧状态的新转换总是由新事件触发的（而不是在S）。S触发特别意味着不添加旧状态之间的新转换，也不删除或限制现有转换。这个条件对于消除添加特性的影响很例如，一个只添加日志记录输出而不添加新的转换或状态的日志记录特性就不在这里讨论。图1和图6中的报警示例是S触发的。对于从S到S′的扩张，我们定义了两个wostate′s和s′to benext step形式上，对于所有iI，S，I，O，S我，我提供sS.例如，在图5中，状态DoAlarm、AskSnoozeSet和DoSnooze是下一步骤兼容的，因为它们经由AlO返回到原始状态图中的相同状态（AlarmO）存在S中的状态s，其中（s，i，o，s）使得(i) s和s′在S或s′s中是下一步兼容的，(ii) i的形式为i i0 i′，其中i0在I中。(iii) 当输入i在状态s上时，S ′不会进入混沌状态。例如，在图6中，考虑跟踪T（SetAl（）：Time（x）：TimerEvent（）：Snooze（）：Time（y）：A10超时，AskTime：SetTimerEvent（x）：AskTime：SetTimerEventy（y））。目标是消除新的Flex-Snooze功能的影响。对旧状态图的相应遍历是Tel（SetAl（）：Time（x）：TimerEvent（）：A10事件，AskTime：SetTimerEvent（x））在这个例子中，我们有el（Snooze（）：Time（y），AskTime：SetTimerEvent（x）），它描述了我们要消除的新行为非正式地说，eli，o成立，如果有一个遍历通过扩张，其中ich包含i，74C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65′′∣我们将el定义为el在迹（i，o）上的扩张，其中el保持并且可以∈（）′∈（）∈一个bove定义意味着（sS，ils，ols）∈S，这意味着至少有一个可能的已应用新输入事件的所有位置，以在存储器中进行I/I操作，从而避免丢失（）∈（∶′）∈′（）如果i∈S，first（il）∈S/S，（i，o）是S中迹，且存在il1，il 2，ol 1，ol 2，使得我们定义为一个病毒的修正，它不是一个从S到S的消除，如果我们定义从S到S′的一步精化和消去el，如果输入到S在输入端消去的情况下，导致S中的相同状态，稍等S的行为被保留。由于S可能是不确定的，因此需要输入i的混沌状态。注意，我们不能消除来自三个下一步骤兼容状态的A10跳变，因为它也发生在基本状态图的对应迹线如果S是S的扩张，我们用s S表示状态s对S的状态和变量的限制。这可以对S中不存在的状态进行定义。在重症在这种情况下，Wer i t e（i l，ol′）∈el（ie l，oe l）。形式上，el（i∶∶il，o∶∶ol）保持不变il=il1∶∶il2，ol=ol1∶∶ol2，以及el（il1， ol1）和el（il2， ol2）根据上面的例子，我们有了所需的Telel T请注意，el是部分定义的，例如，在这些新元素不能完全消除的情况下。(E.g.在Flex-Snooze情况下，跟踪可能在Flex-Snooze部分内停止，这意味着不能完全删除此功能的影响从机翼下保持。假设u∈（i∶∶ils，o∶∶ols） ∈S，其中i∈（In/I）且存在ie，ol（i，o）∈el（i，o）成立，且ils∈IΩ。 则（il∶∶ils，ol∶∶ols）∈S.该性质表明S'在输入i之后保留序列ils上的行为，该输入i使用S'的新特征。这意味着扩展的兼容性，因为在使用新功能后，在可观察的痕迹方面的行为完全保留。我们的目标是定义简单的标准，以建立行为细化。为此，我们首先定义一个单步细化。如果（s，iel∶∶ils，oel∶∶ols）∈S其中first（iel）∈In/I且el（iel，oel）霍尔斯IΩ，而且s S在S中定义。 然后 s S，ils，olsS.这个定义指出，消除函数在消除之后，对于任何有限或无限输入（在I上），消除函数消除了一部分输入/输出行为，而没有消除全局行为。注意el可以依赖于S的内部。回想一下，我们的状态图语义是完全定义的。因此，在这个定义中，隐含的另一个方向是针对输入的可能输出之一假设s S，ils，ols S和s，iel，oel ols S和el iel，oel。则上述定义表明，这种功能的单一使用不会影响以后的行为。接下来，我们的目标是证明这个定义足够强大，足以表明即使在多次使用一个特征之后，我们也会返回到原始行为。为了保持这一点，我们需要对扩展进行更多的假设。特别是，扩展只有在多次使用时才有可能改变未来的行为。例子构造起来很简单，因为扩展可以添加本地状态。我们说S′′在某种消去函数下是S的保守扩张，如果在S. 当（s∈S，i′，o）且el（i，o） =（i′，o′）时，y（s，i，o）∈ S ′.C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6575′′ ′′不足消除色葡萄我们表明，这意味着多次使用的属性行为。定理4.1（消去下的扩张相容性）：假设S是从S消去el的一步精化，消去函数为el，S是S的保守的′S-触发扩张。那么S是一种行为修饰这个定理的例子是图1和图6中的贪睡特性。为了应用上面的定理，我们从添加的新特征构造el函数，如上面的示例所示。通过这种方式，我们可以显示系统变化的兼容性。更详细地说，我们得到一个建设性的检查，如果扩展的兼容性持有的扩展。我们可以从添加特征的图形表示中构造消除，然后我们必须检查上述条件（在大多数情况下，这可以很容易地完成，除非新转换条件中的代码包含复杂的编程构造，而通常情况下并非如此。有趣的是，讨论为什么从单个局部修改到多个修改的步骤需要对添加的功能进行如此强烈的假设。事实上，构建扩展修改后续行为的示例很容易，但如果只使用一次就不容易了。例如，状态图可以只在变量中记录某个特性的使用频率，并根据它调整行为--例如图1中的变量i。因此，我们要求该功能不修改现有状态图的状态。这也意味着我们不能仅仅通过外部输入和输出行为的推理来5相关工作在下文中，我们将讨论状态图细化的相关工作以及UML状态机和自动机模型等相关概念。我们声称，我们的消除下的精化概念是新的，可以涵盖新特征使用现有事件的实际例子此外，我们还可以涵盖新特征添加状态的情况，这些状态对于某些事件来说是未知的，因此可能导致混沌行为。早期关于状态图细化的工作[13][8][12]，使用了类似的状态图语义模型，已经开发了几个细化规则。这些都是用状态图实体来表示的，比如添加转换或状态。主要结果是，细化遵循简单的条件上的操作状态图。例如，添加一个由新事件触发的新转换会导致细化。然而，这些结果没有考虑兼容性，也没有涵盖我们的扩展兼容性概念。具体地说，[13]中的工作使用了如上所述的精化概念，但没有涵盖消除的形式，也没有涵盖扩展相容性。[12]中的工作并没有明确地消除新添加的事件或消息。假设在未定义事件的情况下，状态图进入混沌状态，这反过来又不允许在使用新功能（如此处所开发的）后覆盖兼容性。76C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65工作[11]基于到Z语言的映射并将其与抽象数据类型中的细化和模拟相关联，为[13]中的状态图开发了细化演算其基本机制也是消除新的输入和输出事件，如前所述。[4]中涵盖了以逐步发展和服务组成为对于表表示的自动机模型，开发了服务组合如上所述，细化基于新输入和输出事件的抽象，如前所述，这是有限的。对于UML建模的相关工作，[15]中开发的概念基本上涵盖了将一个状态细化为几个状态的基本情况，这是不同的，在这里不涉及。[10]中的工作重点是将添加的功能建模为独立的模块化实体，建模为状态图片段。此外，特征交互被建模为这样的片段。为了进一步完善，使用了[8][12][16]中关于UML的其他工作，建立在对象生命周期建模[14]的概念上，考虑了一致继承和观察一致性的问题，这与我们的兼容性概念相似在上面的工作中，他们考虑从新的输入信号中抽象出这些属性。然而，这种情况更简单，因为它们不考虑输出事件。其他关于模型检查的模块化的工作[3][9]也考虑了这个问题通过新的状态和转换来扩展自动机模型。在这些作品中，状态图的组成导致了对特定属性的证明义务。这些反过来又由模型检查器进行验证。因此，这些方法与这里介绍的工作非常不同。具体而言，他们要求在扩展后指定和建立每个单独的财产。 在这里，我们专注于任何行为的兼容性。在状态机的方面建模的上下文中也追求类似的目标，如[17]所示最近也有关于接口自动机的兼容性的工作[1，5，2]。在这里，兼容性本质上意味着两个自动机的输入和输出行为是兼容的，在这个意义上，一个自动机可能不会发送某个事件，而另一个自动机还没有准备好接收这个事件。精化是基于交替模拟（更多的输入，更少的输出），并保持两个自动机之间的兼容性在其他工作中，自动机中的可选转换被显式地标记，被称为模式[2，7]。在这里，我们强烈地依赖于非决定论的统一概念.即使系统模型如所讨论的那样是非常不同的，我们的相容性概念更接近于[7]中的一致性概念，基于两个自动机的状态之间的然而，这种一致性的概念并不包括新事件的接口扩展，如这里所讨论的6结论我们已经比较了状态图所描述的系统模型的细化和兼容性的概念。虽然细化粗略地说，原始行为C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）6577如果一个系统被保留在一个扩展的系统中（通过某种抽象），兼容性意味着这样的系统可以在使用原始系统的任何地方使用。具体地说，如果新的特征扩展了接口，这些属性是独立的。我们已经讨论了在什么条件下细化意味着相容性。如果一个扩展系统在没有明确使用新输入的情况下产生新的输出事件，那么精化并不意味着兼容性。 反过来，如果添加的功能使用旧的输入/输出事件，兼容性并不意味着基于简单消除的改进。在许多情况下，添加的功能会局部更改行为，但不会更改未来的行为。为了抓住这一点，我们引入了扩展兼容性的概念，它通过一个额外的前提来扩展兼容性：即使使用了新添加我们的新结果显示了在什么条件下，即使在重复使用之后，新功能的使用也会保留粗略地说，我们需要假设扩展不干扰基本模型，并且由新事件触发我们的主要新结果表明，当系统的扩展保持兼容性。这可以用于增量式系统开发，也可以用于管理一个系统的变体，如上所示。特别是，我们的目标是显示在许多情况下，扩展是与现有系统兼容，这是在许多应用场景中很重要。主要的新技术概念是在跟踪级别上消除新添加的行为。从本质上讲，我们提取可能的新行为，并从可观察的痕迹中消除这在我们使用状态图的表示中是可能的，因为控制流程（状态转换）在这个模型中非常明确。通过这种方式，我们的精化概念仍然可以从增加的功能的遍历中计算出来，并且比现有的关系精确得多。尽管现有的细化工作只是简单地消除了扩展（包括接口扩展）中新添加的事件，但我们可以处理扩展使用现有事件的许多实际情况。我们构造这样一个消除操作，从一个新的功能的单一用途，下面的图形表示这样的状态图基于此，即使新添加的功能使用现有的输入和输出事件，我们也可以实现扩展的兼容性对于这个结果，需要额外的假设来推断一个特征的多次使用会保留行为。特别地，新特征的使用可以不修改现有特征的状态。这导致了许多新的应用，而这些应用在现有的抽象和细化概念中是不可能实现的。对于未来的工作，我们的目标是涵盖更大的一组状态图的概念，如分层和并行组合。其次，另一个有趣的方面是这种扩展的时序行为，这里没有考虑。致谢。作者感谢Peter Scholz和Sebastian Bauer对本文的讨论和反馈78C. Prehofer/Electronic Notes in Theoretical Computer Science 295（2013）65引用[1] L. Alfaro和T.亨辛格基于界面的设计。In M. Broy，J. Grnbauer，D. Harel和T. Hoare，编辑，软件密集型系统的工程理论，NATO科学系列第195卷，第83-104页。Springer荷兰，2005年。[2] S. Bauer ， P.Mayer ， A.Schroeder 和R. 亨 尼克 关 于 弱模 态 兼 容性 ， refinement 和 mio 工 作台 。 在j.Esparza和R.Majumdar，编辑，系统构造和分析的工具和算法，计算机科学讲义第6015卷，第175-189页。 Springer Berlin / Heidelberg，2010.[3] C. Blundell，K. Fisler，S. Krishnamurthi，and P. Van Hentenrvck.参数化接口，用于产品线的开放系统验证。自动化软件工程，2004年。诉讼第19届国际会议，第258 - 267页，2004年9月。[4] M.布洛伊多功能软件系统：功能需求的结构化建模和规范。Sci. Comput.程序. ，75：1193[5] A. David，K. G.拉森A.莱盖，美国Nyman和A.华斯基时间输入输出自动机：实时系统的完备规范理论在第13届ACM混合系统国际会议论文集：计算和控制，HSCCACM。[6] R.伊苏伊斯 验证状态图语义。 Science of Computer Programming，74（3）：65[7] D. Fischbein，S. Uchitel和V. Braberman。软件产品线架构中行为一致性的基础。在ISSTA 2006年关于测试和分析软件架构的作用的研讨会论文集，ROSATEA'06，第39-48页，美国纽约州纽约市，2006年ACM。[8] C.克莱因角Prehofer和B.朗普使用状态转换图进行特性规范和细化。在第四届IEEE电信网络和分布式特征交互研讨会上，第284IOS Press，1997.[9] J. Liu，S. Basu，和R.卢茨使用变异点义务的软体产品线组合模型检查。自动化软件工程，18：39[10] C. 普雷霍弗功能的即插即用组合以及与状态图的功能交互。软件和系统建模，3：221[11] G. Reeve和S.里夫斯图表的逻辑和细化。在Proceedings of the 29th Australasian Computer ScienceConference - Volume 48，ACSC'06，pages 13-23，Darlinghurst，Australia，Australia，2006中。澳大利亚计算机协会[12] B. Rumpe 和C.克莱恩描 述对象行为的自 动机。面向对象 信息建模中的行 为语义规范， 第265KluwerAcademic Publishers，1996.[13] P. Scholz。状态图规范的增量设计。计算机程序设计科学，40（1）：119– 145,[14] M. Schre Schleman和M. Stumptner对象生命周期的行为一致专门化。ACM Trans. Softw.工程师，Methodol。，11：92[15] A. J. H. Simons，M. P. Stannett，K. E. Bogdanov和W. M. L.霍尔科姆W.m.l.：安全即插即用：行为兼容性规则 In In：Proc. 第六届IASTED国际Conf. 软件工程和应用，第263-268页， 2 0 0 2 年 。[16] M. Stumptner和M.施雷uml中的行为一致继承第451两千[17] G. Zhang和M. 霍茨尔 Hila：High-le velas pectforumlstatemachine. InS. Ghosh，编辑，软件工程中的Models，计算机科学讲义第6002卷，第104-118页。Springer Berlin / Heidelberg，2010.