理论计算机科学电子笔记130（2005）39-55www.elsevier.com/locate/entcs形式、演化和模型驱动的软件工程吉姆·戴维斯 查尔斯·克莱顿 爱德华·克莱顿a Ib HolmSørensenb一牛津大学计算实验室，Parks Road，Oxford，OX1 3QD，UKBB-Core（UK）Limited，Kings Piece，Harwell，Oxfordshire OX110PA，UK摘要本文介绍了一种软件开发方法，其中一系列的工作实现自动生成从一系列的正式规格。 这些实现是通过标准协议进行通信的数据存储。规范是精确的对象模型，其中操作是根据前置条件和后置条件来描述的。这种方法是渐进的，在这个意义上，规范可以在系统使用时演变，以响应 需求的变化，对规范的任何变化都会自动反映在实现的结构和当前存储的任何数据的表示中关键词：模型驱动，对象建模，形式化方法1介绍模型驱动架构（MDA）这个术语对于大多数软件开发人员来说都很熟悉。它经常被描述为“软件工程的未来”。一个流行的，充分的，这个词的特征是这样的：“MDA is about using modelling languages as programming languages ratherthan为了使这个特征更精确一点：MDA是关于编程语言，目前，只用于规范和设计的目的。建筑这个词反映了这个术语的起源。它首先应用于嵌入式系统的环境中，其中的要求是精确确定的。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.00440J. Davies等理论计算机科学电子笔记130（2005）39开采，组件的设计是高度规则的，并且有很大程度的重复使用。从同一个模型中构建几个不同的相同类型的嵌入式系统，简单地通过改变参数或修改状态转换图，这并不罕见大多数现代汽车中控制刹车的软件是MDA在其原始环境中的一个很好的例子：数学模型的方程确定用于标记状态图上的转换的值，然后自动转换为C，并使用一组标准库进行编译。同样的基本模型可以重复用于许多不同种类的汽车，只需改变方程或图表。随着对其他类型系统的需求得到更好的理解，并且随着它们的设计变得更加规则-通过增加语言，协议和接口的标准化-模型驱动方法正在扩展到其他应用领域：最值得注意的是，Web服务和企业计算系统。本文首先简要探讨了一种稍微更通用的方法-模型驱动的软件工程-其中抽象模型用于生成许多不同类型的工件：程序，测试套件，原型，文档，接口和其他抽象模型。在第2节中，我们展示了如何根据目的对模型进行分类，并讨论了自动模型转换的潜力。如果它们被当作程序来编译，或者被用作任何类型的自动生成的基础，那么抽象模型必须具有精确的、形式化的语义。现有的模型驱动开发的例子使用统一建模语言（UML）[2]的精确子语言，或相关的符号，如Harel在第3节中，我们引入了一个新的基于对象的符号，从Z [8]，B [6]和RefinementCalculus [4]等形式化方法中汲取灵感。在第6节中，我们将展示这种语言如何支持迭代式的开发，在这种开发中，模型被反复更新以包含额外的功能，或者考虑需求的变化。每次更新都会生成系统的新版本，并且会自动传输先前版本中的任何数据：因此，系统在使用时似乎会不断发展。本文最后简要讨论了影响。2模型驱动软件工程软件工程，正如鲍尔[5]所定义的那样，“the establishment and use of sound engineering principles in orderJ. Davies等理论计算机科学电子笔记130（2005）3941以经济的方式获得可靠的软件，并在真实的机器上有效地工作”这些原则包括对预期功能的描述，没有这些描述，评价和确认的基本工程活动将是不可能的。这种描述通常涉及创建系统的一个或多个模型。我们可以根据目的对这些模型进行分类：草图模型这些包含有关设计特征和系统要求的信息。它们应该被看作是非正式的模型--即使所使用的语言可能承认一个正式的语义--因为它们不是被设计成字面上的。例如，草图模型中的状态图可能包括转换，在进一步考虑之后，这些转换将被重定向或删除。设计模型这些与草图模型的不同之处在于，它们是设计的忠实记录，可在开发、测试和后续维护中参考。它们不需要解释所描述的特征是如何实现的;它们也不需要解释系统的每个特征或行为。分析模型这些是系统的忠实表示，用于模拟、验证和确认。它们通常包含的信息比设计模型少得多，并且这些信息的方向可能非常不同。例如，交互序列可以表示为单个事件，或者复杂数据结构可以表示为单个整数。测试模型在信息内容和方向方面与分析模型相似。然而，这里的目的是指导实施测试的构建。例如，模型可以准确地解释系统应该如何响应特定的消息序列。这些是实现的结构化表示;它们包含自动生成最终工作系统所需的所有信息。这些是在编程工具或交互式开发环境中呈现的模型（通常将结构化表示和可执行程序之间的返回旅程描述为图1的图表显示了这五类模型在构造方面是如何相关的：箭头表示源类的模型可以用作生成目标类模型的基础。42J. Davies等理论计算机科学电子笔记130（2005）39草图分析设计测试程序Fig. 1. 模型驱动/基于模型的软件工程值得注意的是，分析和测试类仅在应用方面有所不同：• 基于设计或程序模型构建分析模型;分析的结果可以通知进一步的草图模型，并导致设计中的改变。• 基于设计和草图模型构建测试模型;测试的结果可能导致对程序模型的改变这两个类并不是不相交的：同一个模型可以用于分析和测试。然而，目的的不同使得这是不可能的：测试模型用于检查程序是否满足设计;分析模型用于检查设计是否符合需求。在图中，我们区分了两种情况，一种是一个模型的构造基于另一个模型中包含的信息，另一种是构造被驱动。在前者，可能需要大量的创造性投入。在后者中，建造过程在很大程度上是确定的，并且自动生成应该是可能的。我们将使用术语模型驱动的软件工程来描述任何在很大程度上由模型的信息内容决定的软件工程活动。在模型驱动架构的特殊情况下，活动是程序模型的构造，或者系统本身的生产。J. Davies等理论计算机科学电子笔记130（2005）3943系统新闻集合定义SET =. ;def ==. ;枚举实用程序类别枚举... END;util = ... ;为末CLASS Class1[dim1]... 结束语：...CLASS ClassN[dimN]... 端图二. Booster模型概述3使用规范模型驱动的软件工程需要对开发发生的环境进行假设我们在这里提出的特定方法做出了以下假设：• 正在开发的系统作为一个基于对象的数据存储;• 所有外部通信将通过标准协议进行;• 不需要同时访问。其中第一个体现在建模语言的语法中，它本身是基于对象的。第二个是一个实际问题：模型不需要关心外部协议的设计。第三个是非常基本的：建模语言不能用来描述并发访问数据的效果。建模语言，暂命名为助推器，具有许多面向对象的编程符号的功能：类，关联，属性，方法，原语和枚举。然而，描述这些特征的方式更容易让人想起Z的形式符号和精化演算[4]。图2显示了用该语言编写的规范的结构。一个模型由一个单独的SYSTEM组成，它被描述为一个类的集合，在通过定义集合、枚举类型、类型同义词和外部实用程序创建的上下文中。每个类中的对象数量都有严格的限制，尽管随着系统的发展，这个限制很容易增加44J. Davies等理论计算机科学电子笔记130（2005）393.1属性该语言有两个内置类型：STRING和NAT;其他基本类型可以直接引入，作为集合，或通过枚举类或类型同义词间接引入。简单地通过编写pAtt：PTYPE来声明原始类型的属性。只要PTYPE是STRING，就使用一个额外的参数来给出预期的长度。关联信息通过引用或集值属性来描述。一个额外的参数给出了集合的最大大小，它可以是有序的（OSET）或可能重复的有序（SEQ）。 如果关联是双向 的 ， 那 么 也会给出相反属性的 名 称 。 例如， 我 们 编 写 sAtt： SET（Other.oAtt）[num]来引入属性sAtt表示对Other类对象的一组引用。预期这个集合的基数是num，并且sAtt包含对其他对象的引用当且仅当other.oAtt包含对当前对象的引用时可选属性是集值属性的特殊情况，对应于多重性为0的关联。1 .一、派生属性是用相等符号=引入的，它们的值完全由当前对象可访问的其他值确定。3.2方法方法可以与类相关联，也可以与集值属性相关联。原始方法被定义为三元组：方法（预|变更列表|员额）这应该理解为：“给定前置条件，实现后置条件，只改变改变列表中的类、对象和属性的值“。复合方法可以构造为其他方法的逻辑组合，包括为当前类或属性声明的任何局部方法。Booster中的方法组合子与Z符号的模式运算符密切对应：ALSO，顺序组合;ALL，univer-一个人，一个人;一个人，一个人;一个人，一个人。第四组合子，Occurse，对应于具有不相交前提的操作的析取：它与第一个操作（从左到右读取）具有相同的效果，其前条件满足了。图3显示了一个类的结构，有两个类级别的方法Method1和Method2，以及五个属性。 att 1是原语;att 2和att 3是引用值。att 2是一个强制性的引用，指向一个类oAttA的对象，其属性oAttA引用了这个对象;att 3是一个可选的J. Davies等理论计算机科学电子笔记130（2005）3945类别名称方法方法1、方法2属性att1：PTYPE1;att2：[A.oAttA];att3： [B.oAttB];att4： SET（SET C.oAttC）[num]METHODS方法3、方法4和方法_方法方法5、方法6;att5 = att2.oAttS ^att2.oAttT端图三. 在Booster上引用一个Class B的对象。att4是一个集值属性，包含对类attr C的对象的引用。 这个属性有两个自己的方法，方法3和方法4;这些方法的定义可能包括对本地方法方法5和方法6的引用。att4的预期大小为num。att5是一个派生属性，其值通过连接两个（字符串值）属性att2.oAttS和att2.oAttT的值获得。3.3前置和后置条件前置条件可以是任何逻辑表达式，但是为了便于自动生成，后置条件的语法受到很大的限制。有三个基本后置条件，• att=exp：属性att的值应该等于表达式exp的值;• att：sAtt：属性att应该是集值属性sAtt的元素;• att/：sAt tt：t处的属性不应是集值属性sAtt的元素。表达式exp可以是可达值（通过可导航关联链接到当前对象的对象中的属性值）和对外部实用程序的调用的任意组合。这些基本条件可以使用（）和=>组合;在一个隐含意义中，前件可以是任何逻辑表达式。&限制形式的普遍和存在的组合也是可能的;然而，它们的使用是不鼓励的;相应的方法组合子产生的描述更优雅，更容易维护。46J. Davies等理论计算机科学电子笔记130（2005）39decoration_each用于引入对象类型的绑定变量;其他装饰的使用如下：• _0：• _this：特定类的当前封闭对象（这对应于Z表示法的• _in：从方法的上下文输入的值（这对应于’• _out：输出到方法上下文的值（这对应于'！’ decoration in• _new新创建的特定类的对象。除了_0之外，这些修饰可以应用于类名（指示特定对象）或属性名（指示特定属性）。 如果属性名称在方法的作用域中是唯一的，则可以省略任何根限定：例如，Class.att1.att2可以写为att2，Classthis.att3可以写为att3。4模型扩展自动生成过程的第一步是模型扩展。该模型被扩展到包括任何默认方法的定义，并在必要时加强前提条件，以确保链接-关联实例-被保留。扩展后的模型，也在助推器，通常会比原来的4或5倍大4.1默认方法和关联每个类都有两个默认方法：• Create，创建一个新对象;• Destroy，销毁一个现有的对象。每个可选属性都有两个：• Set，设置属性;• 清，为清;每个集值属性都有四个：• Add，添加对现有对象的引用• 移除，移除对现有对象的引用J. Davies等理论计算机科学电子笔记130（2005）3947• New，向新对象添加引用，创建该对象;• 删除，删除对现有对象的引用，销毁它。每个默认方法都有一个基本定义：例如，类C的Create方法将被定义为Create（true|C| C_new：C）.它没有先决条件（true），它可以改变集合C-该类的所有对象的集合-并且它应该确保新对象C new是C的元素。除非C new已经在作用域中，否则使用修饰new将导致创建一个新对象C类的集值属性S上的默认Add方法，包含对D类对象的引用，定义如下：Add（C_this：C&S_in：D&S_in/：S|S|S_in：S）前提条件坚持当前对象是类C的对象;输入Sin引用类D的对象;并且Sin还不是S的元素。改变列表指示该方法可以改变S的值。后置条件指出，之后，Sin应该在S中。模型中给出的基数约束被添加到默认的Create和New方法的前提条件中：例如，如果类C引入了维度N，则该类的Create方法将扩展为卡片<，卡片|C| C_new：C）其中.card是内置的基数运算符。对Destroy和Destroy的前置条件和后置条件进行了扩展，以考虑模型中的关联信息如果我们要销毁一个对象O，我们必须确保没有关联对象的属性att的值包含对O的引用。如果关联的对象是P，属于D类，那么这可以通过三种不同的方式来实现(i) 如果att是设置值的或可选的，则扩展后置条件以要求改变att，如果必要的话，以移除对O的引用;(ii) 如果att是强制性的并且D不在改变列表中，则前提条件被扩展为要求att不包含对O的引用;(iii) 如果att是强制性的，并且D在变更列表中，则后置条件被扩展为要求P也被销毁。默认语义由i和ii给出。我们可以选择III，而不是通过添加D添加到更改列表中。默认方法可以通过将它们的名称添加到CLASS声明中来使用：Create和Destroy，在类级别; Set和Clear，到可选属性;其他到集值属性。当涉及48J. Davies等理论计算机科学电子笔记130（2005）39默认方法，我们可以插入附加的前置或后置条件，并添加到更改列表中：例如，声明attA：其他sAttB： SET（其他）[5]方法加上，删除（sAttB\_this/= attA|跳过）引入两个属性attA和sAttB，以及attB上的一对方法。第一个方法是默认的Add;第二个方法扩展了默认的Remove，增加了一个先决条件，要求要删除的对象与attA中当前引用的对象不同。由于单个谓词可以表示前置条件或后置条件，因此没有更改列表的方法定义必须包含两者或两者都不包含。即使只有一个是必需的--就像上面的例子--我们也必须包含另一个来消除表达式的歧义：true表示一个空的前置条件;skip，一个空的后置条件（带有一个空的更改列表）。每个方法都有相应的装饰。 在类C中，方法Create和Destroy可以使用C new和C this来引用要创建或销毁的对象。 对于可选属性att，方法Set和Clear可以分别使用attin和attthis来引用要插入或删除的对 象 。对于集值属性sAtt：方法New可以使用sAtt new来引用正在创建的对象;Add可以使用sAtt in来引用正在添加的对象; Remove和Delete可以使用sAttthis来引用正在移除或删除的对象。 可以使用in和out装饰引入其他输入和输出对象。4.2图书馆的例子图4示出了文库系统的增强模型的片段。类Person的维度值为10：在基于该模型构建的系统中，这些对象不能超过10个。 这个类的Create方法是 默认创建的扩展：将personName添加到更改列表中表示当新人员对象被创建。personName是一个基本属性：一个人的名字将被表示为一个字符串，预期长度为30。其他属性personLoans和personRequests都表示对Book类对象的引用集。在每种情况下，关联都是双向的：对于每个人p• 只要对书b的引用出现在集合p.personLoans中，J. Davies等理论计算机科学电子笔记130（2005）3949[10]第10话创建（personName）、销毁、属性public String[30];personLoans：SET（Book.bookLoanedTo）[3]添加（personLoans.card<3 |skip），Remove;personRequests：SET（Book.bookcheckedBy）[3]方法添加（personRequests_in/：personLoans|跳过），删除结束语：[50]第五十话创建（bookTitle，bookNumber），销毁属性bookTitle：String[20];bookNumber：NAT;bookLoanedTo：[Person.personLoans];bookLoanedBy：[Person.personRequests]结束语：见图4。 文库模型（片段）对p的引用将出现在集合b.bookLoanedTo中;• 只要对bookb的引用出现在集合p.personRequests中，对p的引用就会出现在集合b.books.edBy中。personLoans的默认Add方法已经扩展了一个前提条件，即任何人一次都不能借阅超过3本书;personRequests的方法有一个额外的约束，即任何人都不能请求他们已经拥有的书。图5显示了扩展模型中Person类将personName添加到Create方法的更改列表中导致了一个额外的前提条件：中的personName是一个有效的字符串。 还有一个附加的后置条件：新对象中personName的值应该等于这个输入字符串的值。Person和Book之间的关联导致了Destroy方法的附加后置条件。后置条件为所有（书）。(Book_each： Person_this.personLoans =>Person_this/：Book_each.bookLoanedTo）&要 求 如 果 一 本 书 出 现 在 personLoans 属 性 中 ， 则 当 前 人 员 应 从 相 应 的bookLoanedTo属性中删除。（注意，后置条件中逻辑蕴涵的前因是在执行操作之前进行评估。）两个附加的postcondition在销毁当前对象的同时删除对它的任何引用。personLoans的Add方法包括几个额外的先决条件。50J. Davies等理论计算机科学电子笔记130（2005）39[10]第10话创建（Person.card10personName_in：STRING| Person_new：人员|Person_new :Person&Person_new.personName =personName_in），销毁（Person_this：Person| 人员，bookLoanedTo，bookLoanedBy|为所有（书）。(Book_each：Person_this.personLoans =>Person_this/： Book_each.bookLoanedTo）for all（Book）.&(Book_each： Person_this.personRequests =>Person_this/： Book_each.bookbookbookedBy）Person_this/：Person），&属性public String[30];personLoans：SET（Book.bookLoanedTo）[3]添加（0<书.卡人_此：人&Person_this.personLoans.card3personLoans_in/：Person_this.personLoanspersonLoans_in：BookpersonLoans_in.bookLoanedTo.card = 0| bookLoanedTo，personLoans|Person_this：personLoans_in.bookLoanedTopersonLoans_in：Person_this.personLoans），&...图五.文库模型，扩展（片段）其中三个是健全性检查：引用指向预期类型的对象，输入类型非空：• 此分类上一篇：Person• personLoans in：Book• 0书.卡其中一项已明确提出：• 人this.personLoans.card<3另一个例子说明了我们对Add的严格解释：如果对象已经是set的元素，则• personLoans in/：Person this.personLoans最后一个前提条件特别有趣：它是Set方法对相反属性的前提条件的结果：• 个人贷款in.bookLoanedTo.card=零此方法的附加后置条件坚持使用对当前人员的引用更新bookLoanedToJ. Davies等理论计算机科学电子笔记130（2005）39515代码生成扩展后的模型在随后的编译过程中充当源代码。该模型先被翻译成抽象的机器符号，然后通过B规则库被翻译成C源代码，最后使用标准的B工具包库进行编译。5.1方法实现方法的实现非常简单：前置条件成为要计算的布尔表达式，后置条件成为程序语句.在最简单的情况下，• 原始后置条件a=e被实现为简单赋值a：=e;• 原始后置条件a：s和a/：s使用从集合中添加或移除元素的函数来实现• 逻辑蕴涵是使用条件if实现的。然后施工;• 逻辑合取使用语句的顺序组合来实现：c1;c2每个操作都用代码包装，如果操作的任何部分失败，这些代码将自动恢复原始状态。上下文信息用于解决歧义：例如，以下定义中的后置条件可能允许两种替代实现：方法（a<10 &b> 3 |B |a = b）我们可以满足这样的要求，即a和b的“after”值是两个w的值：a：=b或b：= a。然而，a没有出现在更改列表中，所以第一个是不允许的;后置条件必须实现a sb：= a。如果无法解决模糊性，或者定义似乎不一致，则需要修改模型。例如，如果上述定义被替换为方法（a<10&b> 3|甲乙丙|a= b）则编译过程将停止，报告变更列表中同时存在a和b将与a= b的使用不一致，后置条件编译器可以选择一个实现--两个赋值中的任何一个--但最好是它应该发出错误信号：52J. Davies等理论计算机科学电子笔记130（2005）39这个定义至少有一部分可能是错误的。模型的作者可以通过从更改列表中删除其中一个变量，或者通过使用 0：后置条件a=b 0说明操作后a的值应该等于b的值在操作被调用之前;然后这个条件将使用赋值a：= b来实现。5.2界面和文档方法实现构成到底层数据存储的编程接口。这个接口不是直接访问的：相反，请求排队等待解码器组件进行顺序处理。为了使前置条件和后置条件的组合作为方法m的充分描述，必须不存在另一种方法更新变量在前或后条件中，而m仍在执行。请求和响应以结构化语言表示，使用与模型操作相对应解码器逻辑与编程接口和数据存储同时生成。如果系统具有用户界面，则还可以生成该界面的组件以及用户文档。尽管扩展后的模型可读性很强，但有时候用一个前提条件的音译来增强界面是有用的：例如，操作Enrol的不可用，可能对应于网页上按钮的“The operation在助推器技术的这一方面花费的精力相对较少：目前，这样的信息如下：“前提条件：姓名：已注册学生注册。卡类容量”然而，这些信息的计算和呈现在为模型开发提供反馈方面可能非常有价值6模型演化在基于模型的开发中，即使最初的程序设计与模型完全对应，这种对应也常常会随着开发而减弱J. Davies等理论计算机科学电子笔记130（2005）3953收益。在实现或维护过程中获得的额外见解可能会导致未正确纳入模型的更改：一旦生成代码，它就成为关注的焦点，而模型则被忽略。模型驱动的方法消除了这个问题，但另一个问题仍然存在：对模型的每次更改都会产生系统的新版本，但以前版本可能收集的数据呢？booster编译器就是为了解决这个问题而设计的。在生成系统的每个新版本时，编译器会将新模型与用于生成先前版本的模型进行比较。如果它可以确定模型是如何被转换的，它就可以对已经收集的任何数据如果转换是一个小的，那么这个数据升级过程将是完全自动的。在新版本的系统中，生成代码来创建对象和设置属性值;以前版本的数据以与新模型匹配的形式存储;根据关联约束检查数据的完整性;最后，执行代码以创建新系统并安装数据。较小的改造包括：• 重命名类和属性;• 删除类和属性;• 添加新的类、集合或枚举;• 添加集值或可选属性;• 添加原始属性。在某些情况下，不需要数据升级：以前版本的数据当模型的唯一更改涉及以下内容时，即为这种情况：• 添加、删除或修改方法;• 添加、删除或修改派生属性。其他转换可能会使直接的自动升级变得不可能;因此可以采用两种策略(i) 将转换表示为一系列较小的转换，每个转换都允许自动升级;(ii) 引入第三个中间模型，并将所需的升级转换指定为该模型中的方法在某些情况下，只有第二种策略才能成功。例如，要向类C引入强制引用值属性att，54J. Davies等理论计算机科学电子笔记130（2005）39默认对象值，我们需要引入一个中间模型，其中属性是可选的。这个模型可以包含一个方法升级（ALL C THEN Set_att（...）结束）其具有设置属性的每个实例的效果。 调用此方法后，可以自动升级到强制使用att的型号。7讨论在本文中，我们描述了一个模型驱动的方法，软件工程，围绕使用一个新的基于对象的语言。这一方法已通过应用得到发展：已编制并正在维持若干大型案例研究，包括为商业客户编制的两个系统。该语言的灵感来自于Z，并使用B实现，结合了形式化技术和代码生成，已被证明特别有效。迄今为止，最大的系统是一个拥有1000个用户的在线数据库系统：该系统的模型是3000行长，并保持完美的可读性;实现由300000行（生成）C程序，相当于也许30000行手写代码。对该系统的要求仍在不断变化，目前的型号为88.03版。系统从来没有失败过;它已经停止了，但只有当模型说它应该这样做的时候。进一步开发的潜力很大：例如，已经创建了一个助推器系统来管理开发，更新作为对象的助推器模型;采用这种方法，有可能使更广泛的数据升级自动化。编译器可以被重定向以生成Java或C#，并且添加库以构建其他类的系统。尽管在整合形式化方法方面已经做了大量的工作--特别是在将Z与B结合，以及将B与UML结合[9]--我们不知道在这一领域有任何工作也解决了如何从前置条件和后置条件生成方法实现的问题;重点是对建议的实现进行验证。一个重要的参考点--从本文的介绍中应该可以清楚地看到--是关于模型驱动架构的工作[1]，以及对象约束语言（OCL）的进一步发展[2]。我们对booster的使用将其作为一种高级编程语言，这是从机器代码到Cobol，到C，再到J2EE的又一步，. NET。对于一个特定的应用程序类，至少，我们已经准备好编程J. Davies等理论计算机科学电子笔记130（2005）3955在正式的方法。引用[1] D. S.弗兰克尔，模型驱动架构。Wiley 2003.[2] M. 福勒UML Distilled：A Brief Guide to the Standard Object Modeling Language. Addison-Wesley 2003.[3] D. Harel和E.格里使用Statecharts进行可执行对象建模。30.第三十章一九九七年。[4] C. C. Morgan. 编程从规格。 普伦蒂斯 大厅 1990. （可于http://users.comlab.ox.ac.uk/carroll.morgan/PfS/网站。[5] P. Naur和B.兰德尔软件工程：关于1969年北约科学委员会主办的会议的报告。[6] S. A. 施耐德B方法。Palgrave 2001.[7] C.斯努克和M.管家U2B-UML到B翻译工具.可用 在http://www.ecs.soton.ac.ukwww.example.com/cfs/U2B下载/U2 B下载[8] J. M.斯皮维Z符号：参考手册。Prentice-Hall International，第二版，1992年。[9] H.特雷哈恩用B补充UML开发过程。在FME 2002会议录中：形式方法第2391章. 2002年。
我的内容管理
展开
