理论计算机科学电子笔记127（2005）3-16www.elsevier.com/locate/entcs基于形式化方法的UML自动验证工具MaEncarnaci'onBeato1，2EscuelaUniversitariadeInforma'ticaUniversidad Ponti fiscia deSalamanca萨拉曼卡，西班牙我是卡洛斯·E. 奎斯塔4号Pablo de la Fuente5FacultaddeInforma'ticaUniversidad de Valladolid巴利亚多利德，西班牙摘要UML规范语言的使用由于其某些特性而非常广泛然而，当今越来越复杂的系统需要建模方法，允许在开发的初始阶段检测错误形式化方法的使用使得这种错误检测成为可能，但学习成本很高。本文提出了一种工具，它避免了这种学习成本，使一个系统的活动行为表示在UML中被验证，在一个完全自动的方式，通过形式化的方法技术。它包含了一个验证助手，作为编写属性的用户指南，这样她/他就不需要了解时间逻辑或所获得的规范的形式关键词：形式化方法，自动验证，UML主动行为，形式化UML验证。1份由JuntadeCastillayLe'on（西班牙）在研究项目VA117/03中提交的研究报告2电子邮件地址：ebeato@upsa.es3电子邮件地址：mbarrio@infor.uva.es4电子邮件地址：cecuesta@infor.uva.es5电子邮件地址：pfuente@infor.uva.es1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2004.10.0244法医Beato等人/理论计算机科学电子笔记127（2005）31介绍统一建模语言（UML）[1，12]作为一种可视化建模技术具有毋庸置疑除了UML本身的特性之外，还必须添加市场上存在的许多工具来帮助它的使用（Rational Rose，Argo UML，Rhapsody.）。然而，不幸的是，它们都不能保证规范的正确性。然而，人们普遍认为，在开发的早期阶段进行错误检测可以大大降低成本和开发时间，因为检测到的错误不会被传输到后期阶段或在后期阶段被放大。因此，如果有一种工具能够将这种半正式的开发方法与正式的方法相结合，以实现系统验证，那将是非常有用的。本文提出了一种工具-TABU（UML的主动行为工具）-进行这种整合，提供了一个正式的框架，在其中验证UML的主动行为。该工具使用SMV [10]（符号模型验证器），就像正式规范一样，因为它具有足够的特征来表示UML中规范的活动行为。其主要原因是它基于标记转换系统，并且允许用户自己定义数据类型使用，从而方便变量的定义。它还使用符号模型检查进行验证，这意味着测试是自动的，总是获得答案，更重要的是，如果属性不满足，则生成识别原始错误的方法该工具在用户不干预的情况下XMI [11]（XML元数据交换）被用作输入格式，因此使其独立于用于系统规范的工具另一方面，该工具有一个多功能的助手，可以指导用户使用时态逻辑来编写要验证的属性。验证的方式是用户不需要了解以下两种情况：这是一个非常困难的问题，因为它可以使语言或时序逻辑能够利用其潜力;这是传统上在决定使用形式方法时难以克服的问题。此外，所获得的规范的形式的概念是不必要的：也就是说，验证不需要所获得的变量或模块的内部结构的知识。 图1是工具架构的图形表示法医Beato等人/理论计算机科学电子笔记127（2005）35奥布泰纳平阿尔马解 码器PinAl卡 赫 罗 恩 托 尔 诺<> introPin（ ）<？ XML version ='1.0'encoding ='ISO-8859-1'？ ><！DOCTYPE XMI SYSTEM 'file：/D：/documentos/Valladolid/UML-XMI/pruebas/ejemplosConRational/UMLX13.dtd'>Unisys.JCR.2/XMI.exporter><模 型 _管 理 .模 型xmi.id='G.0'>e.ModelElement.name>/Foundation.Core.ModelElement.name>cajero}{3FBF234E0028}.（ 角色 1）[关 联结束] =--><> pulsarAceptar（ ）1.3.4/XMI.exporterVersion><<发送 >><<发<！ -- == ejemplo1Modificado1[模 型 ]<< 信 号 >><< 信 号 >><<信==校 正 针塔 耶 塔introPin内塔 列塔脉 冲ejemplo1Modificado1/Foundation.CorPin或=<基 础 .核 心 .空 间 .所 有 元 素 ><！ -- ==<基 金会 .核 心.协 会xmi.id ='G.14'>类进 入 /保 留图博通<！ -- ==萨 尔 多<基 金会 .核 心.协 会结 束xmi.id='G.15'>/actualizarSaldoCajeroState diagram[校正 后的Ps>=2]活动图静止图.xmi不 活 动 的内 塔列 塔输 入 /cajero.contError=0]introPin[R=3 埃 斯 佩 拉平rront工程师UML工具（理性，阿尔戈，......）奥斯 托全 球[]（ ！P）R之 前阿利 滕西 亚全 球>（ P ）R之 前！ R W（ P！ 右 ）在 Q和 R 之 间[](Q ！ R ->Universalidad全 球[]（ P ）R之 前<>R -> （ P U R ）Q之 后[](Q-> []（ P） ）在 Q和 R 之 间[]((Q ！R>R ） -> （ P U R） ） 在 Q之 后直 到 R[](Q！ R -> （ PW R） ）/**************************************************//**主 模 块 *//**************************************************//**************************************************//*/introTarjeta： boolean;inputPin： boolean;pinCorrecto：boolean;errorPin：boolean;expulsarTarjeta：boolean;actualizarSaldoCajero：/**************************************************//* 属 性*/publicvoid run （ ） {/* 信 号 声 明*/prop1_6： assert G（ 目标 实例.en_operativa introPin~retenida -> X（ TarjetaInstancia.en_identificarTarjeta） ）;prop2_6： assert G（ pinCorrecto -> Fprop3_6：assert G（TarjetaInstancia.en_comprobarPinbotonOperacion： boolean;pulsarCancelar： boolean;/**类 实 例 */G（ TarjetaInstancia.en_obtenerPinAlmacenado->TarjetaInstancia.en_obtenerPinIntroducido） ; G（ TarjetaInstancia.en_identificarTarjeta ->F（TarjetaInstancia.en_obtenerPinAlmacenado&TarjetaInstancia.en_obtenerPinIntroducido） ）;prop6_6：assertFprop5_6：断 言X F->（ ~TarjetaInstancia.en_compararPines/*类 的 实 例 ： Tarjeta*/TarjetaInstancia ： Tarjeta（ finTratamientoError，/**************************************************/X（~TarjetaInstancia.en_compararPines（ TarjetaInstancia.en_identificarTarjeta） ） ;X（ cajeroInstancia.en_comprobar） ）;TarjetaInstancia.en_obtcajeroInstancia.en_esperaPin）;X FTarjetaInstancia.en_obtenerPinIntroducido） ） ;prop6_6： 断 言F（ TarjetaInstancia.en_compararPines） ->cajeroInstancia.est_comprobarErrores = DontKnow） ;（ ~TarjetaInstancia.en_compararPinesUX（ ~TarjetaInstancia.en_compararPines U~TarjetaInstancia.en_compararPines&tarjetaInstancia.en_decodificarPinAlmacenado） ;.smv时态逻辑属性TABU（UML主动行为011111111校 正针011111111errorPin不 活动的主 动的不 活动的主 动的不 活动 的主 动的不 活动的主 动的不 活动 的埃 斯特 卡赫 罗不 活动的不 活动的不 活动的不 活动的主 动的主 动的主 动的主 动的主 动的estTarjeta主 动的主 动的主 动的主 动的主 动的不 活动的不 活动 的不 活动的不 活动的埃 斯特 卡赫 罗011111111errorPin第 九章 ： |867|： 5341Cadence SMV型号（自动验证）自动手动辅助从XMI到SMV编写属性的助手要检查的属性Paraponer a prueba la utilidadde la transformación realizada，as ícomosuvalidez， espruarioverificarlaspecificación de unsistema querecoja todas lascharacterísticas de UML， y queconcluir que la transformaciónen SMV， del comportamientoactivo deunaspecificaciónrealizadaen UML， escorrecta.最后，这一融合体现了进步的形式，它代表了一个深刻而独特的使命体系，它包含了转型中的一个方面。Pudiéndose llegara laconclusiónque el comportamiento activoreflejado en la specificaciónenUMLse corresponde con elreflejadoen SMV.Pararealizar estacomprobación seelegirán propiedades temporalesadecuadas que propionale asegurarla corrección de laspecificación.La specificaciónen SMV obtenidapara cadaunode los sistemas puedeencontrarseen elapéndice~\ref{smvEjemplos}.由 于 punto departida se utilizaun sistema conocidoquereflejael comportamiento de un cajeroautomático. 这一系统是一个独特的系统，它的细节是一个小细节，它的特点是最完整的，它的结论是系统的细节。 El objetivo que sepersigue， es que la mayoría delos comportamientosque puedenreflejarse en una specificaciónen UML， se encuentren también enalguno deloscasosde ejemplo.为了你 ，我 用自动驾驶系统，介绍了一个允许正确使用历史数据的自动驾驶系统。所 有 这些的 核查都没 有特别的 限制，因 为它不影 响SMV实 现 转 换 的 验 证 。 现在 我们还没有认识到，这个问题的主要目标是将形式化的工具（ SMV） 与一种半 正 式 的工具 （UML）相结合，这种工具是使用和重新认识的。 在 软件开发的初始阶段，允许实现系统的形式化，在软件开发的初始阶段，允许检测错误，在实现系统的具体化和程序的具体化的过程中，允许实现系统的形式化。（自然语言）好反例迹Fig. 1. 工具架构该工具利用UML和所研究系统的知识，自动地从XMI的文本表示中获得SMV的形式化表示。平行，一个向导帮助编写使用LTL（线性时序逻辑）验证的属性，此外，如果属性不满足，该工具会显示一个反例跟踪。本文的其余部分通过案例研究展示了该工具的功能。它是根据两个主要方面进行分析，工具：如何从UML图中获得正式规范，以及助手如何帮助和指导验证属性。这之后是回顾了文献中相同领域的工作，最后提出了结论以及未来可能的工作。6法医Beato等人/理论计算机科学电子笔记127（2005）32从UML到SMV工具输入是一个UML规范，它已经使用XMI交换语法进行了格式化。根据此输入，自动生成SMV规格。在将UML的活动行为转换为SMV时，考虑了三种图：类图、状态图和活动图。第一个提供了关于组成系统的元素及其关系的信息，而第二个和第三个提供了关于这些元素中的每个元素随时间的行为的为了说明该工具是如何工作的，我们使用了自动柜员机的例子（图2、3、4、5和6），这既是因为它是一个非常著名的例子，也是因为它在其规范中包含了大多数现有的语句机和活动图的构建块。以下是该系统的基本描述。首先，用户输入信用卡，然后输入密码。系统会检查它是否正确，如果不正确，则允许用户重试。如果用户输入了连续三个错误的PIN码，则卡将不会返回给用户。一旦引入右销，将允许用户按下操作按钮。此操作更新卡信息，包括可用剩余卡。在任何时候，用户可以按下取消按钮，这将使卡被返回，并产生一个错误信号3类图作为我们出发点的基本概念是活动阶级的概念。该系统根据与信号接收相关的活动类别进行指定。每个活动类的行为反映在不同的SMV模块中，SMV模块又由每个类对象在主模块中实例化。每个SMV模块，代表一个类，需要类接收的信号作为其输入参数，类发出的信号作为输出参数。因此，所述信号在类图中使用原型send>>和signal>>表示，如图2所示。这里，信号okPin、errorPin和updateBalanceCard 对 应 于 Card 类 发 出 的 信 号 ， 而 introPin 、 introCard 和returnCard是它接收的信号。还必须包括一个称为环境的附加类。它没有相关的行为，并包含外部产生的信号的细节。系统和哪些是输入信号。法医Beato等人/理论计算机科学电子笔记127（2005）37<<发送>><<发送>>发送>><<发送>><<发送>><<发送>><<发送>><<发送>><<发送>><<发送>><<发送>><<发送>>发送<<>><<信号>>pushOperation<<信号>>pushCancel<<信号>>introCard<>introPin环境的<<信号>>保留<<信号>>errorPin<<信号>>errorEnd<>updateBalanceCard<> introPin（）<> introCard（）<> returnCard（）<> returned（）<> pushOperation（）<> error（）<> ok（）checkPin<> introPin（）<> introCard（）<> OkPin（）<> errorPin（）<>PushOperation（）<>pushCancel（）<>updateBalanceCard（）checkErrors（）OkPinCounter：0.. 6 = 0错误计数器：0.. 3 = 0卡ATM<<信号>>OkPin<<信号>>返回卡<<信号>>错误<<信号>>Ok<<信号>>updateBalanceATM图二. ATM系统4状态机每个活动对象的行为通过状态机和活动图反映。为了正确地控制状态机的演化，必须知道它在任何给定时刻所处的状态。这是通过使用单独的变量来存储每台机器的此信息来此外，组合状态（顺序和并发）可能出现在机器中的事实意味着需要额外的变量来处理子机器。除了它们在激活和去激活方面所具有的特殊性之外，这些将按照与主机相同的推理至于进化机，接下来使用SMV算子。这表示变量在下一步中采用的值。使用init操作符启动状态机。就ATM类的机器而言（见图3），最外层机器行为的SMV表示如下所示：6/* Statemachine for state：ATM*/st_ATM：{checkBalance，waitOperation，active，inactive，returningCard};/** 类的语句机演化：ATM*/ init（st_ATM）：=inactive;next（st_ATM）：= case {6每个转换都被分配了一个唯一的标识符，该标识符对应于自动分配的XMI8法医Beato等人/理论计算机科学电子笔记127（2005）3活性非活动introCardentry / ATM.errorCounter=0（tr_G_4）introPinwaitPincheckingPinerrorPin保留(tr（G_29）updateErrordo/check错误奥克(tr_G_16）(trG_7）返回卡退出/返回卡wait操作pushOperation(tr_G_12）（tr_G_9）/okpushCancel/error(tr_G_13）(tr_G_46）CheckBalanceATM(tr_G_44）更新ATM支票自动柜员机/updateBalanceATMcheckBalanceCardupdateBalanceCard(tr_G_38）checkCardcheckBalance图三. ATM类tr_G_9：checkBalance;tr_G_7：waitOperation;tr_G_4： active;tr_G_29： inactive;tr_G_16： inactive;tr_G_12：returningCard;tr_G_13：returningCard;默认值：st_ATM;};其中，tr_G_9、tr_G_7、tr_G_4. 表示触发转换tr_G_9、tr_G_7、tr_G_4. 块默认值表示没有状态变化的行为，也就是说，当机器中没有转换被触发并且在下一个步骤中保持相同的状态时类似的推理已被用于子机的行为，基于每个顺序复合状态和并发复合状态的每个区域具有不同的机器。通过这样做，与图3的并发复合状态checkBalance相关联的行为用以下机器来表示：/* Statemachinefor state： checkBalanceATM*/st_checkBalanceATM：{updateATM，checkATM，FINAL，DontKnow};/* Statemachine forstate： checkBalanceCard */st_checkBalanceCard：{checkCard，FINAL，DontKnow};/** Evolution语句机器状态：checkBalanceATM */ init（st_checkBalanceATM）：= DontKnow; next（st_checkBalanceATM）：= case {tr_G_12：不知道;tr_G_13：不知道;法医Beato等人/理论计算机科学电子笔记127（2005）39tr_G_9： checkATM;tr_G_44： updateATM;tr_G_46： FINAL;默认值：st_checkBalanceATM;};/** Evolution语句机器状态：checkBalanceCard */ init（st_checkBalanceCard）：= DontKnow; next（st_checkBalanceCard）：= case {tr_G_12 ： 不 知 道 ;tr_G_13：不知道 ;tr_G_9 ： 检 查卡; tr_G_38：最终;默认值：st_checkBalanceCard;};其中DontKnow是已停用的机器的状态。由于触发了转换tr_G_13，按下取消按钮，或者由于两个子机都达到最终状态，tr_G_12因终止而触发，因此可能发生停用。其语法如下：tr_G_12：=in_checkBalance&in_FINALcheckBalanceATM&in_FINALcheckBalanceCard;5行动活动对象的演化可以导致不同的动作，包括发送信号和修改类属性的值关于发送信号，它可以发生在以下任何情况下：（1）触发转换，如果信号是在转换事件中;（2）激活状态，如果信号是在其进入动作中;（3）停用状态，如果信号是在其退出动作中。考虑到状态激活和去激活都是由于某些转换的触发、信号演变可以以与状态机演变类似的方式表示。至于修改属性的值，它将通过使用SMV操作符init和next指定。如果属性在类图中有一个初始值，它们将被初始化，而它们的演化（下一步）将取决于转换的触发例如，ATM类中errorCounter属性的SMV行为如下所示（参见图2、图3和图4），该SMV行为记录了引入了多少个错误的连续pin号/***** 属性：errorCounter ****/ATM_errorCounter：0..3;init（ATM_errorCounter）：=0; next（ATM_errorCounter）：= case {tr_G_55：ATM_errorCounter +1;tr_G_29：0;tr_G_16：0;10法医Beato等人/理论计算机科学电子笔记127（2005）3非活动保留/卡.okPinCounter = 0introCard误差执行部分好更新帐户保留/card.okPinCounter = 0introPin [~retained]/updateBalanceCardendError误差检查余额checkingPindo/checkPinwait操作pushOperation检查[ATM.errorCounter >= 2] /保留保持[ATM.errorCounter 2]/ATM.errorCounter = ATM.errorCounter +1，errorEnd(tr_G_55）见图4。 活动checkErrors图五. Card类的状态图。默认值：ATM_errorCounter;};6活动图类操作控制流程可以使用活动图来建模，活动图基本上显示活动之间的控制流程它的SMV规范可以在反映类行为的模块中找到。这些活动图在使用doactivity>表示法的状态中产生对活动的调用时被激活。活动图可以被认为是状态图其中大多数状态是活动状态，大多数转换是通过终止来触发的。因此，用于表示它们的机制类似于用于状态机的机制。唯一的区别是，对于并发进化，使用了特殊的分裂和联合状态（fork和join）。只要激活了其中调用此Activity的任何状态，它们就会被激活。同样，每当产生转换时，法医Beato等人/理论计算机科学电子笔记127（2005）311identifyCardgetStoredPingetIntroducedPindecodeStoredPincomparePins[card.okPinCounter >= 2] /errorPin错误检查[card.okPinCounter 2]/card.okPinCounter = card.okPinCounter +1，okPin确认见图6。 checkPin活动的活动图。使其所在的状态失效7验证用具有坚实数学基础的形式语言获得系统规范意味着可以检查系统是否符合某些期望的与形式规范方法一样，软件系统的复杂性不断增加，需要开发新的验证方法和工具来自动或半自动地执行。在我们的工具中，使用SMV工具模型检查器进行验证。有了这个，就有可能使验证过程完全自动化。也就是说，给定一个属性，总是得到肯定或否定的回答该属性必须以SMV7中的时态逻辑、CTL（计算树逻辑）或LTL（线性时态逻辑）表示。这种属性写入不是一个简单的问题。 为了正确地编写它们，需要先进的逻辑知识和从系统中获得的规范类型。我们的工具克服了这个问题，因为它有一个助手，可以指导用户编写属性，直到最终按照适当的语法获得要验证的属性。我们的出发点是Dwyer等人提出的模式分类”[4]“我的一个朋友，是一个不平凡的人。7Cadence SMV。http：//www-cad.eecs.berkeley.edu/enmcmil/smv12法医Beato等人/理论计算机科学电子笔记127（2005）3R前全局Q之后在Q和R在Q之后直到RQ QQQ R QR QQQ R Q见图7。 规范范围。已经添加了验证。7.1财产形态属性写作助手是基于Dwyer等人[4]提出的模式方案，其中建立了模式之间的第一个分类的发生和顺序。一个系统的大多数性质在实践中得到验证，都符合这两个类别之一发生模式描述了系统演化过程中状态或信号发生的特性这些包括缺席（从不），普遍性（总是），存在（有时）和有限存在（出现一定次数）。顺序模式根据它们出现的顺序建立属性。它们包括：优先级（s先于p），响应（s响应p），以及两者的组合：链优先级（s和t先于p或p先于s和t），链响应（s和t响应p或p响应s和t）和约束链（s和t不响应p）。另一方面，每种模式都有一个应用范围，它表明了它必须在其上进行验证的系统执行。有五个基本范围：全局（整个程序执行），在R之前（直到给定属性的执行），在Q之后（在给定属性之后的执行），在Q和R之间（从给定属性到另一个给定属性的执行的任何部分）以及在Q之后直到R（类似于之间，但即使第二个属性没有发生，执行的指定部分也会继续）。图7显示了由不同类型的作用域指定的执行部分。7.2物业分类需要验证的不同属性已被编目，以确定范围（Q和R）的限制，并指定更多属性时的属性顺序RR法医Beato等人/理论计算机科学电子笔记127（2005）313见图8。财产分类。必须确定（s，tooz），因此用户不需要知道或理解SMV中获得的质量标准的结构即可进行验证。已建立的属性类型如下所示（参见图8）。• 具有一个活动对象的状态机处于特定状态。• 对象Activity处于特定状态。• 产生信号或事件• 属性的值比较该工具将根据所选选项和所选模式和范围，以适当的格式自动生成属性。一旦我们有了要验证的属性，就可以使用工具本身执行SMV模型检查器来执行验证。如果属性不满足，它会生成一个跟踪，显示它未被验证的情况例如，对于自动柜员机，可以验证卡从未被保留;这意味着保留的信号从未发生。物业描述如下：D描述卡永远不会被保留P模式缺失S型罩全球产生一个信号S规格自动获得G（~保留）正如预期的那样，检查器的结果是假的。如果分析生成的反例跟踪（见下表），可以看出，当有2个错误的PIN号时，卡被保留，并再次生成errorPin14法医Beato等人/理论计算机科学电子笔记127（2005）3步骤626364|：65st_ATM活性活性活性活性st_activecheckingPinupdateErrorupdateErrorupdateErrorst_checkError不知道检查分支保持errorPin1000ATM_errorCounter2222保留00018相关工作大多数使用形式方法技术处理UML验证的工作都集中在状态图验证上。许多这样的论文是基于以前的工作，使用形式化的方法，验证了经典的状态图哈雷尔[6]，UML状态图是基于。然而今天，由于UML的使用如此广泛，研究人员正在寻求用形式化方法在UML验证方面更进一步。研究的重点是获得能够在没有用户干预的情况下以正式语言自动给出系统规范的工具为验证UML系统规范而开发的工具可以根据所使用的形式语言进行分类，作为验证之前的语言，用于表示系统。• Promela语言（工具Spin）。大多数关于UML验证的工作都是为模型检查器Spin开发的在这一领域的主要贡献是：vUML [9，13]。vUML是一个自动验证UML模型的工具，专注于状态图。它易于使用，自动生成Spin中系统的表示，并执行自动验证，以检查从未达到错误状态，并达到编目为理想状态的状态。Latella ， Majzik Massink [8] 使 用 UML 状 态 图 ， 通 过 分 层 自 动 机（HA）对其进行编码，从中生成Spin的规范。转换不是自动进行的，尽管他们在后来的作品中使用XMI DarMajBen02实现了这一点雨果[14，7]。这个项目包括一组工具，用于将模型检查应用于UML状态图和协作图。后者用于检查协作图中表示的交互是否可以使用状态机执行。这是为了验证。从UML到Spin的步骤是使用XMI自动执行的• SMV语言。在文献中也有一些作品试图通过使用SMV模型检查器来验证UML。VeriUML [2]是一套在大学开发的集成工具···法医Beato等人/理论计算机科学电子笔记127（2005）315它允许验证UML状态图，并检查模型在语法上是否正确。第一套工具于2000年开发，后来得到了扩展[15，16]，允许验证模型这种方法的切入点但核查不是自动的。TCM（Toolkit for Conceptual Modeling）是R.Eshuis [5]只允许通过将活动图转换为可以使用nuSMV验证的转换系统来验证活动图。转换是自动的，尽管它不是基于XMI的。如果将本文中的工作与上述工作进行比较，可以得出结论，本文的主要特点集中在对UML规范的行为进行自动验证的可能性上，其中所述行为通过状态和活动图来反映，并且对用户也是半透明的。大多数作品都没有进行自动验证，而vUML [9，13]没有使用时态逻辑的潜力，基于检查不可能达到错误状态来实现有限的验证。这些错误状态是由用户在图中引入的，因此图更加复杂。还应该指出的是，虽然由于篇幅有限，这里没有讨论，但是状态和活动图的代表元素都包含在这种方法中（除了同步状态、带参数的事件以及对象的动态创建和销毁），这是这个领域中其他贡献所不能说的，其中UML提供的特征很少（历史状态、延迟事件、由终止触发的transi-tions..）都处理好了9结论和今后的工作本文提出了一种工具，其主要目的是整合正式的方法与非正式的方式是透明的用户。准确地说，它使用SMV验证UML活动行为。虽然这不是一个新的想法，但就我们目前所知，没有任何地方可以联合验证活动图和状态图，使用前者来表示类操作的行为。然而，该工具最具创新性的特点是，尽管使用了时态逻辑的潜力来验证系统，但用户不需要了解其工作原理。此外，用户不需要知道·16法医Beato等人/理论计算机科学电子笔记127（2005）3得到的规范的结构，从而消除了使用形式方法的主要不便之一。至于未来的工作路线，当性质不满足时，对验证中获得的痕迹进行某种处理似乎是很有意义的。更准确地说，跟踪的表示应该是可视化的，而不是书面的，通过使用一些UML图或状态和活动机器的动画表示，这可以帮助用户非常快速地定位错误源。引用[1] 布奇·G Rumbaugh J.和Jacobson I.：统一建模语言。02 The Dog（1999）[2] 康普顿K.，Gurevich Y.，Huggins J.和Shen W.：UML的自动验证工具。密歇根大学CSE-TR-423-00（2000年）[3] Darvas A.，迈济克岛Beny B.：嵌入式系统的UML状态图模型验证第五届IEEE电子电路与系统设计与诊断研讨会论文集（2002）70-77[4] 德怀尔·M B、阿夫鲁宁湾S. Corbett J.C.：有限状态验证的属性规范模式。第21届软件工程国际会议论文集（1999）[5] Eshuis R.：工作流程建模的UML活动图的语义和验证PhD. 特温特大学。（2002年）[6] Harel D.：STATECHARTS：A Visual Formalism for Complex Systems.计算机程序设计科学，北荷兰8（1987）231[7] 纳普河Merz S.：UML状态机和协作的模型检查和代码生成。Proc. 第五届WSH系统设计和验证工具（2002）59[8] 拉泰拉·D迈济克岛Massink M.：使用SPIN模型检查器自动验证UML状态图的行为子集。计算的形式方面。国际形式方法杂志，Springer6，n。11（1999）637[9] Lilius J.和Porres I.：vUML：一个建模UML模型的工具。Turku Centre for ComputerScience，图尔库计算机科学中心，2000年，第272期（1999年）[10] 麦克米兰L.：符号模型检查。一种解决状态爆炸问题的方法。卡内基梅隆大学。CMU-CS-92-131。（一九九二年）[11] OMG
我的内容管理
展开
