严格模型驱动开发下的模板框架

理论计算机科学电子笔记191（2007）3-23www.elsevier.com/locate/entcs基于模板的框架用于严格的模型驱动开发NunoAm'alio1Fion aPolack2SusanStepney3英国约克大学计算机科学系摘要工程系统的可接受的正确性是一个难题。一方面，在实际的大规模系统开发中使用的半形式化建模方法，如UML，不适合形式化分析和一致性检查。另一方面，正式的建模和分析需要一定的能力和专业知识，这在商业开发社区中并不常见，正式的方法没有很好地与开发过程的其余部分相结合。 本文提倡一种为严格的模型驱动开发构建工程环境（或框架）(MDD)这是基于结合半正式符号与正式建模语言。 为了支持这种方法，有一种形式化的模板语言，它捕获了形式化开发的模式，并支持使用模板进行证明的方法这允许构建模式目录（代表-以模板的形式表示）和框架的元定理。本文提出并举例说明了一个结合UML和形式化语言Z的顺序系统框架。关键词：UML，MDD，Z，模式，模板。1介绍模型驱动开发（MDD）[17]试图通过选择模型而不是代码作为软件开发的主要工件来提高抽象级别。模型描述了系统的域和所需的行为，在软件的构建和维护阶段非常有用。模型的分析揭示了规律，并提出了与系统的需求和设计有关的基本问题在开发的早期阶段，当代码还不存在的时候，模型分析是最有价值的，它暴露了一些问题，这些问题如果直到后来才被发现的话，需要花费更多的时间来修复。1电子邮件：namalio@cs.york.ac.uk2电子邮件：fiona@cs.york.ac.uk3电子邮件：susan@cs.york.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.09.0024N. Amálio等人理论计算机科学电子笔记191（2007）3主流软件工程使用半形式化技术进行MDD。4这些都是基于图表符号，这是用来描述系统的不同方面正是它们的图形特性和实用的开发方法使它们流行。事实上，半形式化符号是直观的，并且提供了系统不同方面的易于阅读的草图此外，一些半正式的符号，如UML和实体关系图，是软件工程师事实上然而，正是在细节中，我们发现了他们的弱点。半形式符号缺乏形式语义，因此：模型可能是模糊的，不一致的，不适合机械语义分析。语义问题由于半形式化符号有许多语义解释的事实而变得更加严重：语义的选择成为一个方便的问题，开发人员根据手头的问题类型使用一种语义或另一此外，并不是所有的系统属性都可以用图来表达;通常，开发人员采用文本符号来描述详细的系统约束。另一方面，形式化技术主要用于需要严格开发的利基领域（例如安全关键系统）。形式化建模语言（如Z、B、CSP、Alloy）基于数学和形式逻辑，它们体现了形式化开发中多年的研究和最佳实践。由此产生的模型是精确的，明确的，并服从形式化分析。然而，正式的建模和分析需要一定的能力和专门知识，这在商业开发界并不常见，正式的方法也没有很好地与开发过程的其他部分结合起来。在主流模型开发中已经有许多尝试引入形式化技术[2].一些方法建议将diagram翻译成正式的建模语言，但不支持分析本身（例如[13，14，18]）;为了探索分析，用户需要成为正式语言的专家。其他方法花费精力开发另一种特殊用途的形式语言，而不是建立在现有的成熟工作上（例如[15，7，8]）。大多数方法没有考虑半形式化符号的多种语义（参见[2]的例子）;然而，开发人员可能希望某些高级建模概念的替代语义，即使在同一开发中，因此，为了应对这一点，需要一种灵活实用的方法来定义半形式化符号的语义。为了解决这些问题，在[2]中，我们借鉴了基于模式的开发[10]和问题驱动方法[11]的思想，以倡导一种基于框架的方法，用于严格但实用的MDD。我们的MDD框架是工程师构建、分析和细化软件系统模型的旨在解决特定问题领域的需求。它们使用图表和形式化建模语言，图表充当下面的形式的图形接口。目的是完全隐藏形式，但这并不总是可能的。为了支持框架的构建，我们开发了形式模板语言（FTL）[2，6]，这是一种模板语言，可以使用模板表示进行证明。4 它们被称为半形式的，因为它们的符号有形式语法，但没有形式语义。N. Amálio等人理论计算机科学电子笔记191（2007）35情感FTL允许表示形式化开发的模式（例如，模型结构），并使用元证明（例如，在模式级别计算先决条件或证明初始化定理）在模式级别进行推理，以建立元定理。模板和元定理被组装在框架目录中，因此每个模式实例都是通过实例化模板来生成的，并且，如果适用的话，通过实例化元定理来简化模式实例的一致性证明（通常是平凡的情况）。[2]开发了一个结合建模语言UML和Z的顺序系统框架-UML+Z框架。本文概述了[2]中提出的生成式框架的一般构造方法，特别是[2]中提出的UML+Z它说明了一个生成的模型开发与UML+Z框架，其中Z模型是从UML+Z目录的模板生成。本文展示了如何在更广泛的背景下的UML+Z框架中使用与这里报道的研究相关的已发表的结果特别是，它显示了如何在[2，6]中开发的语言FTL可以用于为UML+Z构建模板和元定理的目录，如何通过将UML+Z应用于[4]中开发的案例研究的简单版本，使用目录可以用于生成具有[2，3]中开发的面向对象（OO）风格的Z模型，以及如何通过使用开发的快照分析技术来正式分析所得到的UML+Z模型在[2，5]中。下面首先简要介绍FTL及其元证明方法。然后，它给出了一个概述的方法，提出了建立框架，特别是UML+Z框架。接下来，它通过将UML+Z框架应用于一个简单的问题来说明它。最后，对本文的研究结果进行了讨论，并与相关工作进行了比较，得出了结论。2超光速和元防护模板捕获某种语言的句子的形式（或形状），在实例化时生成该语言的句子，其形式由模板规定，并且可以用于描述构成模式的那些常见结构。我们的形式模板语言（FTL）[6，2]是一种表达模板的语言，可以使用模板表示进行证明。例如，FTL可用于捕获Z提升ADT的状态[20]：P==[ids：ID;st： ID›→S|domst =ids[I]这引入了五个占位符，P，ids，ID，st，S和I，它们在实例化时将被一些文本值可以实例化此模板以产生：Bank==[accs：ACCID;accSt：ACCID›→Acc|domaccSt =accs true]6N. Amálio等人理论计算机科学电子笔记191（2007）3任何形式的句子或某种形式语言的句子（这里是Z）都可以表示为FTL中表达的模板。有没有可能用这些模板表示进行推理（或证明）？如果可能的话，这将具有很大的实际价值。这将意味着重用可以达到证明的水平某些模板的元定理将被证明一次，但可能是适用的每次这些模板被实例化时。这种使用模板的证明方法称为元证明。首先，通过一个实例说明了元证明的实用价值。在Z中，将抽象数据类型（ADT）的状态空间的描述（如上面的Bank）引入到规范中，需要证明描述是一致的：至少存在一个满足描述的状态。这涉及到定义ADT的初始状态（所谓的初始化）并证明初始状态确实存在（初始化定理）。银行的初始化假设在初始状态下没有账户：BankInit == [BankJ|accsJ=accStJ=]为了证明班克的一致性，我们需要解除这个猜想►？*BankInit·true，在Z/Eves定理证明器中自动释放[16]。这一证明定理仅适用于银行ADT。问题是：它是否适用于所有与银行形式相似的推广ADT？如果是这样，这个结果是否可以一劳永逸地证明，这样开发人员提升的ADT的空初始化和相关猜想用模板表示：PInit==[PJ|[idJ=0]►？ CUP初始化·真我们可以通过分析这些模板的良构实例来推理它们。在这些情况下，P、id和st保存名称，ID和S是集合，而I是谓词。通过使用模式计算的定律扩展模板模式，并应用一点规则（见上面的证明），我们得到公式，dom=∈ID∈ID›→SiJ[ IDsJ：= 0，stJ：=]这减少到， 我J[ IDsJ：= 0，StJ：= 0]。5 如果我用true实例化，则公式归约为true。这建立了两个元定理，其中后者是前者的专门化（或推论），这是适用的到从这些模板实例化的所有提升的ADT。专门的Meta定理通过构造给出了true的良好性质：只要这些模板5P[x：=val]表示将P中的自由变量x替换为值val而得到的Z表达式。我们采用这种特殊的表示法，因为在Z中，通常的逻辑替换运算符符号/用于表示模式引用中的变量重命名。N. Amálio等人理论计算机科学电子笔记191（2007）37被实例化，使得I被实例化为真，则初始化猜想简单地为真。即使 我 没有用true实例化，要证明的公式比初始公式简单这个元证明中概述的论点是严格和有效的，但它不是形式的。为了遵循元证明的形式化方法，FTL被赋予了形式化语义[6]。这允许定义Z模板表达式的证明规则，这些规则通过上诉FTL的语义来证明[6]。3UML+Z框架在文献[2]中，我们提出了一种面向对象的时序系统建模框架，它是基于建模语言UML和Z。UML+Z框架（图1）使用UML类、状态和对象图，它们在Z语义域中表示Fig. 1. UML+Z框架中的模型。在下文中，我们将使用UML+Z框架讨论MDD框架的三个主要组件。3.1建模框架的建模组件是按照语义定义的指称方法定义的[19]。这包括一组图表类型，它们构成了语法域（框架模型的每个图表都在UML+Z框架[2]中，有一个Z语义域来表示OO模型[3]，因此UML+Z模型的每个图都在这个语义域中表示还有一个与模型一致性相关的模板和元定理的目录，它们捕获了Z语义域的结构;UML+Z模型的每个Z语句都是通过实例化分类. UML+Z的语义映射的正式定义留给未来的工作;目前它是由手工完成的。8N. Amálio等人理论计算机科学电子笔记191（2007）33.2分析分析部分定义了分析框架模型的方法。[2，5]定义了一种基于形式证明和Catalysis[9]快照分析UML+Z模型的方法：基于快照的验证。这种技术基于绘制快照（对象图）。快照描述了模型化系统的一种状态快照可以成对使用来描述操作对系统状态的影响：一个快照描述之前的状态，另一个描述之后的状态。分析包括在Z语义域中表示快照，然后在Z世界中证明快照或快照对满足系统的模型。在这里使用的例子中，这些证明是使用Z/Eves定理证明器[16]执行的3.3细化精化组件定义了一个精化框架模型的策略，并包括一个模型转换（重构）的目录的变换用FTL表示。UML+Z的精化组件留待以后的工作。其目的是定义一种策略来细化UML+Z模型，基于Z的细化理论[20]，以及一些示例模型转换。我们的想法是用超光速捕捉重构和探索元证明，以减少与这些重构相关的证明开销这个过程类似于建模中遵循的过程：（a）重构和相关的正确性分析是用模板捕获的;(b)元证明被应用于这些表示以简化（并且在某些情况下完全证明）正确性证明。这将允许通过实例化模板来执行模型转换：在应用相关的元定理之后，相关的正确性证明可以简化为更小的证明4图示本节通过一个跟踪产品订单的简单系统的用例来说明UML+Z框架。这个用例是[4]中建模的用例的简单版本。由于篇幅原因，仅给出模型的说明性部分。关于本案例研究模型的更多细节可以在[4]中找到。首先，我们建立了一个系统的模型，然后我们分析它的快照。4.1建模UML+Z模型分为UML部分和Z部分。订购系统的UML部分包括一个类图和一个状态图。图2显示了系统的类图。有两个类，Order和Product，每个类代表一组对象（系统的订单和产品）。每个Order对象都有一个quantity属性，表示产品的订购数量，每个Product对象都有一个stock属性，记录N. Amálio等人理论计算机科学电子笔记191（2007）39invoice（）未决发票取消该产品有现货供应。订单和产品是通过一个关联来联系的，也就是说，每个订单只涉及一个产品，而每个产品可能被多个订单所涉及秩序引用产品* 1数量：NAT股票：NAT图二. 平凡订购系统的UML类图。秩序的对象具有可以识别的不同状态。这在图3的UML状态图（或状态图）中进行了描述。 当一个Order对象被创建时，它的状态是pending。当开具发票时，订单从待定状态变为已开具发票状态。图三. Order类的UML状态图。下面为OO Z风格的每一种观点（结构的、内涵的、外延的和关系的;进一步的细节见[3，2]）提供了一个有序系统的部分Z模型。Z模型是从UML+Z目录的模板中生成的，通过使用来自图的信息和来自用户的额外信息实例化它们。附录B给出了用于生成此处所示Z的模板。这些模板使用UML+Z工具箱中的Z泛型（这里使用的泛型在附录A中给出）。从模板生成的Z在以下文本中使用术语表示：• 完全生成-Z完全从模板中生成，实例化信息来自图。如果我们有一个工具，Z会自动生成。• 部分生成-实例化依赖于不是来自UML图的信息，需要由用户显式添加（通常是无法用图表表示的约束）。4.1.1结构图这个观点的定义是完全生成的。我们需要定义模型的每个类的所有可能对象原子的集合。所以，首先，我们定义一个模型的所有类（表示为原子）的集合，通过实例化模板T1：CLASS：：= OrderCl|产品介绍10N. Amálio等人理论计算机科学电子笔记191（2007）3秩序状态：OrderST数量：真订单初始化订单J数量？：状态J=待处理数量J=数量？有一个所有对象原子的集合OBJ，它在工具箱（Ap-pentrumA）中定义。一个类（OBJ的子集）的所有可能对象原子的集合由函数O给出，它通过实例化模板T2来定义：1OBJDO使用这个函数，可以用表达式OOrderCl获得对象的集合，比如Order。4.1.2内涵观这个视图定义了状态空间和每个类的对象的初始化。Order的内涵完全由模板T3生成，对于具有状态图的类：6有一个Z类型表示Order的可能状态，如状态图中所定义：OrderST：：=待定|发票状态空间包括字段数量（来自UML类图）和状态（保存状态图中定义的对象的当前状态）。初始化将状态场设置为状态图的初始状态，并将数量设置为从环境接收的某个值：这个定义的一致性通过证明两个命题（也是从模板中生成的）来检查。第一个是关于形式良好的猜想，►？ 数量多少？·数量？∈在Z/Eves中自动证明。 第二，初始化猜想，►？ OrderInit·true通过诉诸模板的元定理init-int-ni的构造为6Product的内涵将从没有状态图的类的模板中实例化，详见[2]。O：CLASS→不相交类N. Amálio等人理论计算机科学电子笔记191（2007）311ΦS订购新ΔSOrderOrderJ秩序！：OOrderCl秩序！∈ OOrderCl\sOrdersOrderJ=sOrder<${oOrder！}stOrderJ= stOrder{oOrder！›→θOrderJ}4.1.3延伸视图这个视图定义了一个类的现有对象的集合。Order的状态扩展和初始化完全由模板T4生成：SOrder==S CL[OOrderCl，Order][sOrder/os，stOrder/oSt]SOrder Init ==[SOrder J|sOrder J= 0]该定义使用ZOO工具包中的SCL泛型（附录A）。通过构造模板的元定理init-ext证明了初始化猜想成立。我们现在定义创建新Order对象（也是完全生成的）的操作。首先，定义了订单的新促销框架，它是从模板T5生成的：创建新Order对象的操作由模板T6生成：SΔOrderNew==OrderJ· ΦSOrderNewOrderInit利用模板的元定理计算了该运算的前提条件，并证明了该运算的相容性。通过实例化模板的元定理pre-ext-nop来preSΔOrderNew = [SOrder;quantity？ ：|OOrder Cl\sOrder]通过epre-ext-nop元定理证明了一致性猜想总是成立的。4.1.4关系视图这个视图定义了UML关联的Z表示。状态空间、初始化和关联链接模式完全从模板T7生成。关联引用的状态空间定义和初始化是：AReferences== [rReferences：OOrderClParticipOProductCl]AReferencesInit == [AReferencesJ|r参考文献J=]初始化猜想是真的，通过构造，呼吁元定理assoc-init。12N. Amálio等人理论计算机科学电子笔记191（2007）3LinkA参考文献A参考;S订单;S产品multt（rReferences，sOrder，sProduct，mo，mid，mid）AΔ参考添加ΔAReferencesoOrder？：OOrderClo产品？：OProductClrRefe ren cesJ= rRefe ren ces{oOrder？ ›→oProdu c t？}系统S订单;S产品;A参考系统常量链接模式将关联中引用的对象链接到现有对象（类扩展的对象），并声明关联多重性约束。这用于在全局视图中构建系统结构（如下）。该模式所需的约束使用UML+Z工具包的多泛型来表示（参见附录A）：这说明关联References是一个多对一（mo）关联。当关联具有用户定义的多重性约束集（例如1.）时，使用mult的最后两个参数（在这里它们的值为1）。5）。当一个新的订单被输入到系统中时，有一个由新订单和订购产品组成的元组这通过向关联添加新元组的操作来描述，该操作完全从模板T8生成：这个猜想的前提条件由模板的关联前顶点元定理给出;它给出了一个真谓词（它是一个全运算）。一致性猜想通过构造（元定理assoc-pre-atop）是正确的。4.1.5全局视图这种观点将系统定义为一个整体。 系统的状态空间和初始化由模板T9生成。在这种情况下，由于没有全局约束，因此完全生成。有一个模式代表所有的系统约束，因为没有全局约束，这只包括关联链接模式：SysConst==链接A引用系统状态空间通过包括所有类和关联以及系统约束模式来定义：N. Amálio等人理论计算机科学电子笔记191（2007）313系统初始化是系统的类和关联的初始化：SysInit==SystemJSOrderInitSProductInitAReferencesInit系统初始化猜想，►？ SysInit·true通过模板T9的元定理sys-init-ni的构造是真的。我们现在定义新的订单系统操作，它是部分生成的。首先，我们通过实例化模板T10来定义操作的框架：实际的系统操作创建一个新的Order类对象，并添加一个链接（或元组）与对象的关联。 这种系统操作由模板T11捕获;该系统操作的该模板的实例化给出：SysNewOrder==NewOrderSΔOrderNewAΔ参考添加[oOrder！/o订单？]利用模板的元定理计算了运算使用元定理pre-sop-newadd和Z/Eves，操作的前提条件是：【系统：数量？：;oProduct？：OProductCl|OOrderCl\sOrder/=订单产品？∈sProduct]一致性猜想（也是从模板生成的），►？ 返回SysNewOrder·true通过元定理epre-sop-newadd-ncs简化为在Z/Eves中容易证明的东西。这里提出的模型已经从两个图通过实例化模板生成现在是检查模型是否满足系统要求的时候了。4.2分析现在使用快照分析系统的模型。首先，使用单快照来分析状态空间，然后使用快照对来分析系统操作。14N. Amálio等人理论计算机科学电子笔记191（2007）3PY：产品O1：订单PX：产品StSnap1系统sOrder={oO1} 第一Order={oO1→O1}sProduct={oPX，oPY} 初始Produt={oPX<$→PX，oPY<$→PY}rReferences={oO1<$→oPX，oO1<$→oPY}4.2.1状态空间状态空间分析说明了一个要求的订购系统，说，每个订单必须只引用一个产品。为了检查模型是否满足这一要求，我们画一个否定情况的快照，也就是说，它描述了一个不应该被系统模型接受的状态。 图4显示了一个快照，其中一个Order对象引用了两个Product对象。见图4。 与两个产品关联的订单的快照。为了检查模型是否接受这个快照，首先用Z表示快照，然后证明一个猜想。快照的表示是通过实例化完整目录的一些模板来完全生成的（参见[2]）。Z中快照的部分表示为：(Here系统是Z模式，它将系统定义为一个整体，见上文。由于快照不应该被系统接受，我们证明了猜想（肯定情况的否定）：►？ （而这个猜想是正确的（在Z/Eves [16]中已经得到证明），这意味着快照所描述的状态不被系统的模型所接受4.2.2操作我们现在分析系统操作的模型，以向系统添加订单。图5描述了两个快照对。首先，在操作之前，有一个没有订单的产品，在操作之后，系统中有一个新的订单，它引用了该产品。在第二个快照对中，before状态是一个订单引用产品的状态，after状态是两个订单引用产品的状态。这两个状态转换应该被系统接受。快照以Z表示，如上所示（从模板实例化）。快照对的有效性通过证明两个命题来检查。第一个演示了之前的状态快照和操作的输入描述了一个N. Amálio等人理论计算机科学电子笔记191（2007）315库存= 1数量= 2状态=待定数量= 2状态=已开票PX：产品O2：订单O1：订单库存= 1数量= 2状态=已开票PX：产品O1：订单NewOrder（oProduct？= PX，数量？= 2）图五. 操作新订单的快照，一个产品的订单。满足操作前提条件的系统的有效状态►？ 返回SysNewOrder·BOpSnap1目录IOpSnap1第二个猜想证明了快照对描述了由系统操作指定的有效状态转换►？SysNewOrder·BOpSnap1上面给出的两个快照对所需的所有构造都可以在Z/Eves中证明：操作new order满足快照描述的状态转换。有关使用快照进行分析的其他示例，请参见[5，4]5讨论这里提倡的MDD框架旨在对用户隐藏形式语言。在UML+Z中，这一点无法完全实现。至少需要一位专家来编写Z操作规范和不变量，这些规范和不变量不能用UML图来表达。然而，UML+Z框架允许非Z专家通过绘制类、状态和对象图来参与建模和分析。半正式符号的语义问题的解决，考虑一个语义，是适合的框架所针对的问题域。如果一个框架需要一个建模概念的变体，那么这些可以被定义为UML原型，每个原型都有一个唯一的语义。基于快照的验证仍然需要创造性地构造一组合适的快照然而，这是在图语言中完成的，而不是形式语言。然后正式进行分析使用针对问题域定制的模板模式和框架有助于促进知识重用。MDD框架以模式的形式封装了知识和同样的工作可以重复使用和适应，16N. Amálio等人理论计算机科学电子笔记191（2007）3满足其他问题的需求（在同一框架内，或为探索新问题域的新框架）。我们的基于模式的方法，基于FTL和元证明，有助于使形式化方法更实用。FTL允许结构化模式的表示，以便它们可以通过实例化来重用（或适应上下文）。Meta- Proof允许在模式级别进行推理以建立元定理，从而可以重用相同的推理结果在UML+Z中，所有Z都是通过模板实例化生成的，并且通过应用元定理来减少与一致性检查相关的证明任务。工具支持将使MDD框架全面开花。目前，模板是手工实例化的，用户需要从UML工具切换到Z工具。然而，我们设想了一种可以自动化大部分过程的工具，最大限度地减少开发人员对Z工具的暴露。6相关工作这里介绍的工作借鉴了几个来源的思想。基于模式的开发思想来自于设计模式的工作[10]，而设计模式的工作又受到Christopher Alexander在Architecture [1]中的工作的启发问题驱动的方法和框架的想法是针对问题域的启发，在迈克尔杰克逊的工作[11，12]，谁主张不同的问题需要不同的方法和使用不同的概念和符号。一个与我们相近的工作是催化[9]，一个基于UML的建模方法。与Catalysis一样，我们也使用模型框架和模板的思想来使模型可重用资产，使用UML图来细化模型的思想，以及定义适合于使用它们的上下文的UML构造的语义的思想。我们的方法不同于这些作品，因为它是完全形式化的。我们的框架旨在集成正式和半正式的建模语言，以实现严格的开发。以UML+Z为例，设计了UML与Z的结合使用。另一个关键的特点是，我们的方法是基于FTL，一个正式的语言来表达模式，这是用来建立一个框架的模板目录这样的目录已经在上面的UML+Z的上下文中说明过了。7结论本文提出了一种为严格的MDD构建框架的方法。为了支持这种方法，本文提出了一种模板语言（FTL），使证明与模板（元证明）。FTL用于构造模式目录（表示为模板）和框架的元定理;因此，通过实例化模板生成模式实例，并且可以在模式级证明模式的某些性质，因此，在实例级的证明要么简单，要么复杂。N. Amálio等人理论计算机科学电子笔记191（2007）317是否需要（根据结构确定）。本文还提出并说明了一个框架的顺序系统，结合了形式化规范语言UML和Z。在示例中，通过实例化目录中的模板来构建形式化模型，通过 使用目录 的元定理 来证明模 型的一 致性，并 且基于快 照和形 式化证明（UML+Z框架的分析策略）来分析模型。确认这项工作由葡萄牙科学和技术基金会资助，赠款6904/2001。这里介绍的一些工作是由教授监督的AugustoSam paio，duringAm'alio所有的资助和监督都是感激的。引用[1] 亚历山大角，S. Ishikawa和M. Silverstein，[2] Am'alio，N.，“Gene r at i v e f r a m e w o r k s for r i go r ou s modd e l - d r i v e n d e v e l op m e n t，“Ph. D. 他是，计算机科学的De partmm mttt，约克大学（2006年），出现。[3] Am'ali o，N.， F. 波拉卡和S。因此，对于基于Z的虚拟机，一个非约束的结构可以在以下情况下实现：H. Treharne等人，编辑，ZB 2005：B和Z用户的国际会议，LNCS3455（2005），pp. 262-278。[4] Am'ali o，N.， F. 波拉卡和S。UML+Z是一种基于Z的UML分析方法，在M. 我的手机和H。 H abrias，编辑，软件规范方法：使用案例研究的概述，Hermes Science，2006年。[5] Am'alio，N.， S. StepneyandF. Polack，对于来自U M L模型的PormalproofroF r of DAVIE S ETAL.，编辑，ICFEM 2004：形式工程方法国际会议，LNCS3308（2004），pp. 418-433[6] Am'alio，N.， S. StepneyandF. Polack，Aformartemplateelanguagenablingmeta-prof，in：FM2006：Formal Methods，LNCS 4085（2006），pp. 252-267。[7] 克拉克，T.，A. Evans和S.元建模语言演算：UML的基础语义，在：H。Hussmann，编辑，FundamentalApproaches to Software Engineering（FASE 2001），LNCS2029（2001），pp.17-31.[8] 克 拉 克 ， T. ， A. Evans 和 S.Kent ， Engineering modeling languages ： A precise meta-modelingapproach，R.D.Kutsche和H. Weber，editors，Fundamental Approaches to Software Engineering（FASE 2002），LNCS2306（2002）. 159-173.[9] D'Sousa，D.和A. C. Wills，[10] 伽马，E.，R.赫尔姆河Johnson和J. Vlissides，[11]杰克逊，M.，形式化方法与传统工程，系统与软件杂志40（1998），pp. 191-194.[12] 杰克逊，M.，“Problem Frames: Analyzing and structuring software development problems,” Addison-Wesley,[13] Mander，K. C.和F. Polack，Structured Specification Using Structured Systems Analysis and Z，Information and Software Technology37（1995），pp. 285-291。18N. Amálio等人理论计算机科学电子笔记191（2007）3OBJ=/SCL [OS，OST]操作系统：OSOSt：OS ›→OSTdomoSt =os[X，Y]mult ： （（X参与Y）×X×Y×MultTy× ×）r：XParticipateY;sx：X;sy：Y;s1，s2：·（mult（r，sx，sy，mm，s1，s2））惠r∈sx参与r：XParticipateY;sx：X;sy：Y;s1，s2：·（mult（r，sx，sy，mo，s1，s2））惠r∈sx→sy.[14] Nguyen，H. P.，“D e r i v a t i r D e S p ec i on s F o r m e l e s B ` a p a r t i r d e S p ec i on s S S e m i - F o rm e l e s“，Ph. D. thesis，LaboratoireCEDR IC，ConservatoireNati onald es Ar t s etMetier s，Evry，France（1998）.[15]Oévergaard，G. ，对于块体结构的特殊性，在：T中。Maibaumm，editorr，Fundamental Approaches to Software Engineering（FASE 2000），LNCS1783（2000），pp.193-207.[16]Saaltink，M.，Z/EVES系统，在：ZUM（1997年）。[17] 施密特，D。C.的方法，模型驱动工程，IEEE计算机39（2006），pp.25比31[18] 斯努克角和M. Butler，UML-B：UML辅助的形式化建模和设计，ACM Trans. Softw。工程师，Methodol。15（2006），pp. 92比122[19] 坦嫩特河D、编程语言的指称语义，Commun。ACM19（1976），pp. 437-453[20] Woodcock，J.和J. Davies，一个精简的Z泛型工具包本附录包含在第4节的插图中使用的Z泛型。完整的工具包见[2]。[OBJ]MultTy：：= mm|莫|om |MZO |Zom |oo |Zozo|动物园|Ozo |MS |SM |SS|OS| szo| ZOS|zosN. Amálio等人理论计算机科学电子笔记191（2007）319O：CLASS→1OBJ不相交（O类）CL在：atT状态：Cl STCLICI初始化CLJII？：iiT在J=IV状态J=initStB精简的模板本附录包含第4节插图中使用的模板。[2]《易经》中的“卦”，是指卦的卦。模板T1（类原子集）CLASS：：=01 - 02 -02|、“”）模板T2（类的对象集）模板T3（内涵状态空间和状态图初始化）CLST：：=initSt|OST►？∀II？：iiT·iv∈atT► ？ ∃CL初始化·真元定理Γ 氯氰菊酯初始化·真[int-init]Γ►∃II？：iiT·CLIJ[在J：=iv，状态J：=[initSt]I;CLI初始化·true[init-int-ni]真[at T]模板T4（扩展状态空间和初始化）20N. Amálio等人理论计算机科学电子笔记191（2007）3Φ SCL NΔSClCLJOCL！：O型Cl ClO CL！∈OClJ=sCLCl\sCLSCL{oCl！}StCLJ=stCL{oCL！›→ θClJ}LinkA作为一作为; SClA;SClB多个作为，ClA，s ClB，multE、MS1、MS2）SCL==SCL[OCLCl，CL][sCL/os，stCl/oSt]SCLInit==[S ClJ|SClJ=最大值ClJ=Cl]元定理Γ ►∃ SCLInit·true [init-ext]真模板T5（新促销框架）模板T6（新类操作）SΔCL新== ClJ·Φ SCLNCI初始化元定理[pre-ext-nop]Pleasure SΔCL新[epre-ext-nop]真模板T7（关联状态空间和初始化）A作为==[r作为：O型ClAClParticipOClB[Cl]A作为Init==[A AsJ|R由于J=]► 前SΔCl新[S Cl;ii]？：IIT|OCLCl\sCL/=]N. Amálio等人理论计算机科学电子笔记191（2007）321AΔ如添加ΔAAsoClA？：O型ClACloClB？：O型ClBClR当J= r时作为{\fn黑体\fs22\bord1\shad0\3aHBE\4aH00\fscx67\fscy66\2cHFFFFFF\3cH808080}›→o常数SConstS常量Cl;A常量系统氯;砷SysConst元定理Γ ►∃ A作为Init·true [assoc-init]真模板T8（关联，添加元组操作）元定理[assoc-pre-atop]前AΔ作为添加·true [assoc-epre-atop]真模板T9（系统状态空间、初始化和约束）SysConst==LinkA作为常数SConstSysInit==SystemJ S ClInit一初始化时► ？SysInit·true前AΔ作为添加·真[答作为; o中情局？：O型ClACl; oClB？：O型ClBCl]22N. Amálio等人理论计算机科学电子笔记191（2007）3元定理[sys-init]r;Const调用SysInit·true[sys-init-ni]真模板T10（系统操作框架）ΨSOP== Δ系统∧ΞSfCl∧ΞAfAs模板T11（系统操作新对象和添加元组）SysSOP== SOPOpConstopConstnCl新AΔAAS添加[oNCL！/onCl？]►？ { Cl}={nCl，fCl}{ As}={aAs，fAs}► ？ 阿斯普雷系统SOP·真实元定理前（前）SOPOpConst opConstnCl新AΔAAS添加[oNCL！/onCl？]）[pre-sop-newadd]系统压力SΔnCl新阿托佐NCL！：O型nClCl;nClJ; A aAsJ·（SysConstJOpConst opConst）[θSfClJ：=θSfCl，θAfAsJ：=θAfAs，SnClJ：=sNCL{onCl！}，StNCLJ：=st nCl{oNCL！<$→θ nClJ}]∧nCl初始化AΔAAS添加[oNCL！/onCl？]康斯特J[Γ 返回SysInit·trueSClJ：=0，stClJ：= Cl，r作为J：=]