基于Promela的UML建模方法及其应用

２０１０年第２期　文章编号：１００６－２４７５（２０１０）０２－０１０１－Ｏ４　计算机与现代化　＿ⅡＳＵＡＮＪＩ　ＹＵ　ＸＩＡＮＤＡＩＨＵＡ　总第１７４期　基于Ｐｒｏｍｅｌａ的ＵＭＬ建模方法及其应用　舒良春　，饶俊　，肖美华　，尹传文　（１．南昌大学计算中心，江西南昌３３００３１；２．江西省信息中心，江西南昌３３００４６）　摘要：针对形式化方法与可视化方法的优缺点，本文提出形式化方法与可视化ＵＭＬ互补的建模方法，主要探讨用形式化　方法验证ＵＭＬ模型，将ＵＭＬ模型转换为Ｐｍｍｅｌａ模型，再用模型检测工具ＳＰＩＮ对Ｐｍｍｅｌａ模型进行验证。最后通过实　例对此转换方法进行验证，实验结果表明了此方法的有效性。　关键词：ＵＭＬ；Ｐｒｏｍｅｌａ；ＳＰＩＮ；形式化方法　中图分类号：ＴＰ３１１　文献标识码：Ａ　ｄｏｉ：１０．３９６９／ｊ．ｉｓｓｎ．１００６－２４７５．２０１０．０２．０２８　Ｐｒｏｍｅｌａ－ｂａｓｅｄ　ＵＭＬ　Ｍｏｄｅｌｉｎｇ　Ｍｅｔｈｏｄｓ　ａｎｄ　Ｉｔｓ　Ａｐｐｌｉｃａｔｉｏｎ　ＳＨＵ　Ｌｉａｎｇ—ｃｈｕｎ　，ＲＡＯ　Ｊｕｎ　，ＸＩＡＯ　Ｍｅｉ．ｈｕａ　，ＹＩＮ　Ｃｈｕａｎ—ｗｅｎ　（１，Ｃｏｍｐｕｔｉｎｇ　Ｃｅｎｔｅｒ，Ｎａｎｃｈａｎｇ　Ｕｎｉｖｅｒｓｉｔｙ，Ｎａｎｅｈａｎｇ　３３００３１，Ｃｈｉｎａ；２．Ｊｉａｎｇｘｉ　Ｉｎｆｏｒｍａｔｉｏｎ　Ｃｅｎｔｅｒ，Ｎａｎｅｈａｎｇ　３３００４６，Ｃ￣ｎａ）　Ａｂｓｔｒａｃｔ：Ｉｎ　ｔｅｒｍｓ　ｏｆ　ｔｉｌｅ　ａｄｖａｎｔａｇｅｓ　ａｎｄ　ｄｉｓａｄｖａｎｔａｇｅｓ　ｏｆ　ｔｉｌｅ　ｆｏｒｍａｌｉｚａｔｉｏｎ　ｍｅｔｈｏｄｓ　ａｎｄ　ｔｈｅ　ｖｉｓｕａｌｉｚａｔｉｏｎ　ｍｅｔｈｏｄｓ，ｔｈｉｓ　ｐａｐｅｒ　ｐｒｏ—　ｐｏｓｅｓ　ｍｏｄｅｌｉｎｇ　ｍｅｔｈｏｄｓ　ｂａｓｅｄ　ｏｎ　ｈｅ　ｔｔＷＯ　ｍｅｔｈｏｄｓ，ｗｈｉｃｈ　ａｌｅ　ｒｅｃｉｐｒｏｃａｌ　ｓｕｐｐｌｅｍｅｎｔｅｄ　ｅａｃｈ　ｏｔｈｅｒ，ｉｔ　ｍａｉｎｌｙ　ｆｏｃｕｓｅｓ　ｏｎ　ｈｏｗ　ｔｏ　ｕｓｅ　ｈｅ　ｆｔｏｒｍａｌｉｚａｔｉｏｎ　ｍｅｔｈｏｄｓ　ｔｏ　ｖｅｒｉｆｙ　ｔｈｅ　ＵＭＬ　ｍｏｄｅｌ，ｃｏｎｖｅｙｓ　ａ　ＵＭＬ　ｍｏｄｅｌ　ｔｏ　ａ　Ｐｒｏｍｅｌａ　ｓｐｅｃｉｉｆｃａｔｉｏｎ，ａｎｄ　ｔｈｅｎ　ｕｓｅｓ　ｔｈｅ　ｆａｍｏｕｓ　ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ　ｔｏｏｌ　ＳＰＩＮ　ｔｏ　ｖｅｒｉｆｙ　ｉｔ．Ａｎｄ　ｉｔ　ｉｓ　ｒｅｓｕｌｔｅｄ　ｔｏ　ｂｅ　ａｖａｉｌａｂｌｅ　ｔｏ　ｖｅｒｉｆｙ　ｔｈｅ　ｃｏｎｖｅ￣ｉｎｇ　ｍｅｔｈｏｄｓ　ｔｈｒｏｕｇｈ　ａｎ　ｉｎｓｔａｎｃｅ．　Ｋｅｙ　ｗｏｒｄｓ：ＵＭＬ；Ｐｍｍｅｌａ；ＳＰＩＮ；ｆｏｒｍａｌｉｚａｔｉｏｎ　０　引　言　在目前通用的软件开发方法中，其描述通常还是　非形式化的方法和Ｔ具。然而这种非形式化的方法　并不能很好地描述不同组成系统之间的一些特性，已　经难以适应软件体系结构研究的进一步发展。因此，　在软件体系结构的研究过程中必须要有能显示描述、　有性的形式化研究工具。形式化方法作为一种　言，并在许多领域的软件开发中得到应用。但ＵＭＬ　对软件体系结构建模时，缺少分析体系结构所需的准　确语义，多视角建模视图之间也存在不一致性，这使　得对模型难以进行一致性检查和正确性分析，进而限　制了它的有效性。并且，这些非形式化特征使开发者　无法从中看　设计的优劣，不利于对系统优劣的度　量，不能帮助开发人员评估和改进。　因此，ＵＭＬ结合形式化的建模方法是解决ＵＭＬ　非形式化缺陷的重要途径之一，并将对软件系统的开　发具有重大的研究价值。　严格以数学为基础的方法，能够清晰、精确、抽象、简　明地规范和验证软件系统及其性质，帮助发现其它方　法不容易发现的系统描述的不一致、不明确或不完　整，有助于增加软件开发人员对系统的理解，因而形　式化方法能够极大地提高软件的安全性和可靠性。　ＵＭＬ作为一种通用的面向对象的建模语言，经　１　软件体系结构建模方法概述　形式化描述和可视化描述是目前主要的两类软　过了十几年的不断使用、修改、发展和完善，现在逐渐　趋于成熟，已成为在软件工业中占支配地位的建模语　收稿日期：２００９—１１－０２　件体系结构描述方法…。其中，形式化描述以体系　结构描述语言ＡＤＬ为代表，可视化描述以统一建模　语言ＵＭＬ为代表。　基金项目：２００８年江西省研究生创新专项资金省教育厅资助项目（ＹＣ０８Ａ０３２）　作者简介：舒良春（１９８３－），男，江西余干人，南昌大学计算中心硕士研究生，研究方向：计算机软件与理论；饶俊（１９７７一），男，　江西南昌人，江西省信息中心工程师，研究方向：计算机应用，计算机网络；肖美华（１９６４一），男，江西南昌人，教授，博士生导　师，博士，研究方向：软件＿Ｔ程，网络安全。　计算机与现代化　２０１０年第２期　１．１形式化描述软件体系结构　明显的不同，主要体现在需求分析和设计阶段，需要　软件工程中的形式化方法就是依靠数学模型和　投入比传统开发模式更多的＿［作量，但保证了软件体　系结构设计的一致性和可靠性，使得后期的编码和测　试工作相对简单。图１为ＵＭＬ与模型检测相结合的　计算来描述和验证一个目标软件系统的行为和特性，　包括需求规格、设计和实现等，其最根本的一点就是　建立在严格的数学基础上。使用形式化方法可以帮　软件体系结构建模过程　。　助开发者获得对其所描述的系统的深刻而正确的理　解，发现并及时更正设计中的错误和缺陷。软件开发　中的形式化方法主要是形式化规范说明语言，目前广　泛应用的一些形式语言，如Ｚ、ＶＤＭ、Ｂ、ＣＳＰ、Ｔｅｍｐｏｒａｌ　３形式化方法验证ＵＭＬ模型　３．１　ＵＭＬ模型验证过程　ＵＭＬ模型的验证过程是先将ＵＭＬ模型转换为　Ｌｏｇｉｃ、Ｌ１１Ｌ、Ｐｅｔｉｆ图等，这些形式化方法在功能上各有　侧重，可以互补　Ｊ。　１．２可视化描述软件体系结构　ＵＭＬ是一种将软件开发过程中　现的各种模型　用可视化图形来描述的语言，它融合了多种面向对象　开发方法的优点，采用统一的图形和符号从多个视角　描述软件系统的各种抽象模型，获得了国际标准化组　织的认可，并被国际软件界广泛接纳。但是随着软件　规模和复杂性不断增大，ＵＭＬ的不足就逐渐暴露出　来了。这是由于复杂系统的建模往往需要严格的语　义分析，而ＵＭＬ却缺乏准确的语义，这使得对软件体　系结构的可构造性建模能力较弱，缺乏形式化语义，　对体系结构的描述只能到达非形式化的层次，不利于　系统的求精和验证。　１．３形式化与可视化语言结合的软件体系结构建模　方法　形式化方法能产生精确、无二义性的形式规约，　为软件开发提供了严格的数学基础，但不够直观。　ＵＭＬ是一种可视化的图形建模语言，采用直观的图　形表示法为系统进行建模，但缺乏精确的语义。形式　化方法和ＵＭＬ存在很大的互补性，两者的结合研究　对提高软件的可靠性有着非常重要的意义［３］。　２　形式化方法与可视化ＵＭＬ互补的　建模方法　形　需　式　程　求　化　序　文　方　开　档　三　法　发　＾　规　建　验　格　慎　证　代　说　主　码　实　明　现　型　一　图１　ＵＭＬ与模型检测相结合的软件体系结构建模过程　由于形式化方法的加人，ＵＭＬ和形式化方法结　合的建模的目标与开发模式与传统的建模过程有着　形式化模型，再用模型检测工具进行验证。模型检测　的基本思想是用状态迁移系统（ｓ）表示系统的行为，　用模　时序逻辑公式（Ｆ）描述系统的性质。这样　“系统是否具有所期望的性质”就转化为数学问题　“状态迁移系统Ｓ是否是公式Ｆ的一个模型？”，用公　式表示为Ｓ　Ｉ＝Ｆ？。模型检测的优点在于它可以完全　自动地进行验证，目前，主要的模型检测丁具有：　ＳＭＶ、ＳＰＩＮ、ＣＷＢ、Ｖｅｆｉｓｏｆｔ、ＴＡＵ等　引。　本文主要讨论将ＵＭＬ模型转换为形式化建模语　言Ｐｒｏｍｅｌａ模型，并通过模型检测工具ＳＰＩＮ进行验　证。图２为ＵＭＬ模型的验证过程¨　。　图２　ＵＭＬ模型验证过程　３．２　ＵＭＬ模型的Ｐｒｏｍｅｌａ转换　从ＵＭＬ模型到Ｐｒｏｍｅｌａ模型的转换最重要的是　要保证转换的一致性。因此，本节从元模型的角度出　发，采用同态映射作为转换的方法，来保证转换的一　致性。所以，从ＵＭＬ验证模型到Ｐｒｏｍｅｌａ模型的转换　是通过建立ＵＭＬ元模型到Ｐｒｏｍｅｌａ元模型的同态映　射来完成的。　完整的描述系统需要能够捕捉系统的静态结构、　动态行为和对象之间的消息通信，因此，用ＵＭＬ模型　完整地描述系统需要涉及系统的静态、动态和测试用　例三个方面。　在ＵＭＬ视图中，类图描述了系统的静态结构，表　达一组对象类和它们的联系。在类图中，一方面描述　各个类本身的组成，即类的属性、操作和对象类的约　束；另一方面描述系统中类之间的各种静态的联系。　状态图描述了对象在事件驱动下状态转移的流程，反　映了一个对象生命周期内的行为。它将系统的动态　行为离散化为格局及其格局间的瞬时转换，格局类似　系统的快照，是相对稳定可见的；而转换是格局之间　２０１０年第２期　舒良春等：基于Ｐｒｏｍｅｌａ的ＵＭＬ建模方法及其应用　：：１０３　的跳转，是瞬时的，不可见的。协作图描述了与对象　结构相关的通信，有助于验证类之间的关联，甚至发　现新的关联需求。因而，使用类图作为系统的静态结　构，状态机图作为系统的动态结构，以及协作图作为　Ｑ　ｅＩ＿＿＋Ｅｖ＝ｅｌ；ＱｅＩ＝０　：：Ｑ　ｅｎ－÷Ｅｖ＝ｅ　；Ｑｅ　＝０　：：ｅ１ｓｅ—｝ｓｋｉｐ　ｆｉ　测试用例，就能够完整的描述一个系统。所以本文主　要讨论类图、状态图、协作图的Ｐｒｏｍｅｌａ转换。　（１）类图的Ｐｒｏｍｅｌａ语义。　ＨＪ、入动作的转换：　令状态ｓ的　、人动作函数分别为ｅｎｔｒｙ—Ａｃｔｉｏｎ　（Ｓ），ｅｘｉｔ—Ａｃｔｉｏｎ（Ｓ）进人某状态定义为：　规则１：类转换为同名的Ｐｒｏｍｅｌａ结构体类型，其　中参数转换为相应结构体参数。如：　Ｔｙｐｅｄｅｆ　Ｍｅｓｓａｇｅ｛ｍｙｔｙｐｅ　ｖａｒｌ；　Ｍｙｔｙｐｅ　ｖａｒ２；　｝　（２）状态图的Ｐｒｏｍｅｌａ转换。　①状态的形式化语义。　ＵＭＬ　Ｓｔａｔｅｃｈａｒ图的状态分为基本状态、ＯＲ一状　态、ＡＮＤ一状态和伪状态。ＯＲ．状态和ＡＮＤ一状态均是　一种状态精化，使得一个状态包含多个子状态，实现　状态层次结构和并发。伪状态又称连接子，是迁移路　径上的暂时点。它包括初始（ｉｎｉｔｉａ１）伪状态，浅度　（ｓｈａｌｌｏｗ）历史、深度（ｄｅｅｐ）历史ｊｏｉｎ、ｆｏｒｋ、条件分支　（ｂｒａｎｃｈ）和终止伪（ｆｉｎａ１）状态。　定义１顺序自动机。顺序自动机Ａ是一个四元　组（　，ｓ　，入　，８　），其中：　是有限状态集合；　ｓ０Ａ∈仃　是顺序自动机的初始状态；　是迁移标签的有限集合；　８　（【『Ａ×入　×　）是状态之间的迁移关系。　定义２层次自动机Ｈ是一个四元组：（Ｆ，Ｅ，Ｐ，　人）。　定义３一个格局表示层次自动机的一个全局状　态，它是一个状态集合Ｃ　（Ｓ　Ｈ），满足：　Ｓ∈　ｃａｍｔ．ｓ∈Ｃ；Ｖ　Ｓ１Ａ．ｓ∈ＣＡＡ∈ｐｓ＝　ｊ　ｌｓ　∈Ａ。ｓ　∈Ｃ。　定义４层次自动机Ｈ的操作语义是一个Ｋｒｉｐｋｅ　结构ｋ＝（Ｓ，Ｓ。，一）。　②转换算法。　把状态图中的事件定义为ｉｎｔ型常量，并且为每　个事件定义一个ｂｉｔ型的环境变量，假设状态图的事　件集合为：｛ｅ　一，ｅ　｝，则事件常量定义如下¨　：　＃ｄｅｆｉｎｅ　ｅｌ　１　＃ｄｅｆｉｎｅ　ｅ　ｎ　模拟选择事件的代码定义：　Ｓｅｌｅｃｔ＿ｅｖｅｎｔ（ｔｔ）　Ⅱ　Ｅｎｔｅｒ＿ｓｔａｔｅ（ｓ）＝　Ｓ＝１；ｅｎｔｒｙ＿Ａｃｔｉｏｎ（ｓ）　离开某个状态的代码定义为：　ｅｘｉｔ＿ｓｔａｔｅ（ｓ）＝　ｉｆ　：：（Ｓ一１）—｝ｓ＝０；ｅｘｉｔ—Ａｃｔｉｏｎ（ｓ）　：：ｅｌｓｅ－－￣ｓｋｉｐ　ｆｉ　模拟执行算法：　ｅｘｅｃｕｔｅＳｔａｔｅｃｈａｒ（Ｓ）Ｅ　Ｃ￣－－ｉｎｉｔＡｃｔｉｖｅＳｔａｔｅｃｈａｒ（Ｓ）　Ｑ　Ｓ．Ｅｖｔ　Ｗｈｉｌｅ（！ｅｍｐｔｙ（Ｑ））ｄｏ　Ｄｅｑｕｅｕｅ（Ｑ）　ＳＨ￣－－ｔｒａｎｓｉｔｌｏａｎ—ｓｅｌｅｃｔｉｏｎ（Ｃ，ｅ）　Ｉｆ（ＳＨ！＝　）　Ｆｏｒ　ｅａｃｈ　ｔ∈ＳＨ　ｄｏ　Ｃ　Ｃ＼｛ｓｏｕｒｃｅ（ｔ）｝　ｒｕｎＡｃｔ（ｅｆｅｃｔ（ｔ））　ｃ—ｃｕ｛ｔａｒｇｅｔ（ｔ）｝　ｏｄ　ｆｉ　ｏｄ　③协作图的Ｐｒｏｍｅｌａ转换。　在ＵＭＬ的模型中，协作图显示了关联和类元角　色，通过消息编号指定了它们的发送次序，描述了系　统的一个协作中参与对象之间的交互。因此，可以根　据其消息编号写出相应的　Ｌ公式，并转换为　Ｐｒｏｍｅｌａ中的Ｎｅｖｅｒ　Ｃｌａｉｍ，从而通过ＳＰＩＮ工具来验证　系统的正确性。　４　实　验　举一个并发模型的例子，图３为著名的哲学家进　餐问题的类图，哲学家一边吃一边思考，但是在他吃　东西之前，必须拿起左有两边的叉子。因为哲学家类　被标记为激活状态，因此这个类的所有对象都能并发　的运行　“　。　１０４　Ｐｈｌｌｏ，，ｏｐｈｅｖ　ｆｉ２ｔｌ１～　计Ｆｏｒｋ　ｔａｋｅｎ：ｂｏｏｊ　算机与现代化　２０１０年第２期　５　结束语　从广义的角度上说，形式化方法是软件开发过程　ｅａｔ（）　ｔｌｈｎｋ０　ｌｅｆｔ～　“）　ｉｅｔｅａ￣ｅ（）　中分析、设计及实现的系统工程方法；从狭义的角度上　图３哲学家进餐问题的类图　看，形式化方法是软件规格（Ｓｐｅｃｉｉｆｃａｔｉｏｎ）和验证　（Ｖｅｒｉｉｆｃａｔｉｏｎ）的方法。将形式化方法用于软件开发　的主要目的是保证软件的正确性。通过ＵＭＬ与形式　化方法的结合，可以消除对模型理解时存在的二义　在例子中，笔者使用状态图来描述哲学家进餐的　行为，如图４所示。将叉子对象的行为抽象为两个不　同的状态：“可用状态”，表示叉子在桌上，处于可以使　用的状态；“占用状态”，表示叉子不在桌上，而在某人　性，更精确地表示系统的功能，同时也可以使程序员　的手中。叉子对应着两个调用事件：获得和释放。　●　Ｔ　］　．、、１　１　　押…　］　ｉ（　ｌｒ一一。｝兰兰；　图４哲学家进餐问题的状态图　ＵＭＬ协作图表示几个相关对象的合作关系。组　成协作图的主要元素是对象及对象之间的链接。通　过上面的转换方法，可以得出Ｐｒｏｍｅｌａ模型．　ＩＴｌｙｌｙｐｅ＝｛ｔｈｉｎｋｉｎｇ，ｈｕｎｇｒｙ，ｅａｔｉｎｇ｝　ｐｒｏｃｔｙｐｅ　ｐｈｉｌｏｓｏｐｈｅｒ｛　ｓｔａｔｅ＝ｈｕｎｇｒｙ；　ｉｆ　：：ｓｔａｔｅ．Ｌｅｆｔ＝Ｗａｉｔ．Ｌｅｆｔ　：：ｓｔａｔｅ．Ｌｅｆｔ＝Ｇｅｔ．Ｌｅｆｔ　６　ｉｆ　：：ｓｔａｔｅＲｉｇｈｔ＝ＷａｉｔＲｉｇｈｔ　—＿：：ｓｔａｔｅ—Ｒｉｇｈｔ＝ＧｅＬ硒ｇＩｌｔ　矗　ｓｔａｔｅ＝ｅａｔｉｎｇ；　Ｒｅｌｅａｓｅ＿Ｌｅｆｔ；　Ｒｅｌｅａｓｅ—．Ｒｉｇｈｔ；　Ｓｔａｔｅ：ｔｈｉｎｋｉｎｇ；　｝　利用ＳＰＩＮ模型检测Ｔ具对上述Ｐｒｏｍｅｌａ模型进　行验证，可以检测出当所有哲学家都持有左边的叉子　而等待右边叉子这个死锁问题。　较早地对系统功能有一个清晰、准确的理解，从而有　助于整个系统的开发。　参考文献：　［１］戎玫，张广泉．形式化与可视化相结合的软件体系结构　描述方法研究［Ｊ］．计算机科学，２００５（４）：２０５－２０８．　［２］古天龙．软件开发的形式化方法［Ｍ］．北京：高等教育出　版社，２００５．　［３］夏建勋，唐红武．需求分析的ｚ语言形式化方法［Ｊ］．科　学技术与Ｔ程，２０ｏ８（８）：２２４５－２２４８．　［４］　祝义，张永长，张广泉，等．ＵＭＬ与ｚ结合的建模过程及　其应用［Ｊ］．计算机科学，２００７（５）：２７３－２７６．　［５］林惠民，张文辉．模型检测：理论、方法与应用［Ｊ］．电子　学报，２００２，３０（１２Ａ）：１９０７－１９１２．　［６］张频，罗贵明．ＵＭＬ模型检测方法的研究［Ｊ］．计算机应　用，２００７，２７（１０）：２４９３－２４９７．　［７］王璐珍，董威，陈火旺．ＵＭＬ顺序图的自动验证［Ｊ］．计　算机工程与应用，２００３，３９（２９）：８０－８３．　［８］　马重明，胡湘云．基于ＵＭＬ的软件体系结构建模方法研　究［Ｊ］．计算技术与自动化，２００５（２）：９４－９６．　［９］　黄锦，陈晓苏，肖道举，等．基于模型检验的软件安全静　态分析研究［Ｊ］．微计算机信息，２００７，２３（３Ｏ）：８６－８７．　［１０］钱忠胜，缪淮扣．面向构件的系统开发及其形式化［Ｊ］．　计算机应用与软件，２００８，２５（３）：９９—１０１．　［１１］Ｊｏｈａｎ　Ｌｉｌｉｕｓ，Ｉｖａｎ　Ｐｏｒｒｅｓ　Ｐａｈｏｒ．ｖＵＭＬ：ａ　Ｔｏｏｌ　ｆｏｒ　Ｖｅｒｉｆｙｉｎｇ　ＵＭＬ　Ｍｏｄｅｌｓ［Ｒ］．Ｔｅｃｈｎｉｃａｌ　Ｒｅｐｏｒｔ　２７２，Ｔｕｒｋｕ　Ｃｅｎｔｒｅ　ｆｏｒ　Ｃｏｍｐｕｔｅｒ　Ｓｃｉｅｎｃｅ，１９９９．　［１２］Ｔ０ｎｉ　Ｊｕｓｓｉｌａ，Ｊｏｒｉ　Ｄｕｂｒｏｖｉｎ，Ｔｏｍｍｉ　Ｊｕｎｔｔｉｌａ，ｅｔ　ａ１．Ｍｏｄｅｌ　ｃｈｅｃｋｉｎｇ　ｄｙｎａｍｉｃ　ａｎｄ　ｈｉｅｒａｒｃｈｉｃａｌ　ＵＭＬ　ｓｔａｔｅ　ｍａｃｈｉｎｅｓ　［Ｃ］／／Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　３ｒｄ　Ｗｏｒｋｓｈｏｐ　ＯＮ　Ｍｏｄｅｌ　Ｄｅｓｉｇｎ　ａｎｄ　Ｖａｌｉｄａｔｉｏｎ．ＭｏＤｅＶａ，２００６．　『１３］Ｓｔｅｆａｎ　Ｌｅｕｅ，ｅＧｒａｒｄ　Ｈｏｌｚｍａｎｎ．ｖ．Ｐｍｍｅｌａ：Ａ　ｖｉｓｕａｌ，ｏｂｊｅｃｔ－　ｏｒｉｅｎｔｅｄ　ｌａｎｇｕａｇｅ　ｆｏｒ　ＳＰＩＮ［Ｃ］／／（ＩＳＯＲＣ’９９）Ｐｒｏｃｅｅｄｉｎｇｓ　ｏｆ　２ｎｄ　ＩＥＥＥ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ｏｂｊｅｃｔ—Ｏｒｉｅｎｔｅｄ　Ｒｅａｌ－Ｔｉｍｅ　Ｄｉｓｔｉｒｂｕｔｅｄ　Ｃｏｍｐｕｔｉｎｇ．１９９９．　［Ｉ４］Ｃｈｅｎｇ　Ｂ，Ｃａｍｐｂｅｌｌ　Ｌ．ｉｎｔｅｇｒａｔｉｎｇ　Ｉｎｆｏｒｍａｌ　ａｎｄ　ｆｏｒｍａｌ　ａｐ－　ｐｒｏａｃｈｅｓ　ｔｏ　ｒｅｑｕｉｒｅｍｅｎｔｓ　ｍｏｄｅｌｉｎｇ　ａｎｄ　ａｎａｌｙｓｉｓ［Ｃ］／／Ｐｒｏ－　ｃｅｅｄｉｎｇｓ　ｏｆ　ｔｈｅ　Ｆｉｆｔｈ　ＩＥＥＥ　Ｉｎｔｅｒｎａｔｉｏｎａｌ　Ｓｙｍｐｏｓｉｕｍ　ｏｎ　Ｒｅ－　ｑｕｉｒｅｍｅｎｔｓ　Ｅｎｇｉｎｅｅｒｉｎｇ．２００１．