没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记133(2005)159-174www.elsevier.com/locate/entcs面向对象概念与形式B规范的Akram Idani,Yves LedruLaboratoireLoggiciels,Syst`emes,R′eeaux-IMAGUniversit′eJosephFourier法国格勒诺布尔摘要本文使用UML类图讨论了B规范静态方面的图形表示这些图表可以帮助不熟悉B方法的利益相关者(如客户或认证机构)了解具体情况。本文首先讨论了类图的一些初步推导规则然后从面向对象的角度研究了初步识别的概念的一个正式的概念分析技术用于区分一致的类,属性,关联和操作。所提出的技术是逐步增加操作到正式规范,自动导致类图的演变关键词:B,UML,集成方法。1介绍形式化方法是当今最严格的软件生产方法。它们提供了一些技术来确保规范的一致性,并保证某些代码实现了给定的规范。涉及安全关键活动的几个行业,如铁路行业,已经意识到这种方法的好处,并且像巴黎流星地铁这样的重大发展已经部分使用正式方法进行[1]。尽管如此,虽然形式化方法提供了验证问题的解决方案(1 电子邮件:{Akram.Idani,Yves.Ledru}@ imag.fr1571-0661 © 2005 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2004.08.063160A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159正确的困难之一是确保关键项目的各个利益相关者(开发人员、客户、认证机构)就正式规范的含义达成一致通常情况下,在正式的方法,其数学概念和符号,以及在这样的项目中的各种利益相关者的常用技术(图形格式和自然语言文档)之间存在文化差距因此,存在一个重大风险,即错误(如对要求和规范文档的误解)导致错误地验证规范,从而产生错误的系统。为了弥合这一差距,一些研究团队提出了整合形式和图形规范的方法[14,15]。一种可能的集成策略是为现有的符号提供图形语法,例如在90年代早期,Dick和Loubersac [5]提出了VDM的图形语法。另一种方法是设计集成形式概念的工业语言。这种方法是几种UML符号开发的例如 , UML 状 态 转 换 图 深 受 几 种 状 态 机 语 言 的 影 响 , 特 别 是STATECHARTS[9]。此外,对象约束语言[23]包括来自基于模型的规范语言(如Z[20])的概念。研究界已经投入了大量的精力来建立UML和形式化方法之间的联系。特别是,几种方法提供了从带注释的UML图到形式化方法的转换[6,11,13,16,18,19]。这些方法的目的是利用形式化的方法和工具,同时保持集成在一个基于UML的标准工业过程中。本文研究了相反的方法:使用图形符号,如UML图,作为一种方式来记录正式的发展。它始于这样一个事实,即几个重要的形式化发展主要基于形式化方法。例如,B方法已用于工业铁路[1]和智能卡[4]应用。此类关键应用通常必须由独立认证机构接受,这些机构不一定是正式方法方面的专家。因此,从正式开发中构造图形视图作为附加文档是有意义的。预计这些更直观的表示将更容易被认证机构接受。可以使用两种工具来构建图形表示:(i) 提取B规范的静态方面的工具。 例如[21]定义了一些规则来自动导出UML类图A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159161从正式的B规格。在相同的上下文中,[7]提出了一些可以构建交互式更简单的图表的方法。(ii) 表示规范行为的工具。[2]是推导给定B规范行为的视觉表示的第一个建议。这种行为使用有限标记转换系统(LTS)来描述。从用户引导的重要状态的选择开始,证明技术用于探索系统的所有有效转换。由此产生的LTS,然后可以进一步重用,以验证时序逻辑属性的模型检查。在相同的上下文中[22,8]提出了一些从B规范生成状态图的推导规则。最后,在[17]中,提出了一个辅助B规范动画的工具,它也有助于构建状态转换图。在这些图中,状态是B变量的赋值,转换是一些操作调用。本文研究了第一类工具,它从现有的形式规格中提取结构视图,以便于理解和维护。结构信息的提取是软件维护领域的一个经典问题。事实上,理解应用程序是如何组织的是维护它的一个主要因素,特别是当它的结构复杂,文档不可用或过时时。大多数程序理解技术的目标是对软件进行模块化的重构,以便于软件的维护。我们相信,类似的技术可以应用于正式规范。本文提出了一种从B规范构造类图的两步方法。• 第一步(第2节)将生成规则应用于B规范,将B概念转换为类图的元素。它接近现有的方法,如[21,7]。• 虽然第一步只涉及B规范的变量,但第二步(第3节)也考虑了运算。一个概念依赖技术被用来帮助定位每个操作的适当类。第4节进一步研究了类图对B规范演化的鲁棒性最后,Sect。第五章总结了本研究的结论和162A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)1592生成初步的类图UML类图和B共享类似的概念,例如操作和变量的封装这促使一些研究将一种语言翻译成另一种语言。本节将强调如何利用概念的重叠来自动将B规范转换为UML类图。将UML图转化为B形式规格说明的方法给出了图形概念和形式概念之间的不同可追溯性规则。例如,在[11,12]中,类c被转换为给定集合Sc和变量集合Vc以及不变属性:Vc<$Sc。由于推导是自动进行的,我们认为这可能是明智的,进行类似的推理,并从正式的B规范给出的信息中导出UML图。例如,在一个正式的B规范中,一个给定的集合Se可以被看作是一组对象的抽象,并且可以被转换为一个UML类。2.1一个简单的例子网络控制规范是对授权用户访问网络资源的控制。 相应的B规范在例2.1中给出。实施例2.1机器人控制集用户;资源;地址变量已允许、已禁用、IpAdress、未使用不变Permitted∈USERSParticipRESOURCESIpAddress∈ADDRESSES>RESOURCES ∈USERS→RESOURCESPermitted未使用的资源未使用的样本量(μ)=μ初始化允许,:=,||IpAddress,Unused:=,操作添加权限(用户,资源)=预user∈USERSresource∈资源(user›→resource)/∈允许然后允许:=Permitted{user<$→resource}端st←列表用户(资源)=预资源∈资源然后st:=dom(PermitteddD{resurce})结束语:分配资源(用户,资源)=预user∈USERSresource∈ RESOURCES(user ›→resource)∈Permitted_user/∈dom(assigned)然后:=分配数据{user<$→resource}端端此规范具有三个抽象集,分别是USERS,RE,A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159163来源和地址。网络资源本质上是通过其IP地址(变量IpAddress)识别的计算机。用户必须具有访问给定资源的权限(变量Permitted)。一个用户一次只能使用一个资源。变量“”表示用户正在使用某个资源。最后,称为Unused的RESOURCES子集给出了未使用资源的集合。我们考虑三种基本操作:• AddPermission(user,resource):向给定用户授予访问资源的权限;• 列出用户(资源):列出有权访问给定资源的用户;• Assign Resource(user,resource):将用户分配给他有权使用的资源。2.2类图的派生规则本节将提出一些初步的规则,用于直接从B规范的变量和常量导出类图。我们将尝试找出B和面向对象概念之间的类比2.2.1类在面向对象的范例中,类表示具有共同特征的实体的抽象。它表示一组具体的对象,这些对象被称为实例。对象存在的形式化可以独立于对象本身的结构来完成。它只需要一组对象标识。这是B中集合的典型概念,它允许我们将它们识别为某些具体元素的抽象表示规则1:B规范中的集合对应于UML规范中的类。例 如 , 我 们 为 例 2.1 的 机 器 识 别 了 三 个 类 , 分 别 是 USERS 、RESOURCES和ADDRESSES,它们对应于SETS子句中声明的抽象集2.2.2协会关联是表达类之间关系的双向连接它是对类的对象实例之间可能存在的联系的抽象。当我们将抽象集合转换为类时,关联将是这些集合之间存在的每一个关系。规则2:B规范中的关系对应于UML规范中的关联。164A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159在图1中,Permitted和Permitted作为用户之间的关联出现和资源在UML中,一些约束应该在一个关系或一组关系上表达。例如,在机器不变量控制中,机器不变量属性定义了两个关系Permitted 和Permitted之间的约束。该约束可以被看作是两个集合(也称为角色)之间的传统子集分配允许图1.一、包含约束的可视化2.2.3角色关联的极端定义了一个角色,它是源类的伪属性。在B规范中,没有概念能够用户允许资源我们的和平图二、派生类图中角色的标识可以追踪到某个角色然后,我们选择手动将角色标识为已标识的源类名及其关联名的前两个字符2.2.4多重性UML中的多重性是对对象之间可能存在的链接数量的约束。B关系的特化对应于各种多重性约束。规则3:使用下表从B规范中推导出倍数:关系类型符号一B关系类型符号一B关系A参与者B**部分满射A→›B1. *0..1部分A→›B*0.. 1全满射A→ B1. *1总A →B*1部分双射A→>›B10..1部分喷射A>›B0..10.. 1全双射A→>B11总喷射A> B0..112.2.5继承由于集合和类之间的等价性,子集的概念可以转化为子类。与类泛化机制类似,用户联系我们v资源A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159165集合B设置分配*re as联系我们我们是0…1*雷佩允许v*美国体育1IP地址re ipad ip0..1地址未使用资源用户集合包含定义了一组对象的概念性子集合规则4:B规范中的一个子集被转换为UML图中的一个特殊类。设置A设置B图3.第三章。子类的形式化和面向对象的概念匹配2.3讨论应用前面的规则,我们得到图。四、见图4。 用于EQUIPControl规范虽然我们相信图4给出了一个访问控制规范的可读图,但我们担心本节中给出的规则的系统应用特别是,每一组值,包括基本类型的集合,如INTEGER或STRING,都会导致相应的类。例如,如果指定包含一个名为Name的字符串变量,并且定义为:Name∈ USERS→ STRING,我们将获得一个由fig表示的结构。五、用户*姓名1字符串图五. 表示数据结构的直观名称应该是所考虑的类的属性。为了区分类别候选者和属性候选者,Sect.3将考虑访问这些属性或类的B规范的操作。我们仍然相信,这第一步提供了可比或更好的结果比现有的方法。166A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159用户资源:资源允许:{资源}添加权限(r:RESOURCES)分配资源(r:RESOURCES)地址IP地址:RESOURCES[21]中给出的规则为B规范的每个机器、集合和关系生成类。此外,这些类别由许多协会联系在一起。只有布尔和整数变量成为这些类的属性。这会导致比我们的方法更多的类,因此会导致更复杂的图。在[7]中,类是根据一个简单的规则导出的,如果一个关系的定义域对应于一个抽象集,则该规则将该关系的定义域标识为类。在例2.1中应用这个规则,我们得到两个类,它们对应于没有关联的集合USERS和ADDRESSES(图6)。关系Permitted和IpAddress然后被认为是由它们的共域RESOURCES类型化的属性。[7]给出的经验规则导致了一个不完整的类图,它图六、使用[7]的规则生成的控制器控制机的类图3考虑到业务上一节已经确定了一组候选类别。在本节中,我们将尝试将这些候选项分类到潜在的类或属性中。为了评估类候选的相关性,将建立一个概念依赖上下文,将类候选与规范的操作联系起来。我们的研究集中在B操作和初步类图中识别的数据之间的依赖性。首先,我们研究了B操作和类之间的关系和协会的初步类图,以确定它们的相关性从面向对象的角度来看。然后,我们决定这些元素在相关类图实体上的分布。最后,我们添加B规范的其他数据作为定义的类的属性。我们可以非正式地定义相关性如下:• 一个操作与一个类的相关性衡量将这个操作关联为类的方法是否有意义。• 一个类是相关的,如果它的所有方法都是相关的。没有方法的类相关性低A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159167• 如果关联链接相关的类,则它是相关的。因此,相关性是根据操作相关性来定义的。为了衡量操作相关性,我们使用了概念依赖图。初步结构和操作的元素形成了一个上下文,称为概念依赖上下文。在定义的上下文中,我们只考虑由操作操纵的初步类图中的概念因此,概念要么对应于类,要么对应于联想。B操作和初步识别的概念之间的依赖关系被形式化为二分图G。该图是概念依赖性上下文的表示,其形式上表示如下:定义3.1一个概念dependancecontextG=(C,O,I)包含两个集合C和O以及C和O之间的二元关系I(其中dom(I)= C)。O的元素是所考虑的B规范的操作,C的元素是与规范中的某些形式元素相对应的初步识别的概念。概念c(c∈C)与运算o(o∈ O)相关当且仅当o使用对应于c的形式数据。概念依赖性上下文的定义需要更精确地定义操作对概念的“使用”。在B方法中,我们可以确定三种(i) 修改:操作访问和修改与概念相(ii) 读:执行操作需要对与概念(iii) 前置条件访问:操作的前置条件是指概念对应的我们选择只处理在操作规范中明确出现的概念因此,在我们的方法中,“用途”被定义为对所考虑概念的明确引用。例如,概念USERS不会与操作List USERS联系起来处理,因为它定义3.2对于一个概念集合A C,我们定义:Op(A)={o|o∈ O<$$>c·(c∈ A <$(c,o)∈ I)}A.中的概念所共有的一组运算。定义3.3对于概念依赖上下文G,我们定义最大概念部分,使得:168A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159c∈max ( G ) 惠 s· ( s∈ C-{c}<$Op ( {c} ) /<$Op({s}))其中max(G)是G的所有极大概念部分的集合.例3.4从概念控制规范发出的概念依赖上下文G这个图仅仅意味着在一个概念和另一个概念概念,一个操作和另一个操作之间没有弧线。所有的弧线都是从一个概念到一个操作。 所考虑的图由以下集合定义:除了C={用户,资源,许可,授权},操作集合O ={添加许可,列出用户,分配资源},以及对应于图7中给出的关联函数I的匹配。 虽然AD-在图4中,DRESSES、Unused和IpAddress被确定为初步概念,它们请注意,概念集包括类和关联。在这个例子中,RESOURCES和Permitted是最大部分;因此max(G)等于{RESOURCES,Permitted}。见图7。从控制机我们现在可以定义类或关联的相关性概念:定义3.5类c(c∈ C)是相关的i <$c∈ max(G)。定义3.6两个类c1和c2之间的关联a(a∈ C({c1,c2}∈ C)是相关的i <${c1,c2}∈max(G)且Op(a)<$Op(c1)<$Op(c2).相关的概念将成为类图中的类和关联。出现在初步类图上的其余类和关联,以及不相关的,将成为相关类的属性。规则5:类图以所有相关的类和关联为特征。规则6:非相关类c1(c1∈ C)成为类c2(c2∈ C)i <$c2∈max(G)和Op(c1)<$Op(c2)中的属性或属性类型。A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159169根据非相关类的定义,我们知道至少存在一个c2如果几个相关的类都可以将c1作为属性,那么选择权就留给了分析师。对于关联和操作也给出了类似的规则:规则7:一个非相关关联a(a∈ C)成为类c(c∈ C)i <$c∈max(G)中的一个属性,并且Op(a)<$Op(c)。然后,被标识的属性将由关联a的一个极端类型化。规 则 8 : 运 算 o ( o∈ O ) 成 为 类 c1 ( c1∈ C ) i <$c1∈max ( G )<$ ( o∈Op ( c1) <$ ( <$c2·( c2∈ C <$c2∈Attributes ( c1 ) <$o∈Op(c2)中在我们的例子中,我们有max(G)={RESOURCES,Permitted}。这组最大部分只包括一个类(资源)。按照我们的规则,它成为类图中唯一的类(图8)。其余图7的概念成为该类的属性或类型。由于B规范的三个操作都使用了RESOURCES,它们就成为了这个类的方法。虽然允许是最大部分,但它不是相关关联,因为它不满足定义3.6。此外,遵循规则6,USERS可以成为属性或类型。由于它是一个常量集,我们觉得它应该被建模为一个类型。初步图中的某些概念(ADDRESSES、IpAddress、Un- used)不再出现在结果图中.实际上,由于我们的规则是基于操作对这些概念的使用,不参与B机器行为的概念不会出现在结果图中。资源允许:用户用户名[*]:添加权限:USERS列表USERS():设置(USERS)分配资源:用户图8.第八条。来自控制机器的相关类图与其他方法的比较。[21]的方法系统地将B机器的操作分组在与机器对应的类中。在第4节中,我们将看到我们的方法并不总是导致将所有操作分组到一个类中。我们认为,当B机器变得更大时,这种在几个类之间共享操作的能力是绝对需要的。170A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159图6是将[7]中的规则应用于控制实例的结果。事实上,从这个类图中不可能找到资源的用户列表(操作List USERS)。这样的操作不能是类USERS 的 方 法 , 因 为 它 引 用 了 该 类 的 多 个 实 例 。 它 必 须 是 类RESOURCES的一个方法不幸的是,RE- Sources只在fig中作为一个类型出现。六、因此,应用我们的方法生成的图(图8)更正确。因此,我们认为,我们的方法的第二步,它考虑到操作来评估类的相关性,结果在现有的方法的改进。4B规范的增量开发及其对B图形表示的影响本节将研究B规范演变时图形表示的稳健性。我们引入了一个操作,它将资源分配给一个用户。将该操作引入到先前的上下文中修改了概念依赖上下文的图形表示,如下所示:图9.第九条。一个新的概念依赖上下文,增加了操作列表资源有了这个新的上下文,最大概念部分变得等于{用户,资源,允许}。最初被确定为初步类别的两个概念现在被确定为相关的。封装共享操作(添加权限和分配资源)的类可以无论是USERS 还是RESOURCES ,我们都可以任意选择将它们放在USERS 类 中 。 关 系 Permitted 和 Risk 成 为 两 个 相 关 的 关 联 , 因 为 Op(Permitted)RiskOp(USERS)RiskOp(RESOURCES)和Op(用户)Op(用户)Op(资源)。 图10显示了结果-创建类图现在让我们添加三个其他操作:- Change IP(ip,resource):更改资源的IP地址;A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159171见图10。 一个演化的类图,用于控制规范- 取消分配资源(resource):取消分配资源并将其添加到未使用的集合中;- Disconnect(unused):通过删除其IpAddress断开未使用的资源。这些操作将更改新上下文的表示,如下所示:见图11。 可编程控制规范图11所示的概念依赖上下文具有以下性质:• max(G)={RESOURCES,USERS,Unused,Permitted}导致选择RESOURCES、USERS和Unused作为新图表的类。• Op({ADDRESSES})表示类ADDRESSES的不确定性,并将其转换为类RESOURCES的类型;• Op({IpAddress})表示关系IpAddress作为关联的非相关性,并将其转换为类RESOURCES的属性。最后,图中给出了生成的类图。12172A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159re作为*分配0..1雷佩美国体育添加权限(d:RESOURCES)分配资源(d:RESOURCES)列出资源():设置(RESOURCES)用户*未使用List users():Set(USERS)DeassignResource()Change IP()IpAddress:地址资源t}v*(subse)允许Disconnect()美国成为图12个。最后给出了工控机的相关类图5结论和展望虽然形式化方法为系统的精确描述提供了优秀的技术,但理解这些描述通常仅限于专家。本文提出了一种技术,有助于建立一个图形表示的静态方面的B规格。这些图表预计将比原来的正式规范更直观和可读本文提出了一种从B规范构造类图的两步方法。第一步将系统化的转换规则应用于B规范,并生成一个初步的类图,其目标是识别候选概念。第二步将这些概念与B操作联系起来,并保留最相关的概念。这第二步是相对于现有的方法,如[7,21]原创。我们已经领导了几个案例研究与三种方法,包括本文中提出的一个在每一种情况下,我们都认为我们的方法至少与其他方法一样好。尽管如此,我们的方法仍然存在一些限制:• 由此产生的图的主要限制是,它提供的信息不如正式规范所表达的信息完整。其他视图,例如[2,17]构造的动态视图,需要提供B规范的完整图形文档• 我们的方法的起点是单个B机器。需要进一步的工作来解决具有几台机器或涉及改进的规范。• 我们只利用了UML类图的原语的一个子集。诸如关联类、聚合和组合等构造可能会丰富我们的方法。A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159173• 需要进一步的实验来帮助我们理解我们的方法是如何扩展的。在未来几个月里,我们打算解决其中的几个限制。 我们还计划试验替代逆向工程方法,解决概念的形成。形式化方法与现有的图形符号的成功集成工业界不会放弃目前的做法,但愿意扩大和加强这些做法。我们相信,像我们这样的方法对于弥合当前行业实践与正式方法社区的建议之间的差距是一个小小的贡献。引用[1] Patrick Behm,Paul Benoit,Alain Faivre和Jean-Marc Meynadier。METEOR:B在大型项目中的成功应用。在J.M. Wing,J. Woodcock,and J. Davies,editors,Proceedings ofFMSpringer,1999年。[2] D. Bert和F.洞从B抽象系统构造有限标号迁移系统。1945年,在《计算机科学讲义》(LectureNotes in)中。Springer-Verlag,2000.[3] J.C. Biclobgui。形式化方法的实践:应用B方法的案例研究IEE Proceedings on Software Engineering,144(2):119[4] L. 卡赛特使用形式化方法开发嵌入式java卡字节码验证器在FMESpringer-Verlag,2002.[5] J·迪克和J·卢伯萨克。集成结构化和形式化方法:VDM的可视化方法。以. van Lamsweerde和A.Fugetta,编辑,欧洲软件工程会议论文集(ESEC '91),计算机科学讲义第550卷。Springer-Verlag,第37-59页,1991年10月。[6] S.杜普,Y。 Ledru,andM. 你好- Versuneinte gr at ionut ileden tat ionsemi- formelle setformelles:unexpincenUMLetZ. L'objet t,nu m'e r o t h'e m at iq u e App r o chesforo r mel l le s'a o b jets,6(1),2000.[7] 我 的 意 思 是 , 我 的 意 思 是,Transfororm at iond esspec i ficationnsBendesdiagramesUM L.InAFADL:ApprochesFormellesdansl[8] A.哈马德湾Tatibouet,J.C. Voisinet和Wu Weiping。 从B规范到UML状态图。第四届形式工程方法国际会议[9] D. 哈雷尔复杂系统的可视化形式。计算机科学Programming,8(3),1987.[10] A.井谷项目图表文件B。2003年,法国格勒诺布尔,约瑟夫·傅立叶大学,DEA报告174A. Idani,Y.Ledru/Electronic Notes in Theoretical Computer Science 133(2005)159[11] R. Laleau和A.妈妈 概述了从UML符号生成B规范的方法及其支持工具。自动化软件工程国际会议(ASE2000)IEEE CS Press,2000.[12] R'egineLaleauandFionaPolack. ComingandgoingfromUMLtoB:在严格的IS开发中支持可追溯性的一种在ZB[13] K. 拉诺形式化的面向对象开发。Springer,1995年。[14] K. Lano 和 S. 戈 德 萨 克 整 合 的 形 式 化 和 面 向 对 象 方 法 : VDM++ 方 法 。 In A.Bryant andL.Semmens , editors , MethodIntegrationWorkshop , ElectronicWorkshopinComputing,Leeds,Mars 1996. 史普林格出版社[15] K. 拉诺,H.Houghton和P.维勒面向对象系统开发中形式化与结构化方法的集成在形式化方法和对象技术中,第7章。Springer,1996年。[16] 洪力和我都是一个人。 Contri b utionsforrmodelingUMstate-chartsinB. InIntegrated FormalMethods,Third International Conference,IFM 2002,Volume 2335 ofLecture Notes inComputer Science,pages 109[17] 迈克尔·鲁舍尔和迈克尔·巴特勒。ProB:B的模型检查器在Keijiro Araki,Stefania Gnesi和DinoMandrioli,编辑,FME 2003:形式方法,LNCS 2805,第855Springer-Verlag,2003.[18] 埃米尔·塞克林斯基反应系统的图形化设计。在B'98:第二届国际B会议,B方法的发展和使用的最新进展,计算机科学讲义卷1393。Springer-Verlag,1998.[19] C. 斯努克和M.管家使用图形设计工具进行正式规范。在程序设计兴趣小组心理学第13届年度研讨会的会议记录中,2001年。[20] J.M.斯皮维Z符号-参考手册(第二版).普伦蒂斯·霍尔1992年[21] B. Tatibouet,A. Hammad和J.C. Voisinet。从抽象的B规范到UML类图。2002年12月,在摩洛哥马拉喀什举行的第二届IEEE信号处理和信息技术国际研讨会[22] B. Tatibouet和J.C. Voisinet。生成状态图B规格。在第16届软件和系统工程及其应用国际会议[23] J. Warmer和A.克莱珀对象约束语言:用UML精确建模。艾迪森·韦斯利,马萨诸塞州雷丁,1999年
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功