没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记243(2009)69-87www.elsevier.com/locate/entcsBAS:可信模型驱动开发中Dehui Du,Jing Liu1,4华东师范大学上海市可信计算重点实验室曹红花2武汉大学软件工程国家重点实验室,武汉,中国。中国张苗苗3同济大学软件工程学院,上海,中国摘要多视图建模和关注点分离被广泛应用于降低大型软件系统的设计复杂度。为了保证多视图需求模型的正确性和一致性,需要将形式化验证技术应用到模型驱动的开发过程中。然而,严格的建模方法仍然缺乏统一的理论基础和工具支持。为了解决这些问题,我们实现了一个集成的建模和验证环境tMDA(TrustableMDA)。 在tMDA中,开发人员使用UML静态和动态模型对系统需求进行建模,并验证不同模型的正确性和一致性。提出了一个多维模型,支持一致性验证、活性和安全性验证、OCL约束和LTL公式验证.介绍了一个银行ATM系统(BAS),以演示如何利用tMDA的设计和验证。保留字:MDA、验证、合同、UTP、LTL1介绍软件的复杂性不断增加,软件的正确性越来越重要。如何开发复杂的应用程序并保证1电子邮件:dhdu@sei.ecnu.edu.cn,jliu@sei.ecnu.edu.cn2电子邮件地址:caohonghua@hotmail.com3电子邮件地址:miaomiao@mail.tongji.edu.cn4 通讯作者1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2009.07.00670D. Du等/理论计算机科学电子笔记243(2009)69软件的正确性越来越引起研究者的兴趣。基于构件的模型驱动开发是一种很有前途的软件复杂性处理方法该方法采用多视图UML建模并允许分离关注点是至关重要的[1]。不同的关注点在不同的抽象层次上从不同的角度描述系统,包括接口、功能服务、同步行为、交互协议、资源和时序约束。然而,没有严格的理论基础和集成工具来支持开发过程中产生的不同模型的规范和验证[2]。契约式设计(DbC)是一种软件正确性方法[3]。它使用前置条件和后置条件来记录(或以编程方式断言)由程序片段引起的状态更改。DbC的思想已经被工业界所接受,例如,Ei el语言已经取得了巨大的成功[4]。契约可以用来提高软件的可靠性,但如何用UML对契约进行建模仍然是一个挑战。众所周知,在开发过程的早期引入的错误具有显著更高的纠正成本[5]。在软件开发过程中,构建高质量的软件模型可以避免将设计错误传播到实现阶段。因此,模型检查器应集成到模型驱动开发环境中,用于检查不同模型的一致性和系统需求中的约束。在过去的半个世纪里,语义基础、形式化技术和验证工具得到了发展,包括测试、静态分析、模型检验、形式化证明和定理证明等。然而,这些形式化验证技术并不容易应用到实际开发过程中。它缺乏一个集成的建模和验证环境。最近,我们探索了如何将模型检测技术应用到模型驱动的开发过程中。实现了一个集成的建模和验证环境,我们工作的新特点是:• 实现了一个基于MDA的可信软件开发方法的集成建模和验证环境。我们称之为tMDA(Trustable MDA)。• tMDA有效地支持用例驱动的需求分析和建模方法。开发人员可以对系统的静态结构和动态行为进行建模。在模型层次上验证不同模型之间的一致性,保证了PIM模型的正确性。此外,tMDA支持模型仿真,这有助于开发人员分析模型并定位错误。最后,将可信模型转化为C++代码框架.• 在模型层次上用OCL表达式对合约进行建模,使某些方法的前置/后置条件约束可以表达出来。特别地,OCL扩展约束可以被添加到状态图的转换中。由于SPIN的断言验证,可以验证OCL约束此外,我们认为,D. Du等/理论计算机科学电子笔记243(2009)6971tMDA可以自动将OCL表达式转换为生成代码框架中的前置/后置条件语句,方便了DbC在模式驱动开发过程中的应用。本文的其余部分组织如下。第2节概述了tMDA的框架,并提供了一致性验证的一些关键概念的制定在第三节中,我们通过一个BAS案例,展示了模型驱动开发过程中的模型构建、模型验证、模型仿真和代码生成的过程,以及如何将严格建模方法应用到实际的软件开发中。第四部分总结了我们的工作,并讨论了一些未来的工作。2tMDA:可信的模型驱动开发环境该方法的主要思想是为开发人员提供一个集成的建模和验证环境,以便他们可以构建系统需求模型并验证这些多视图模型的正确性和一致性。该方法有助于发现早期设计错误,保证模型的质量,为基于构件的模型驱动开发可信软件提供了可能。tMDA严格的统一理论基础是基于Hoare和何继锋的UTP[ 6 ],它为统一不同视图的模型提供了语义,并支持一致性基于RUP开发过程[7],我们提出了tMDA的框架,它使整个软件开发过程从需求获取、模型构建、基于构件的体系结构设计到代码生成变得容易。tMDA的主要功能如图1所示:开发人员可以通过“Edit models“对系统需求进行项目模型通过tion一致性验证是指验证UML状态图和序列图之间的动态一致性。用例“此外,质量类图和状态图的C++代码框架是自动生成的,这是由用例“代码生成“描述的2.1tMDA框架tMDA的框架如图2所示,主要包含四个模块:模型编辑器、模型验证器、模型模拟器和代码生成器。这四个模块分别完成上述功能。该框架的控制流程如下:• 开发人员在“模型编辑器”中对系统需求建模• 在”模型编辑器“中生成的UML模型72D. Du等/理论计算机科学电子笔记243(2009)69Fig. 1. tMDA的主要功能图二. tMDA框架lator• 另一方面,UML模型可以转换为模型检查器的输入语言,这是通过“模型转换”来完成的然后,模型检查器被激活,以验证UML模型。如果检测到错误,则反例将由“模型生成器”生成在反例的帮助下,开发人员可以修改模型。反例引导的精化方法由E.M.Clarke提出[8]。然而,如何引导开发人员修改模型仍然是一个棘手的问题。在本文中,我们试图提出一个可行的解决方案。• 验证后的模型可以通过“代码生成器”转换为高质量的代码生成的代码可以保存在“代码库”中,该框架具有通用性和可扩展性的特点。众所周知,不同的模型检查器,如SPIN [9],FDR [10],SMV [11]可以集成到框架中用于不同的验证目的。在tMDA中,我们选择了SPIN作为模型检测引擎,因为它的成熟性和流行性。D. Du等/理论计算机科学电子笔记243(2009)69732.2tMDA中各模块的功能在tMDA中,开发人员使用用例图对系统需求建模。根据用例驱动的需求分析方法,开发人员使用序列图对每个用例的事件流程进行建模,以显示对象之间的交互。此外,类图,状态图和活动图被用来建模系统的静态结构和动态行为。关注点分离建模方法为整个系统提供了不同的视图。然而,多视图模型之间的一致性应得到保证。“模型编辑器”是基于UML2.0 Meta模型的一个子集实现的,它提供了一个用户友好的“模型编辑器”的核心框架“”模型转换“的功能如果在UML模型中检测到错误,则由SPIN生成由形式规范语言描述的反例。然而,反例路径太复杂,太长,开发人员无法理解。因此,应该对反例进行解释和分析,以便没有正式数学背景的开发人员也可以利用反例信息来定位错误。开发人员使用根据扩展后的序列图,开发人员可以定位错误,然后在“模型编辑器”中修改模型“Model Verifier”的特点此外,模拟器的算法是根据UML模型的语义逐步执行系统路径来实现的详细的仿真算法可参考文献[13]。到目前为止,tMDA的另一个显著特点是LTL公式[14]可以基于嵌入式系统中常见的属性指定模式由属性指定模板生成。系统的预期性能可用LTL公式表示但是,如何定义正确的LTL公式是一个困难的问题。提出了一种基于属性指定模式的逐步方法开发人员可以根据系统的属性约束选择合适的模板。有关“LTL公式编辑器“的详细信息,UML建模和验证技术的集成形成了一种严格的建模方法,有助于生成高质量的代码。根据模型驱动开发的思想,实现基于生成的代码框架,开发人员可以为特定功能定制生成的代码。这种方法将提高代码生成的效率和代码的质量。74D. Du等/理论计算机科学电子笔记243(2009)692.3理论背景基于何继锋等人[24]提出的rCOS理论,严谨的基于组件的开发方法为tMDA[15]提供了理论基础。在tMDA中,类图和组件图用于描述静态属性或结构属性,序列图、活动图和状态图用于描述动态属性。因此,我们描述了相关的模型,并展示了如何将它们应用到建模和验证过程中。为了给出类图的形式定义,假设CN、AN和AttrN是三个不相交的集合,分别表示类名、关联和属性。对象的每个属性都接受一种称为数据类型的纯数据类型的值。自然数N、布尔值Bool等数据类型的示例。让T表示数据类型的集合。定义2.1类图是一个元组,其中• Ass是一个部分函数,C是CN的一个子集。 屁股:C~(AN~PN ×PN×C)使得Ass(C2)(A−1)=<$M2,M1,C1<$i <$Ass(C1)(A)=<$M1,M2,C2<$i其中PN是N的幂集。若Ass(C1)(A)=,则称A为C1与C2之间的结合,M1和M2称为C1和C2在A中的基数. 关联A一般由A:(C1,M1,M2,C2)表示。我们使用AssN(C1,C2)来表示C1和C2之间的所有关联的集合。• Att是一个偏函数Att:C~(AttrN~T)。我们使用C. a:T来表示Att(C)(a)=T,并称a为C的属性,T为a的类型。 我们使用attV(C)表示集合{a:T|Att(C)(a)= T}。• InhC×C是类之间的直接推广关系。我们用C1InhC2来表示(C1,C2)∈Inh,并说C1是C2的一个直超类,C2是C1的一个直子类。• M eth是从C到一组方法的映射。我们可以使用类似Java的格式来指定类模型,如下所示。类模型CMC 11类扩展C12{T11x1;. ;T1mxm}... ......这是什么?类Cn1扩展Cn2{Tn1y1;. ;Tnkyk}关联(M1,C1,C2,M2)A1;... ;(M1,C1,C2,M2)Aj不变量Φ结束CM1 1 1 1j j j j其中C1ExtendsC2表示super(C1)=C2。M1和M2是自然数的集合我我自然数和代表的多重性的作用C1和C2的协会我我D. Du等/理论计算机科学电子笔记243(2009)6975Ai,i = 1,.,j.序列图由对象和描述对象如何通信的消息组成。当一个对象调用另一个对象的方法时,就会发生交互。定义2.2消息是一个元组:Msg=,其中• N s是类N的对象s,称为消息的源,可以用函数source(Msg)表示。• M t表示消息的目标对象t,其类型M可以用target(Msg)表示。• Action,用action(Msg)表示,是一个形式为g −→ act的保护方法调用,其中g是源(Msg)的非关联属性的布尔表达式,而act是一个没有方法调用的命令(内部动作)或方法名m。• Ord是表示消息在序列图中的顺序的自然数,用order(Msg)表示。一个受保护的命令g−→act被定义为gact。我们要求,如果action(Msg)是 一 个 没 有 方 法 调 用 的 受 保 护 命 令 , 那 么 source ( Msg ) =target(Msg),即对象之间的交互只能通过方法调用来执行。定义2.3序列图是一个元组SD=• Actor是调用消息Start的发起(actor)对象;• Start是这样的开始,即source(Start)= Actor a。• 一组消息MSG包含开始、命令(Start)<、用于MSG中任何其他消息的命令(Msg ),以及如果命令(Msg1)= 命令(Msg2),则仅当源(Msg1)=源(Msg2)。MS(Msg)表示消息Sm ={Msg1,. Msgk},其中消息Msg2在顺序图Msg1中如果order(Msg1)j:= 1;<当j≤k2do{if{(gij−→ Action(M sgij))|1 ≤ j ≤ k2} f};}= 0;i:=i+1};其中k1是消息的数量,N是目标对象的类别,k2是在mi和mi+1之间处理的消息的数量。消息ij是从源对象到目标对象的所有消息。gij是执行消息Msgij的保护。定义2.4给出设计类图DC和序列图SD族的规范。 DC和SD一致,如果• 对于SD中的每个消息Msg=,目标对象Mt被声明为源对象N s的类N的属性。• 如果action(Msg)是g−→m,并且m是方法名,那么m是target(Msg)类中的一个已定义方法。• 从DC获得的相应的类声明部分cdeclsd定义良好。在基于组件的设计中,组件是必不可少的模块。一个组件有一组接口或端口,用于与其他组件通信。 实际上,每个组件都通过端口来实现一些业务功能,这些功能通过方法调用来实现。定义2.5端口p是一个元组(M,t,c),其中M是p中方法的有限集合,t是可以提供或需要的端口类型,c是可以是同步或异步的通信类型。我们使用p.M表示端口p的操作集,p.t表示端口类型,p. c表示通信类型,其中p.t={providedport,requiredport},p.c={同步,异步}定义2.6组件Com是元组(Pp,Pr,G,W),其中Pp是提供的端口的有限集合P是所需端口的有限集合G是有限子分量集W<$TP×C∈G(C.Pp<$C.Pr)是非-其中TP=P p<$Pr<$C∈GC.Pr,C.Pp和C.Pr表示所提供的,子组件的所需端口集。如果G= Φ<$W = Φ,则分量Com=(Pp,Pr,G,W)D. Du等/理论计算机科学电子笔记243(2009)6977,否则Com是一个复合。合约是端口的规范,用于描述组件的行为语义,该组件在tMDA中使用OCL表达式建模定义2.7合同Ctr是一个四元组(P,Init,Spec,Prot),其中• P是一个端口。• Spec将P的每个操作m映射到其规范(am,gm,pm),其中(i)m包含端口P的资源名称以及m的输入和输出参数。(ii) g m是操作m的触发条件,指定可以激活m的环境。(iii) p m是反应设计,描述m的行为。• Init标识初始状态。• Prot是一组操作或服务调用事件?m1(x1)... ?mj(xj)>即组件的行为协议。在这里,引入协议来协调组件与环境之间的交互。在tMDA中,协议Prot采用UML序列图进行建模虽然有一些工作的协议验证模型检查序列图,我们实现的协议验证之间的一致性验证状态图和序列图。也就是说,每当参与者遵循序列图所描述的交互协议,并且状态图可以接受跟踪集时。状态图描述了对象生命周期中的状态转换过程。状态图的语义模型由标签转换系统(LTS)表示根据LTS,状态图的形式化如下:定义2.8状态图是四元组SM=,其中S表示状态集;s0表示初始状态;L标记每个状态L的一组原子命题:S−→2AP,由e→action描述,e是触发事件,action是生成的动作; Δ表示转换关系,其中 Δ<$S×(L<$ε)×S定 义 2.9staechartSM = 的 迹 是 一 个 有 序 的 转 移 集 tr={\displaystyle\tagi,(0 ≤i≤k)}|(si,li,si+1)}。我们使用Ev(tr)来表示状态图的轨迹中的事件集合,其中Ev(tr)={ev(10),ev(11),ev(12),. ev(lk-1)}和sord(ev(l0))都应该在SD中定义。• 在序列图中发送或接收消息的序列对应于由状态图描述的交互行为的轨迹。也就是说,如果Tr是一组事件,则Tr ={ev0,ev1,ev2,.,evk},或i,(k≥i0)|(evi)∈Tr,则78D. Du等/理论计算机科学电子笔记243(2009)69Sm可以映射到Tr。3案例研究:银行ATM系统在本节中,我们将演示tMDA如何促进系统需求的建模和主要目的是说明将形式化验证技术集成到模型驱动开发过程中以提高系统模型质量的可行性。开发过程是用例驱动和基于组件的,包括以下步骤。首先,我们用用例图对系统需求进行其次,给出了系统服务的组件图然后,根据构件图,构造了类图、顺序图、状态图来描述构件的静态结构和动态行为。在建模过程中,采用形式化模型检测技术验证了不同UML模型的正确性和一致性整个建模和验证过程在我们自己开发的集成环境tMDA中进行3.1用例驱动的需求分析与设计我们将通过一个简单的BAS案例研究来说明我们的方法,该案例研究描述了自动柜员机(ATM),一台银行电脑和一个用户一个用户可以在某个ATM上存钱、取钱和转账,这由用例图来描述如图3所示。这些用例可以看作是某些组件的契约。例如,用例描述的这些服务可以由Transition组件提供(如图4(左)所在组件图中,我们只需显示所提供的服务withdrawMoney ofTransition组件,该组件与ATM和Bank通过端口连接。与通常的方法不同,需求组件图是从用例图中派生出来的。 也就是说,在需求分析过程中,我们从分析客户需要的服务开始,然后将服务分配给端口,端口再将服务委托给组件。然后,基于tMDA设计和实现组件。组成组件的协作类 动态行为由ATM和Bank类的状态图指定(如图5,6所示)。此外,交互协议的某个场景由序列图建模(如图7所示)。3.2需求一致性验证3.2.1类图与序列图静态结构和动态行为的一致性是非常重要的,然而这种一致性往往被开发人员所忽视出现在序列图中的消息tMDA的模型验证器可以通过语法检查来验证这种一致性D. Du等/理论计算机科学电子笔记243(2009)6979图三. BAS用例图见图4。 BAS组件图(左)和BAS类图(右)图五. ATM状态图例如,图7所示的序列图中的消息verifyPIN。我们可以得到Msg=(AT M,Action,M t,Ord),其中Action(M sg)=verifyPIN,80D. Du等/理论计算机科学电子笔记243(2009)69见图6。 Statechart for银行target(Msg)=Bank.根据定义2.4,如果类图与序列图一致,则事件verifyPIN应在Bank类中声明。否则,将生成不一致警告消息。3.2.2状态图与顺序图模型验证器的主要功能非正式地说,一致性必须确保无论何时参与者遵循序列图描述的交互协议,状态图都可以接受跟踪集。但是,如何用SPIN验证状态图和序列图的一致性呢?LTL公式适合于描述事件发生的线性时间序列,因此,我们可以用LTL公式来表示序列图中事件触发的状态转移轨迹。验证状态图与时序图的一致性实质上就是验证状态图是否满足描述时序图交互轨迹的LTL公式,因此时序图到LTL公式的转换算法是关键,它利用时序图的特点自动生成LTL公式。在BAS案例研究中,状态图之间的交互应符合序列图指定的协议(如图7所示)。注意,我们通过将状态信息添加到消息传递中来扩展UML序列图,消息传递记录了对象进入的下一个状态。例如,在对象ATM将事件verifyPIN发送到对象Bank之后,对象自动柜员机将进入自动柜员机状态。扩展序列图(如图7所示)指定了行为协议,其中如果某个客户想要取款,他必须输入正确的PIN码。如果PIN码错误,他可以重新输入PIN码。为了简单起见,我们只讨论协议的正确行为。D. Du等/理论计算机科学电子笔记243(2009)6981见图7。 BAS的扩展序列图根 据 定 义 2.3 , 我 们 可 以 得 到 这 个 场 景 的 事 件 序 列 Sm={enterCard ,verifyPIN,reenterPIN,verifyPIN,PINverified}。的相互作用行为的的statechart为ATM和银行可以被描述通过的 微量tr={(CardEntry,enterCard,PINEntry),(PINEntry,verifyPIN,Verifying),(Verifying,reenterPIN,PINEntry),(PINEntry,verifyPIN,Verifying),(验证,PINverif ied,AmountEntry). }中。因此,Ev(tr)={enterCard,verifyPIN,reenterPIN,verifyPIN,PINV erified}。根据定义2.7,如果Sm≠Ev(tr),则tMDA可以为SPIN支持的序列图自动生成LTL公式。LTL公式如下:#define p0 CardEntry#define p1 CardEntry#define p2 PINEntry#define p3 AmountEntry<>(p0&&<>p1)&&<>(p1&&<> p2)||<>(p2&&<>p 3)(LTLformula)注意,p0、p1、p2、p3表示交互行为的状态信息。因此,LTL公式跟踪系统状态转移过程的记录。一旦生成LTL公式,就可以实现状态图和序列图之间的一致性验证。如果我们从ATM的状态图中删除转移PINVerified(图5)并执行一致性验证,结果显示状态图中存在无效的结束状态。实验表明,状态图之间的交互3.3Statechart活性性质的验证验证UML状态图的最常用方法是将状态图转换成模型检查器的输入语言。已经开发了一些工具来分析UML中指定的系统模型,例如vUML [17],Hugo[18]。Lilius和Paltor的工作讨论了82D. Du等/理论计算机科学电子笔记243(2009)69见图8。 Modified state chart of Bank见图9。 反例的扩展序列图作为其验证工具vUML的一部分,用于转换为PROMELA的UML状态机。vUML的主要特点是(1)vUML执行的验证仅限于死锁检查和一些健壮性检查。(2)只考虑UML状态图的一个子集。与他们的工作不同,我们关注的是状态图的性质验证,如活性或安全性。本小节说明了如何在BAS案例研究中验证状态图的活性属性。满足活性性质的系统规范意味着好事最终会发生。 SPIN通过探索系统的执行过程中是否存在循环路径来验证活性属性。例如,我们验证ATM模型是否满足活性性质。 修改后的状态图如下所示 如图8所示,表示如果PIN码错误,客户将继续重新输入PIN码。这发现错误,D. Du等/理论计算机科学电子笔记243(2009)6983见图10。 状态图的模拟当我们执行状态图的活性验证时生成反例。根据反例,扩展序列图如图9所示存在用户继续重新输入PIN码的循环路径为了定位错误,开发人员还可以模拟系统的执行路径,如图10所示。左边的虚线矩形是我们模拟状态图时的消息交互过程在执行每个步骤期间,将在左侧虚线矩形中生成相应的事件和状态信息。右边部分是状态图的模拟过程,其中蓝色状态表示活动状态,红色转换表示下一个触发的转换,绿色转换表示执行的转换。 状态图的模拟有助于分析系统的详细执行路径,从而可以很容易地定位错误。3.4LTL公式由于LTL具有复杂的语法和语义,开发人员很难定义和理解形式化的LTL公式。本小节讨论如何帮助开发人员定义LTL公式。在tMDA中,LTL公式的属性定义模板可以基于Dwyer [19]提出的属性指定模式(PSP)生成。Dwyer图11(左)中所示的称为定性模式的事件模式和顺序模式发生模式涉及程序执行期间单个状态/事件的发生另一方面,顺序模式关注的是在程序执行期间状态/事件多次出现的相对顺序,例如状态/事件之间的优先级或响应此外,S.Konrad [21]提出了实时规范模式(RSP),该模式关注嵌入式系统中与时间相关的RSP有三种类型模式:持续型、周期型和实型。84D. Du等/理论计算机科学电子笔记243(2009)69时间顺序RSP的表达与Dwyer的模式系统相似。PSP和RSP代表了两类属性模式:定性和实时,它们组成了规范模式系统。已经发现这些特定模式足以指定最常见的属性[22]。在tMDA中,开发人员可以根据系统约束选择合适的属性定义模板。逐步生成过程可参考[13]。例如,响应模式的定义模板如图11(右)所示。图十一岁SPS的类别(左)和LTL公式的属性定义模板(右)生成的LTL公式如下:[](verifyPIN→<>(VerifyingCardVerifyingPIN)),这意味着由于事件verifyPIN的发生,系统进入VerifyingCard状态和VerifyingPIN状态。然后,tMDA 可以验证状态图是否满足LTL公式指定的约束。验证结果如图11(右)的右部分所示。3.5合同OCL表达式验证OCL的核心是一种表达式语言。 可使用表达式在各种上下文中,例如,定义约束,如类不变式和方法的前/后条件利用UML的约束表示机制,将OCL表达式作为对转换事件的一种约束,对UML模型中的方法契约进行建模这种建模方法可以表达某种方法的前/后条件。在本小节中,我们将演示如何使用SPIN验证OCL表达式。在状态图的上下文中,我们用触发事件的OCL前/后条件对方法契约进行建模。在tMDA中,每一个OCL约束表达式都代表了方法被激活时应该满足的条件,可以看作是PROMELA程序的断言。 因此,我们的方法的关键点是将OCL表达式转换为断言。由于SPIN的断言验证,可以验证OCL表达式。在案例研究中,我们在图12所示的状态图中定义了OCL表达式。过渡(PINVerified){pre:cardvalid= 1pinV alid = 1}D. Du等/理论计算机科学电子笔记243(2009)6985见图12。 在状态图满足前提条件从OCL表达式{pre:cardvalid=1pinV alid= 1}生成的断言是4结论和相关工作Hnatkowska等人讨论了UML系统模型组件之间的一致性问题[23]。他们提出了OCL来形式化模型组件之间必须保持的一致性条件,其中类的状态图与一个类的类图和一个类与其他类的状态图然而,他们的工作重点放在OCL约束所描述的格式良好的规则上,这只是验证了模型的语法正确性。联合国大学软件所的一个研究小组在将正式规范技术应用于模型驱动的基于组件的软件开发过程方面取得了重大进展[24][25]。在CoCoME项目中,他们使用模型检查器FDR来证明序列和状态图的跟踪等价性X. Yu,et al [28].他们将rCOS规范转换为PROMELA代码,然后调用SPIN引擎来验证生成的PROMELA代码。我们的工作涉及整个基于MDA的软件开发过程,包括需求建模、验证、模拟和代码生成。更重要的是,一个严格的建模和开发方法的实施。我们介绍了我们最近在基于MDA的软件开发过程中应用形式验证技术的经验。通过BAS实例分析,说明了集成建模与验证环境tMDA在系统需求建模和多视图UML模型一致性验证方面的有效性86D. Du等/理论计算机科学电子笔记243(2009)69我们工作的主要贡献包括:(i) 实现了一个集成的建模与验证环境,将DbC的思想应用于系统需求建模,保证了需求模型的正确性。用例图用于对组件的契约进行建模。基于该契约,系统所需的服务被派生并分配给组件的端口。另一方面,方法契约用状态图中的OCL表达式来建模,它表示了某种方法的前/后条件。(ii) 提出了一种多维验证模型,该模型包含几个验证功能:• 验证静态模型和动态模型之间的一致性,例如类图和序列图之间的一致性。• 验证statecharts的活性或安全属性。• 验证动态模型之间的一致性,如状态图和序列图,可以验证状态图之间的交互是否符合序列图所建模的协议。• OCL表达式的验证是通过将OCL表达式转换为PROMELA的断言来完成的。我们未来的工作包括扩展tMDA以支持基于SOA的软件开发,特别是实现可信服务组件的建模和开发我们亦将探索基于模式的细化规则,以促进模型过渡。这有助于完成从PIM模型到PSM模型的转换确认我们感谢审稿人的仔细阅读和详细评论,帮助我们改进了论文。本文的工作得到了国家重点研究项目“依赖性软件理论”(90718014)、国家高技术863计划(2006AA01Z165)、国家自然科学基金(60673114)和国家自然科学基金(2006)的部分资助。60603037。引用[1] X. Li,Z.刘和,何俊,UML需求一致性检验,第九届IEEE国际复杂计算机系统工程会议论文集,ICECCS2005,第411-420页,IEEE计算机协会出版社,2005年。[2] Z.刘俊,何俊,刘俊,统一UML的观点,理论计算机科学电子笔记,101,第95-127页,Elsevier,2004年。[3] B. 面向对象的软件结构,北京:计算机科学出版社,1997。[4] B. Meyer,Ei Zelel:The Language,Prentice Hall,1992.[5] R. R. Lutz,《软件需求分析中的目标安全相关错误》,系统与软件杂志,第222-230页,1993年。D. Du等/理论计算机科学电子笔记243(2009)6987[6] C. A. R. Hoare和J.《Unifying Theories of Programming》,Prentice-Hall,1998年。[7] P. Kruchten,The Rational Unified Process-An Introduction,Addison-Wesly,2000。[8] E. M.克拉克湖,澳-地Grumberg和S. Jha,Counterexample-Guided Abstraction Refinement,LectureNotes in Computer Science 1855,Springer-Verlag,2006。[9] G. J. Holzmann,The Model MSPIN,IEEE Transaction on Software Engineering,第279-295页,1997年。[10] A. W. Roscoe,模型检查CSP,在A.W.罗斯科(Roscoe),《古典思想:纪念C.A.R. Hoare,Prentice Hall,第353-378页,1994年。[11]K. L. McMillan,Symbolic Model Checking:an Approach to the State Explosion Problem,ReportCMC-CS-92-131,1992。[12] D. Du,H. Cao和K. He,MCF4U:A Flexible Model Checking Framework for UML Models,DCDISSeries B,Vol.14(S6),Special issue on software engineering and complex networks,pages 281-286,2007.[13] D.杜,UML模型检测框架及关键技术研究,博士。论文,武汉大学,武汉,2007。[14] Z. Manna 和 A. Pnueli , The Temporal Logic of Reactive and Concurrent Systems : Specification ,Springer-Verlag,1992。[15] Z.叮,Z。Chen和J. Liu,服务组件架构的严格模型,理论计算机科学电子笔记207,第33-48页,Elsevier,2008年。[16] J. 刘,J.何,MDA中模型构造与集成的策略,软件学报,第17卷,第6期,第1411-1422页,2006年。[17] 李文生,《软件工程学》,北京:中国软件工程出版社,1999年。[18] T. Schafer,A. Knapp和S. Merz,Model Checking UML State Machines and Collaborations,ElectronicNotes in Theoretical Computer Science 55(3),Elsevier,2001。[19] M. B. Dwyer , G. S Avrunin 和 C. Corbett , Patterns in Property Specifications for Battle-StateVerification,Proceedings of the 21st International Conference on Software Engineering,ICSE 1999,pages 411-420,IEEE Computer Society Press,1999。[20] E. M. Clarke 和 E. A. Emerson , Design and Synthesis of Syschronization Semetons Using BranchingTime Temporal Logic , Logic of Programs , Workshop , Yorktown Heights , NY , Lecture Notes inComputer Science 131,Springer-Verlag,1981.[21] S. Konrad和B. H. C.程,实时规范模式,第27届国际软件工程会议论文集,ICSE 2005,ACM出版社,2005年。[22] M. B. Dwyer 和 G. S 阿 夫 鲁 宁 角 Corbett , Patterns in Property Specifications for Battle-StateVerification, Proceeding of the 21st International Conference on Software Engineering , ICSE 1999,pages 411-420,IEEE Computer Society Press,1999。[23] B.李文,统一建模语言的一致性检验,第四届信息系统建模国际会议论文集,2001。[24] Z. Liu 和 J. He , Towards a Rigorous Approach to UML-Based Development , Electronic Notes inTheoretical Computer Science 130,第57-77页,Elsevier,2005年。[25] J. 他 , X. Liu 和 Z. Liu , rCOS : A Refinement Calculus of Object Systems , Electronic Notes inTheoretical Computer Science 365,pages
下载后可阅读完整内容,剩余1页未读,立即下载
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)