使用Z符号的用例图的多视图形式化模型:面向提高功能需求质量

摘要

我们提出了一个新的UML用例图的形式化模型，使用Z符号来解决它的一些缺点。因此，UML用例图已被普遍用于构造功能需求，而软件开发人员目前面临的最大挑战是交付满足客户需求的高质量产品。然而，UML模型的主要缺点是不精确。此外，它们基本上是半正式的建模表示形式和相关的自然语言需求，并且缺乏任何严格检查一致性的机制，这导致其模型容易出现歧义。本文报告了在多视图环境中第一个形式化的用例图建模方法。该方法分为两个步骤。在第一步中，使用Z符号提出了UML用例图的形式化模型。然后，提出了一种多视图一致性检查方法。这种方法保证了软件的一致性，提高了需求质量。

1.介绍

今天，人们的日常生活强烈依赖于越来越大而复杂的软件系统。“在软件中，要求是我们所做的一切的基础，所以要求质量是至关重要的”[1］．随着当今系统中的软件越来越大，需求文档变得非常庞大，不可避免地会引入模糊性。许多软件开发项目的失败是由于需求方面的问题。因此，通过更多地关注需求活动来提高软件质量变得非常重要。UML用例图[2，3.因此，由于其简单的设计促进了良好的软件工程实践，因此在推导软件要求的早期阶段常用于衍生软件要求的早期阶段。但是，一方面，UML中缺乏形式的形式用例图定义为误解提供了充足的空间。另一方面，UML型号不直接分析，缺乏机械检查类型的能力。

在本文中，我们建议使用z表示法的正式用例图模型[4，5从形式方法的严格性中获益。通过这种形式主义的概念，我们克服了UML用例图的限制，允许在Z规范(如Z/EVES系统)上使用类型检查器和定理证明器。值得注意的是，本文报告了第一个形式化的Z符号用例图，它考虑了多视图建模中的一致性。

本文是[6- - - - - -8]，他们首先描述了类，序列和状态机图的正式模型，并检查了不同视图之间的一致性。目前纸张中的扩展如下：（1）使用z表示法的正式模型，（2）通过Z定理进行多视图一致性检查。如上所述，“正式规范在软件开发的各个阶段可能是非常有用的工件”[9］．本文的目的是利用形式化方法的表达性和数学基础来提高需求质量。不仅如此，“正式的方法有助于以极低的缺陷率证明具有成本效益的软件开发”[10］．

本文的其余部分组织如下。部分2审查在使用案例图正式化的使用情况下完成的现有工作。部分3.使用Z符号表示用例图的正式模型。部分4讨论使用Z定理的类，序列和用例图之间的多视图一致性。最后，部分5包含一些结束语，并概述了我们今后工作的一些方向。

2.相关工作

形式化UML用例图已经引起了研究团体的极大关注，因为它提供了相当大的潜力来帮助开发人员分析规范是否捕获了预期的需求。在本节中，我们将展示一些研究文献，这些文献展示了定义UML用例图语义的方法，并讨论了它与我们的方法的相似和不同之处。两个主要的研究学派一直在研究这个问题。第一个是提出将用例图转换成不同形式的技术和工具。例如，Junior等人[11提出了一个形式化的用例，使用图转换模型，目标是运行工具支持对用例进行分析并揭示可能的错误。Sinnig等人[12]提出基于非确定性有限状态机形式主义的集成开发方法，其定义了用于使用情况和任务模型的公共语义。巴特勒等人。[13通过用z编写的规范定义用例和相关术语的概念。重点是形式化和澄清用例及其相关概念的基本概念。在我们的工作中，重点是指定不同的组件和由用例施加的约束。此外，还增加了行动者的形式化及其与扩展点之间的继承关系。巴拉哈斯(14]为使用合金的使用情况模型提供模拟系统功能要求的工具的正式规范。除了我们的多视图一致性检查之外，我们的模型与Z语言和略有差异相似。Scandurra等。[15]提出asmetaRE框架，自动将用例模型转换为ASM可执行规范，然后通过对生成ASM的仿真和基于场景的仿真来验证系统需求。沈及刘[16]提出了一种新的严格审查技术，包括执行和测试，可以使用新的语言HCL（高级约束语言）应用于软件要求模型。Murali等。[17描述一种使用事件b在UML用例建模中嵌入正式方法的方法。它们扩展了用例建模以允许安全问题的显式表示。Mostafa等人[18使用Z规范提出了流行UML图(用例图、类图和状态机图)语法的形式化。它们形式化了用例图的每个基本概念，而没有将它指定为一个整体。在我们的模型中，用例图得到了很好的解释和形式化。对模型进行了改进，引入了可扩展场景的概念。

虽然第一所学校只有有针对性的正式化问题，但第二所学校侧重于使用案例图和其他UML图之间的多视图一致性。例如，yue等人。[19，20.]提出一种方法和一个名为ATOUCAN的工具，自动生成包括使用案例模型的类，序列和活动图的UML分析模型。但是，在其信息生成完整的UML分析模型中，使用情况图不充分。虽然它们选择将用案例模型转换为UML分析模型，但是我们使用z表示法提出了使用案例图的正式规范，为使用案例图和正式的UML图之间的子集进行了检查的基础，以便检查一致性。giese和hellal [21提出了一种方法，将用例形式的非正式需求与用OCL编写的更正式的规范联系起来。Ibrahim等人[22提出一组用例图、序列图和类图之间的一致性规则。采用逻辑方法对提出的一致性规则的抽象语法进行形式化定义。本文引用的大多数一致性规则都是用我们提出的Z符号模型处理的。

总体而言，这些研究突出了正式用例图的需要。然而，这些研究仍然狭隘地缩小。我们的方法包括使用z表示法将用案例图转换为正式模型，并在不同的UML图之间检查不同的UML图。此外，我们的作品是在多视图一致性检查和使用Z表示法的第一个的工作作品中很少的工作之一。不用说，通过我们的方法，客户和开发人员都可以享受正式语言的好处，以提高要求的质量，并随后获得所获得的软件的质量。

3.用例图的正式模型

用例图被考虑用于系统的高级需求分析，目的是捕获它的动态视图。它们本质上用于收集用例中捕获的系统的需求和功能，还用于识别与系统交互的内部和外部代理。这些代理人被称为演员。数字1显示ATM系统的用例图示例[3.］．

简而言之，使用案例图包括演员，用例及其关系。数字2说明用例图的抽象语法[3.］．

该方法的第一步是形式化用例的概念和它们之间的关系。为了更好地理解所提议的形式化模型，我们首先定义规范中涉及的不同术语，如包含用例、扩展用例和扩展点。

我们将使用Z符号来指定和描述用例图的不同概念。Z符号的基本概念[4，5的总结如下。

3.1。Z符号摘要

Z (4]是基于集合理论和数学逻辑的J.R.Irial创建的正式规范语言。在z表示法中，规范使用架构的概念来构建底层数学，并易于重用其子部分。它的图形表示法称为架构，如下所示：

架构包含声明部分，该部件可能包含对其他模式的引用旁边的状态变量和一个谓词部分，该谓词部分由约束可变状态值的一组谓词组成。这些谓词在状态变量上表达属性并引入它们之间的关系。z架构的名称可以重新使用。可以使用z架构或重新用作声明，类型或谓词。当规范需要复合类型时，使用模式来表示。

３．２．用例形式化

根据UML标准，用例定义为分类器。实际上，整个规范中的所有唯一标识符集都由给定集合表示分类器．

因此,变量UCASE作为分类器引入，以指定用例标识符集。

使用情况之间存在几种不同的关系。这些是包括关系，延伸关系和泛化，所有这些都在本节中描述。

包括是两个用例之间的关系，用于显示包含的使用情况的行为插入包括用例的行为“[3.］．扩展是一种关系，“它指定了通常可选的扩展用例中定义的行为如何以及何时可以插入到扩展用例中定义的行为中”[3.］．

关系包括和扩展基本上表示为z关系，其涉及两个用例。关系包括用来记录哪个用例直接包含在原始用例中，而关系呢扩展用来记录哪个用例直接扩展了原始用例。

功能includedUsecases和extendingUsecases分别用传递闭包得到包括和扩展．它们用于正式地指定函数，该函数返回与包含或扩展关系直接或间接相关的用例集。

扩展可能发生在被称为扩展点的扩展用例的特定点。扩展点与指示何时发生扩展的约束相关联。根据UML标准，扩展点必须有一个名称。正式地，扩展点的指定如下:

如果没有关联约束，则扩展是无条件的。在本例中，状态变量约束是一个空集，因此它的基数等于0。

用例泛化是从子用例到父用例的关系，指定孩子如何专注于父级描述的所有行为和特征。使用案例泛化通过在架构中添加到z中Usecase，状态变量父母定义为一组用例。

一旦用Z编写的规格说明澄清了用例的相关术语，用例的概念就可以完全形式化了。

因此，用例的概念在下面的模式中清晰地表示出来:

上半部分Usecase模式用它们各自的类型定义用例的不同变量。每个用例都由其调用的标识符标识自我和它的名字。如前所述，变量父母用于定义由当前用例专门化的用例集。

如果一个用例被扩展，那么它将由一系列片段和一个有序的扩展点列表组成。一个扩展用例由一个或多个行为片段描述组成，这些描述将被插入到扩展用例的适当位置。扩展点指定在何处插入扩展用例的各个行为片段[3.］．如果在到达第一个扩展点时条件为真，那么将执行扩展用例。否则不会发生扩展。如果没有约束与扩展关系相关联，则扩展是无条件的。

正如模式后半部分的第一个谓词所述Usecase，一个用例不能包括直接或间接包括它的用例。

在定义了用例的概念及其相关术语之后，我们可以进入下一步，即指定参与者及其关系。

3．3．演员形式化

“Actor指定用户或与主题交互的任何其他系统播放的角色[3.］．根据UML标准，参与者被定义为分类器。实际上给定的集合分类器用于定义整个规范中所有唯一标识符的集合。的变量演员作为分类器引入，以指定参与者标识符集。

参与者可以是人类用户、某些内部应用程序或某些外部应用程序。参与者类型作为代表两种类型参与者的枚举集引入。

对于参与者来说，主要有两种类型的关系:(1)参与者和用例之间的关系，(2)参与者之间的关系只不过是泛化。

参与者和用例之间的关系基本上表示为一个将参与者与用例关联起来的Z关系。关系associationAU用于记录演员可以使用哪种用例，而函数相关性返回与参与者关联的用例集。

参与者泛化用于提取并重用参与者之间的相似性。这种关系表明一个参与者继承了另一个参与者的角色和属性。为了表示泛化，我们选择在模式的声明部分添加一个状态变量演员如下所示。调用此状态变量父母并指定为一组参与者。泛化关系还意味着后代参与者可以使用为其祖先定义的所有用例。这在谓词部分有清楚的说明。

这个函数getActorFromACTOR接受一个参与者标识符并返回相应的参与者。这个功能将在稍后的用例图形式化中使用。

类似地，我们定义函数getUsecaseFromUCASE．

3．4．用例图形式化

根据用例，演员及其关系的形式化，可以完全定义使用案例图的概念。如下面的架构所示，用例图具有名称，它由一组演员和一组用例组成。

我们还指定了在扩展的情况下用例的执行场景。我们提出函数UCexecution它接受一系列用例片段和扩展点，并返回一个布尔类型。该函数指示是否执行扩展。

第一个谓词声明，对于每个参与者，继承的用例只是其父的相关用例。同样重要的是要注意用例和参与者标识符是惟一的。第四个谓词声明用例不能包括直接或间接包含它的用例。最后一个谓词表示只有当约束为真或扩展是无条件的时，才会发生扩展。

现在我们集中讨论如何使用本节中定义的用例图的正式规范来检查多视图的一致性。在下面的部分中，我们将讨论用例图、类图和序列图之间的一致性。

4.多视图一致性检查

讨论了如何使用z表示法构建正式的使用案例图模型，本文的最终部分解决了检查多视图上下文中的一致性的方法。多视图建模是在不同视图或模型方面描述系统的不同方面的方法。该方法呈现了几个挑战，特别是那些与一致性有关的挑战，这可能会使系统的完整性造成风险。“一般来说，当它的部分之间存在逻辑连贯（即，没有矛盾）时，系统是一致的[23］．出于这些原因，必须显示所有视图，它们之间存在一致和连贯。

一旦定义了正式的使用案例图，它对陈述和证明不同视图之间的定理非常有用。这有助于验证系统并检查错误。在本文中，我们专注于系统的三种不同模型的一致性，包括类图，序列图和用例图。请注意，类图和序列图，分别在[中的z表示法中定义6，7］．

4.1。使用案例图和序列图之间的一致性

为了形式化用例图和序列图之间的一致性的概念，我们考虑一个Z定理叫做consistencyUsecaseAndSequenceDiagram。这个定理检验了（一世）每个用例名对应于一个序列图框架;(2)使用情况下的演员图被定义为序列图中的对象。

这里，对于任何用例图ud.，一个用例UC.和一个演员一个这样UC.和一个分别是ud.用例和参与者UC.是在与之相关的用例中一个;然后存在序列图sd使其帧对应于名称UC.和标识符一个是在一套sd对象。

如果定理被证明是真的，那么之前表达的每个约束都可以满足，因此这将保证系统始终保持一致的状态。

4.2。使用案例图和类图之间的一致性

现在让我们定义用例图和类图之间的一致性的概念。

首先，给定一个类图的实例和一个用例图，我们定义一个Z定理称为consistencyUsecaseAndClassDiagram．这个定理声称，如果我们假设，这两种观点是一致的（一世）参与者与类图中已定义的类对象相对应。(2)使用情况下的用例将分配给类图中类的操作。

我们定义函数人事处考虑到用例，返回相应的操作。

这里，对于任何用例图ud.，一个用例UC.和一个演员一个这样UC.和一个分别是ud.用例和参与者;然后存在一个名为班级这样一个的对象集中的班级和UC.对应于其操作之一。

所提出的定理确保规范满足前面提出的约束条件。如果满足了约束条件，那么规范就是一致的。这个定理应该被证明是正确的。

关于类图和序列图形式化的进一步信息，读者可以参考[6，7］．

5.结论和未来的工作

“要求的规范是实现任何软件项目的目标的关键活动，它已经由研究人员和从业者建立和认可”[24］．在本文中，我们考虑了用例图的主要概念的形式化规范。我们工作的目标是使用Z符号和Z定理的一致性检查来提供简明和明确的用例图规范。用例图的正式规范在过去已经使用不同的语言完成了，但是我们相信Z符号的表达性和数学基础为这种形式主义提供了一个更丰富的框架。我们研究背后的主要动机是这样一个事实:使用正式规范可以极大地提高所生产的软件的质量，也可以显著地节省软件开发过程中的成本。

进一步研究的一个重要领域是找到处理更大视图的方法，以检测更多的不一致性。我们还计划扩展我们的原型以包括用例图的形式化。我们重申，我们的原型自动地将UML图的子集转换为Z形式规范，以发现迄今为止发布的大多数UML不一致。此外，我们将使用一些工业应用实例使我们的方法更实际。所有提出的规范都经过了语法检查，并使用Z/EVES系统证明是正确的[25是分析Z规格的工具，支持型式检验和定理证明。

数据可用性

没有数据支持本研究。

的利益冲突

作者声明他们没有利益冲突。

参考文献

1. W. S. Humphrey，《软件质量的挑战》CROSSTALK:国防软件工程杂志，第4-9页，2008。视图:谷歌学术
2. G.Booch，J. Rumbaugh和I. Jacobson，统一建模语言用户指南，艾迪生韦斯利，读书，英国，第1版，1999年。
3. “OMG统一建模语言上层结构2.4.1”，2011，http://www.omg.org/spec/uml/2.4.1/superstructure.．视图:谷歌学术
4. J. M. Spivey，z表示法：参考手册，英国牛津奥里尔学院，第二版，1998。
5. j·伍德考克和j·戴维斯，使用Z:规范、细化和证明， Prentice-Hall，上马鞍河，新泽西州，美国，1996。
6. K. el Miloudi，Y.El Amrani和A. Ettouhami，“将UML类图的自动翻译为正式规范，以检测UML不一致”第六届国际联盟的诉讼程序。关于软件工程进步，pp.332-438，巴塞罗那，西班牙，2011年。视图:谷歌学术
7. K. El Miloudi, Y. El Amrani，和A. Ettouhami，“在多视图建模中使用Z形式规范以确保一致性，”理论与应用信息技术学报，卷。57，没有。3，pp。407-411,2013。视图:谷歌学术
8. K. El Miloudi和A. Ettouhami，“使用Z符号形式化UML状态机图的多视图方法”，WSEAS计算机交易， vol. 14, pp. 72-78, 2015。视图:谷歌学术
9. A. Bollin，“量化Z规范中进化变化的度量”，软件学报:进化与过程，卷。25，不。9，pp。1027-1059,2013。视图:出版商的网站|谷歌学术
10. A. Hall，“实现形式方法的好处”，在正式方法和软件工程年第3785卷计算机科学的讲义，第1-4页，施普林格柏林，海德堡，柏林，海德堡，2005。视图:出版商的网站|谷歌学术
11. J. Oliveira，L.Ribeiro，E.Cota等，“基于形式方法的用例分析：实证研究，”代数发展技术的最新趋势年第9463卷计算机课堂讲稿。科学。，第110-130页，施普林格国际出版公司，瑞士，2015。视图:出版商的网站|谷歌学术|Mathscinet.
12. D. Sinnig, P. Chalin，和F. Khendek，“用例和任务模型，”美国计算机学会软件工程与方法论汇刊，卷。22，没有。3，pp。1-31,2013。视图:出版商的网站|谷歌学术
13. G. Butler, P. Grogono，和F. Khendek，“用例的Z规格说明”第五届亚太软件工程会议论文集，pp.94-101，台北，台湾，1998年。视图:谷歌学术
14. F. V. Barajas，“需求工程工具的正式模型”第一个的诉讼程序。合金车间，pp。63-70，波特兰，奥勒，美国。视图:谷歌学术
15. P. Scandurra, A. Arnoldi, T. Yue，和M. Dolci，“通过将用例模型转换为抽象状态机来验证功能需求”第27届应用计算研讨会论文集，第1063-1068页，ACM出版社，纽约，美国，2012年3月。视图:出版商的网站|谷歌学术
16. W. Shen和S. Liu，“用例图的形式化、测试和执行”，在正式方法和软件工程年第2885卷计算机科学的讲义，第68-85页，施普林格柏林，海德堡，柏林，海德堡，2003。视图:出版商的网站|谷歌学术
17. R. Murali, A. Ireland，和G. Grov，“结合用例建模和事故场景的严格方法”，在美国宇航局的正式方法，卷。9058计算机科学的讲义，pp。263-278，斯普林克国际出版，秋葵，2015年。视图:出版商的网站|谷歌学术
18. a . M. Mostafa, M. a . Ismail, H. EL-Bolok，和E. M. Saad，“使用Z规范走向UML2.0元模型的形式化”，刊于第八届ACIS软件工程国际会议，人工智能，网络和并行/分布式计算会议（SNPD 2007），页694-701，中国青岛，2007年7月。视图:出版商的网站|谷歌学术
19. 岳涛，L. C. Briand, Y. Labiche， " aToucan， "美国计算机学会软件工程与方法论汇刊，卷。24，不。3，pp。1-52,2015。视图:出版商的网站|谷歌学术
20. T. Yue, L. C. Briand，和Y. Labiche，“从用例自动推导UML序列图”，技术代表TR-SCE-10-03，卡尔顿大学，加拿大，2010。视图:谷歌学术
21. M. Giese和R. Hartal，“从UML的非正式规范从UML，”第七届国际会议记录。2004 -统一建模语言。建模语言和应用程序2004，第3273卷计算机科学的讲义，页197-211，施普林格柏林海德堡，德国海德堡，2004。视图:出版商的网站|谷歌学术
22. N. Ibrahim, R. Ibrahim, M. Z. Saringat, R. Mansor，和T. Herawan，“用例驱动的基于规则确保UML模型的一致性，”awerprocdia信息技术与计算机科学， vol. 1, pp. 1485-1491, 2012。视图:谷歌学术
23. M. Alférez, R. E. Lopez-Herrejon, A. Moreira, V. Amaral, and A. Egyed，“早期软件产品线规格说明中的一致性检查- VCC方法，”通用计算机科学杂志，第20卷，第2期。5、2015年。视图:出版商的网站|谷歌学术
24. R. P. Oliveira, E. Insfran, S. Abrahao等人，“软件产品线的功能驱动需求工程方法”2013第七届巴西软件组件、架构和重用研讨会论文集，pp.1-10，Brasília，DF，巴西，2013年9月。视图:出版商的网站|谷歌学术
25. I. Meisels，“Windows Z/EVES版本2.3的软件手册”，技术代表TR-97-5505-04h, Ora，加拿大，2004。视图:谷歌学术

版权

版权所有©2018 Khadija El Miloudi和Aziz Ettouhami。这是一篇发布在知识共享署名许可协议，允许在任何媒介上不受限制地使用、传播和复制，但必须正确引用原作。