广东工业大学学报  2017, Vol. 34Issue (6): 54-60.  DOI: 10.12052/gdutxb.160144.
0

引用本文 

曲璨, 张立臣. 基于形式化方法的面向方面需求分析[J]. 广东工业大学学报, 2017, 34(6): 54-60. DOI: 10.12052/gdutxb.160144.
Qu Can, Zhang Li-chen. An Aspect-oriented Requirement Analysis Based on Formal Method[J]. JOURNAL OF GUANGDONG UNIVERSITY OF TECHNOLOGY, 2017, 34(6): 54-60. DOI: 10.12052/gdutxb.160144.

基金项目:

国家自然科学基金资助项目(61572142，61370082)；广东省自然科学基金资助项目(2015A030313490)

作者简介:

曲璨(1990–)，女，硕士研究生，主要研究方向为信息物理融合系统、面向方面编程。

通信作者

张立臣(1962–)，男，教授，主要研究方向为信息物理系统、分布式处理等. E-mail：lchzhang@gdut.edu.cn

文章历史

收稿日期：2016-11-11
Contents              Abstract              Full text              Figures/Tables              PDF
基于形式化方法的面向方面需求分析
曲璨, 张立臣     
广东工业大学　计算机学院 ，广东　广州  510006
收稿日期：2016-11-11
基金项目：国家自然科学基金资助项目(61572142，61370082)；广东省自然科学基金资助项目(2015A030313490)
作者简介：曲璨(1990–)，女，硕士研究生，主要研究方向为信息物理融合系统、面向方面编程。
通信作者：张立臣(1962–)，男，教授，主要研究方向为信息物理系统、分布式处理等. E-mail：lchzhang@gdut.edu.cn
摘要: 面向方面编程(AOP)可以通过它的横切属性有效地解决代码缠结和分散的问题, 但大部分的工作都集中在编程和实现阶段, 很少有对早期的需求分析模型进行研究. 本文通过采用AOP技术对软件系统的需求分析进行研究. 首先在需求分析阶段, 通过关注点分离技术识别出系统的功能需求和非功能需求, 功能需求由核心关注点通过组件来实现, 非功能需求由横切关注点通过方面来实现; 然后结合具有精确描述性特点的形式化语言Aspect-Z来表示组件和方面. 对于在同一连接点处需要编织多个方面且方面之间可能产生冲突的问题, 通过定义方面的优先级来解决. 最后, 通过定理证明的方法推理出所描述需求的性质与属性, 从而对Aspect-Z规格说明进行形式化验证. 文章的最后给出应用实例.
关键词: 面向方面    需求分析    Aspect-Z语言    形式化验证    
An Aspect-oriented Requirement Analysis Based on Formal Method
Qu Can, Zhang Li-chen     
School of Computer Science, Guangdong University of Technology, Guangzhou 510006, China
Abstract: Aspect-Oriented Programming (AOP) can effectively solve the code-tangling and code-scattering caused by crosscutting attributes; however, much work is presented on the programming and the implementation phase, and little has addressed the early model stages. A research is conducted on the requirements engineering phase of software by using AOP technology. First in the requirements analysis phase, the functional requirements and non-functional requirements are identified by the separation of concerns, and the functional requirements with components and the non-functional requirements with aspects are realized. Then the components and aspects are represented by combining with the formal language Aspect-Z which has the characteristics of accurate description. As actions accompany conflicts while two or more aspects affect the same joint point synchronously, a method is proposed to solve by defining aspects’ priority level. In the end, the properties and attributes of the described requirements are deduced by the theorem proving method, so as to achieve the purpose of formal verification of Aspect-Z specifications. Finally, an application example is given.
Key words: AOP    requirements analysis    Aspect-Z    formal verifications    

软件需求阶段是软件开发过程的第一个阶段，定义良好的需求模型可以避免在后期的设计编码和实现阶段花费昂贵的代价重构系统，从而降低软件开发风险[1-2]. 软件需求包括功能需求和非功能需求. 功能需求要求的是软件必须实现的功能；而非功能需求，是为满足用户业务需求而对软件系统提供的质量属性和功能约束，具体包括系统的性能、可靠性、安全性、可保障性等需求. 传统的需求规格说明[3-4]中，经常采用非形式化的抽象含糊语言描述非功能性需求，容易产生歧义或者被开发人员忽视，这些都造成了功能需求和非功能需求混杂，使代码分散、混乱、难以维护.

面向方面软件编程(AOP)[5-7]通过横切关注点分离出功能需求和非功能需求. 在非功能需求中，用方面定义和实现横切关注点，将非功能需求模块化，实现模块间的松散耦合，改善软件开发过程，提高系统的可维护性和可复用性. 形式化方法[8-9]具有描述的精确性、无二义性，是基于数学的并用于描述系统性质的技术. 形式化规格方法通过具有明确数学定义的语义或语言对软件行为进行精确、简洁描述. 文献[10]提出一种面向方面的非功能需求建模方法，通过扩展UML表达面向方面概念来实现. 文献[11]将AOP技术与AspectJ语言相结合，实现了对实时系统的分析研究，文献[12]采用Aspect-Z技术对实例进行分析.

本文将AOP技术和面向方面的形式化语言Aspect-Z相结合，并针对在同一连接点处产生冲突的问题，提出采用优先级的解决方法，实现对Aspect-Z的扩展. 采用形式化规格说明来对面向方面进行需求建模，可对系统的非功能需求精确表达并处理，对于在同一连接点处需要编织多个方面且方面之间可能产生冲突的问题，本文通过定义方面的优先级来解决. 其基本思想是通过Aspect-Z语言来表示组件和方面，通过编织机制实现系统的集成. 最后本文将通过实例进行详细说明.

1 相关知识 1.1 AOP基本原理及相关概念

AOP从本质上讲是一种关注点分离技术，它以松散耦合的方式来实现独立的关注点，然后组合这些关注点实现最终的系统. 传统的面向对象开发方法中，这些横切关注点散乱地分布在软件的多个类中，如图1左侧3种不同背景代表系统非功能需求的3个不同的关注点，它们散乱地分布在系统中. 在编程或者维护时不仅麻烦且容易遗漏，给开发和维护带来很大的困难. 图1右侧表示AOP技术将3个不同的关注点模块化为3个不同的方面封装在横切关注点中，并通过编织器织入到其他功能模块中，程序的维护和复用就简便许多，这也是AOP的本质特征[13].

面向方面需求工程(Aspect-oriented Requirement Engineering, 简称AORE )则是对AOSD的一种需求工程开发方法，通过关注点分离的方法定义并处理需求，将功能需求分离为系统的核心关注点，通过组件语言负责实现；非功能需求则分离为系统的横切关注点，封装在方面中来实现某个关注点的模块单元. 如果组件和方面之间没有冲突，则这两种语言通过编织器无缝编制来实现系统，若在组件的同一连接点处需要实现多个方面，则需要判定方面之间的优先级来解决冲突，之后再进行编织实现系统. 如图2所示.

图 1 AOP中横切关注点的实现原理图 Figure 1 The schematic diagram of cross cutting concerns in AOP
图 2 AOP系统实现方法 Figure 2 The realization method of AOP
1.2 形式化开发方法及语言

软件的形式化开发方法是在20世纪50年代由Backus提出的巴克斯范式(Backus Normal Formula, BNF), 作为描述程序设计语法的元语言[7]. 形式化方法的基本含义是借助数学的方法来研究计算机科学中的有关问题. 从广义角度，形式化方法是软件开发过程中分析、设计以及实现的系统工程方法. 狭义的，它是软件规格和验证的方法. 在本文中主要讨论软件规格的方法. 形式化规格是通过具有明确数学定义的文法和语义的方法或语言对软件的期望特性或行为进行精确简洁描述.

Z是一种基于集合理论和一阶谓词的形式化语言，它支持软件的形式化规格、规格的推理及求精，是迄今为止最广泛的形式化语言之一. 模式是Z语言的基本结构，较好地描述软件系统的抽象状态和操作功能. 一个模式包括模式的名字、声明部分和谓词部分. 模式名(SchemaName)可以在规格过程中随处调用，也可以作为一个类型名. 模式的声明部分(Declaration)引入变量及其类型，这些变量为该模式的内部变量；谓词部分(Predicate)描述了在这些局部变量之间，或者局部变量在该模式之前声明的全局变量之间的不变式关系. Z模式如图3所示.

图 3 Z模式 Figure 3 Original Z schema
2 面向方面形式化语言Aspect-Z

Aspect-Z语言是通过加入方面符号，在传统Z语言基础上进行的一种扩展. 在软件开发需求分析阶段，通过形式化语言Aspect-Z语言和AORE相结合，将一个系统精确完整的模块化[14]. Aspect-Z将方面模式添加到Z相关的操作模式中，来表明系统方面的相关属性和行为.

需求分析是通过关注点分离出组件和方面(这也是Aspect-Z支持AOSD的主要思想)，且只考虑操作的主要步骤，将功能需求的操作模式建立一个组件模式；将非功能需求的操作模式建立一个方面模式，方面模式是对组件模式的横切. 其中方面模式的声明部分可准确地描述出系统中连接点的位置，谓词部分则主要表示在连接点处需要实现的功能，最后将组件模式和方面模式合并集成. Aspect-Z语言的基本模式如图4所示[9].

图 4 Aspect-Z模式 Figure 4 Original Aspect-Z schema

规则1 　当一个模式被命名之后，在另一个模式中可通过∆SchemaRef调用这个模式.

规则2 　ΩSchemaRef表示当前方面模式横切以SchemaRef命名的那个模式.

规则3 　在Aspect-Z中连接点是系统中一个精确的执行点，是需要执行方面的相关操作. PointcutDecl则是描述一系列连接点和连接点之间的相关属性.

规则4 　Advice是用来描述在切入点中每个连接点处应该执行的具体相关操作，包括insert操作和replace操作.

规则5 　若在同一切入点处有两个或两个以上的方面对此切入点横切，则应事先定义好两个不同方面的优先级，避免方面织入时发生冲突. 在该模式中W(b, pc)为二元操作符，其中b是基本模块名，pc是切入点名，符号“ $\leqslant $ ”表示当同一连接点对应多个不同的方面时，通过该符号表示不同方面之间在与基本模块进行编制的次序. 其合成模式[10](Composition schema)如图5所示.

图 5 合成模式结构图 Figure 5 Composition schema of structure diagram

现将Aspect-Z来表示一个基本模块BaseModel和一个方面模块AspectModel进行简单举例说明. 如图6和图7所示.

图 6 Aspect-Z基本模式 Figure 6 Aspect-Z base schema
图 7 Aspect-Z方面模式 Figure 7 Aspect-Z aspect-schema

从AspectModel方面模式可以看出对于Pointcut PC的通知(advice)是在每个PC元素处插入条件∀ x, y∈A·x≠y→*(x)≠*(y)，通过特殊集成符号“+”来表明最后的编织模式，则集成模式IntegratedModel为BaseModel+AspectModel. 方面集成模式如图8所示.

图 8 Aspect-Z集成模式 Figure 8 Aspect-Z integrated schema
3 基于Aspect-Z的需求分析 3.1 Aspect-Z与Rational的需求管理对比

对比于现有的需求管理的软件，IBM Rational RequisitePro[15]是一个强大、易用、集成的需求管理产品. 通过与Rational系列软件产品的广泛集成，大大扩展了RequisitePro及其他产品的功能，给软件工程生命周期内的各个阶段提供了强大、方便的信息查询、跟踪、管理功能. 表1是对Aspect-Z与Rational在关于需求分析方面的对比.

表 1 Aspect-Z与Rational的需求管理对比 Table 1 Comparison of demand management between Aspect-Z and Rational
3.2 基于Aspect-Z需求分析方法

在系统的需求分析中，用面向方面的开发方法构造的软件系统包括对象层和方面层. 在不修改对象模型的前提下，方面增加了对象的功能，使对象的原有功能不受影响.

基于Aspect-Z的需求分析过程如下所示：

(1) 首先获取系统的需求，构建出业务模型．

(2) 根据业务模型，建立系统用例模型．

(3) 根据系统用例，提取出系统的功能性需求和非功能性需求. 非功能性主要是指系统的功能性项目、可靠性、易用性、维护性、效率、可移植性等特性，并将非功能性需求封装成方面(aspect). 具体过程是由封装在aspect中的函数由advice实现. 首先需要在aspect中通过PoincutDecl定义需要织入的位置, 并定义advice的功能, 然后编织器将advice的调用语句无缝织入到其他模块中. 具体过程如图9所示.

图 9 实现非功能需求框架图 Figure 9 Framework for the realization of non-functional requirements of the system

(4) 用Aspect-Z语言分别来描述出系统的对象层和方面层，若在同一连接点处需要编织多个方面，则通过定义方面的优先级来解决．

(5) 将方面编织到对象中，集成完整的系统．

(6) 最后通过定理证明来验证Aspect-Z的规格说明以及描述的正确性.

4 案例分析 4.1 图书管理系统的体系结构

本文选取一个小型图书管理系统，并对该系统进行需求分析. 图书管理系统将传统的图书馆转换为数字信息化的图书馆，并对图书实现自动化的管理. 该图书管理系统包括管理员和读者两类用户，登录时系统需根据登陆信息判断这两类用户. 管理员可向书库中添加或删除图书，根据图书的编码查询图书信息，查询读者的借书信息. 读者可查询图书信息，并可进行借书、还书和续借等相关行为.

该系统共设置5个活动者. 分别是People、Registrar、Reader、Book和Database. 其中People泛指与系统发生关系的人；Registrar为图书管理员，负责添加、修改图书信息；Reader为所有读者，读者可能发生借书、续借、还书的行为；Book包含书的标题、对象及相关属性；Database为存储各种信息的数据库对象. 系统中共有AddBook、ModifyBook、Borrow、Renew和Return 5个用例. AddBook表示管理员添加图书信息；ModifyBook表示修改图书信息；Borrow表示读者借阅图书；Renew表示读者续借图书；Return表示读者归还图书. 系统的用例图如图10所示.

图 10 图书管理系统用例图 Figure 10 The use case diagram of library management system

除了满足上述的功能性需求之外，也需满足其定义的非功能需求，即记录系统日志并根据相应的结果进行提示. 管理员在添加或删除相应的图书并更新到数据库的同时，系统可调用相应的方面将这些信息记录到系统日志中，如果已成功记录，则提示成功，否则反之. 其中添加图书并调用对应方面模块的结构如图11所示.

图 11 图书管理系统的系统结构 Figure 11 The system structure of library management
4.2 基于Aspect-Z语言的非功能需求实现

图书管理系统中的非功能需求为：当图书信息发生变化，如图书借出或者归还、新增图书或者删减图书，将信息更新至数据库之后，再记录于系统日志中.

根据图书管理系统需求，将建立Users、Book和Database 3个基本模式，Book只包含声明模式用来说明图书的属性，而Users和Database两个模式结合起来则得到完整的系统状态. Book模式的内部变量包括标题(title)、作者(author)和主题(subjects) 3个属性，且同一本书包含有多个复本(copy)，对图书的操作就是复本的操作. Users模式又分为管理者和读者. Database模式中包括书库中所有的副本信息、目前的复本信息、各复本的借出情况、各复本最后一次借出的记录和各读者当前的借阅情况. 则首先用Z语言分别描述图书管理系统的Book、Users、Database的基本模式，如图12~14所示.

图 12 Book模式 Figure 12 Z schema for the Book
图 13 Users模式 Figure 13 Z schema for the Users
图 14 Database模式 Figure 14 Z schema for the Database

系统日志记录方面的形式化描述如图15所示.

图 15 日志类模式 Figure 15 Log Class Model

则完整的初始化图书管理系统如图16所示.

图 16 图书管理系统的初始化 Figure 16 Z schema for the Initialization of Library management system

管理员新增图书的复本，包括新增复本属性，包括标题(title)、作者(author)和主题(subjects)，如图17所示.

图 17 AddBook模式 Figure 17 Z schema for the AddBook

在本系统中对非功能需求的系统日志建立方面. 系统日志记录着系统运行的每一个细节，并记录系统中硬件、软件和系统问题的信息，对系统的稳定运行起着至关重要的作用. 建立的系统日志的方面模式如图18所示.

图 18 日志方面模式 Figure 18 Aspect-Z aspect-schema for Log

在系统的操作中，为了确定操作的执行与否，对于操作的成功或者失败给予提示，在此也可将此信息提示建立方面，方面模式如图19所示.

图 19 信息提示方面模式 Figure 19 Aspect-Z aspect-schema for Message

在本实例中主要是对日志方面和操作的信息反馈进行横切，其中Composition表示横切规则，来说明在连接点处进行方面编织时LogAspect方面的优先级高于AspectMessage方面，对日志记录的成功与否进行反馈. 定义的优先级如图20所示.

图 20 方面的优先级定义 Figure 20 The Priority definition of Aspect-Z

将方面模块织入之后的新增图书集成模块Integerated如图21所示.

图 21 Aspect-Z的集成模式 Figure 21 Aspect-Z integrated schema
4.3 形式化验证方法

当使用形式化规格说明之后，为了保证本文描述过程的正确性，通过定理证明的方法[16]来验证规格说明的一些性质是否满足需求，如果满足，说明描述的这一部分是合理的，反之则不合理. 形式验证方法主要有3种，分别是对初始状态存在验证、前后置条件验证和推理操作的性质验证. 由于篇幅有限，本文主要对初始状态存在进行如下验证.

 

在Aspect-Z中，初始状态用一个Init模式表示. 完成一个形式化规格说明之后，必须验证其初始状态的存在. 则表达式为

Context├∃ x:X·Invariant(x)∧Init(x).

Context表示包括全局变量、局部类型、函数及常量定义等的上下文环境. x:X是类中定义的状态变量x及相应的类型X. Invariant(x)表示状态变量的不变式. Init(x)表示相应的状态变量的初始变量.

在本实例中，初始状态的上下文环境为

Context=[Users∷=Registrar|Readar;Book⊇Title∪Author∪Subject; Registrar≠ $\phi $ ; Reader≠ $\phi $ ; Stock= $\phi $ |0‥maxbooks;Available= $\phi $ |0‥maxbooks; Checked_out= $\phi $ |0‥maxbooks;Available∪Checked_out=maxbooks;]. 因此只需验证

Context├∃Registrar, Reader∶Users;Title, Author, Subject:Book;stock:Stock; available:Available; checked_out:Checked_out·registrar≠ $\phi $ ∧reader ≠ $\phi $ ∧stock=maxbooks∧available=maxbooks∧checked_out= $\phi $ ∧book_info= $\phi $

利用点规则化简可得

Context├Registrar≠ $\phi $ ∧Reader≠ $\phi $ ∧maxbooks∈Stock∧maxbooks∈Available∧ $\phi $ ∈Checked_out∧ $\phi $ ∈book_info.

由状态变量和给定类型有

Registrar≠ $\phi $ ，Reader≠ $\phi $ ，maxbooks∈Stock，maxbooks∈Available， $\phi $ ∈Checked_out， $\phi $ ∈book_info，即有Context├true, 故初始状态存在.

5 结束语

本文主要研究和讨论的是通过采用AOP技术对软件系统的需求分析进行研究，它将系统功能的非功能需求横切并建立为方面，提高了需求分析中非功能需求的模块性和可维护性. 通过采用针对面向方面的形式化语言Aspect-Z与AOP技术相结合，更能够清晰、精确、抽象、简明规范地描述软件的系统需求，极大地提高了软件的安全性和可靠性. 本文充分利用Aspect-Z语言，对系统日志和系统信息提示进行方面的模块化，并通过定义优先级来解决方面之间可能出现的冲突. 最后通过形式化验证方法，对系统实例的初始状态进行验证，确保描述过程和属性本身的正确性. 对于系统的需求分析来说，本文的其他地方还需要进一步的研究，例如系统非功能性需求的可靠性、效率和基于Aspect-Z的面向方面的多维横切形式化问题，在后续会进一步探讨.

参考文献
[1] ZHANG L, HUB M, MANG S, et al. Software for quantitative analysis of radio therapy: overview, requirement analysis and design solutions[J]. Computer Methods and Programs in Biomedicine, 2013, 110(3): 528-537. DOI: 10.1016/j.cmpb.2013.03.002.
[2] GORGAN V. Requirement analysis for a higher education decision support system. Evidence from a Romanian University[J]. Procedia Social and Behavioral Sciences, 2015, 197: 450-455. DOI: 10.1016/j.sbspro.2015.07.165.
[3] KESHAV B A, GOPALAKRISHNAN N T R. Mapping general system characteristics to non- functional requirements[C]//Proceedings of the 2009 IEEE International Advance Computing Conference. [S.l.]: IEEE, 2009: 1634-1638.
[4] 袁仕继, 许世平, 杜松蒲, 等. 一种软件需求规格说明描述质量评价方法[J]. 电子设计工程, 2013, 21(7): 11-13.
YUAN S J, XU S P, DU S P, et al. A method based software requirements specification description quality evaluation[J]. Electronic Design Engineering, 2013, 21(7): 11-13.
[5] 金英, 刘华虓, 张鹏. 一种面向方面需求模型的分析与验证方法[J]. 计算机学报, 2013, 36(1): 63-73.
JIN Y, LIU H B, ZHANG P. An approach to analysis and verifying aspect-oriented requirements model[J]. Chinese Journal of Computers, 2013, 36(1): 63-73.
[6] 金望正, 李莹, 徐江浩, 等. 面向方面编程技术研究[J]. 计算机应用与软件, 2005, 22(8): 42-45.
JIN W Z, LI Y, XU J H, et al. Research on aspect-oriented programming technology[J]. Application and Software, 2005, 22(8): 42-45.
[7] 王书怀, 邢建春, 李决龙, 等. AOP技术在信息管理系统中的应用研究[J]. 计算机应用与软件, 2012, 29(6): 189-195.
WANG S H, XING J C, LI J L, et al. Application research of AOP technology in information management system[J]. Computer Application and Software, 2012, 29(6): 189-195.
[8] CAO F, BRYANT B R, BURT C C, et al. A component assembly approach based on aspect-oriented generative domain modeling[J]. Electronic Notes in Theoretical Computer Science, 2005, 114: 119-136. DOI: 10.1016/j.entcs.2004.02.070.
[9] 姚全珠, 王江. 基于UML的软件形式化需求分析与验证[J]. 计算机工程, 2010, 36(13): 30-33.
YAO Q Z, WANG J. Software formalization requirements analysis and verification based onUML[J]. Computer Engineering, 2010, 36(13): 30-33. DOI: 10.3969/j.issn.1000-3428.2010.13.011.
[10] 刘敬勇, 钟勇, 张立臣. 软件非功能需求的面向方面建模[J]. 计算机应用与软件, 2010, 27(12): 40-41.
LIU J Y, ZHONG Y, ZHANG L C. The aspect-oriented modelling of software non-functional requirements[J]. Computer Application and Software, 2010, 27(12): 40-41.
[11] ZHANG L. Aspect-oriented formal techniques of cyber physical systems[J]. Journal of Software, 2012, 7(4): 823-834.
[12] SILVA C V, SAENS R, DEL R C, et al. Aspect-oriented modeling: applying aspect-oriented U-ML use cases and extending aspectZ[J]. Computing and Informatics, 2013, 32(3): 1001-1021.
[13] FABRY J, KELLENS A, DENIER S, et al. Aspectmaps: extending moose to visualize AOP software[J]. Science of Computer Programming, 2014, 79(1): 6-22.
[14] YU H, LIU D, YANG L, et al. Formal aspect-oriented modeling and analysis by aspect-Z[C]//International Conference on Software Engineering and Knowledge Engineering. [S.l.]:[s.n.], 2005: 169-174.
[15] ZIELCZYNSKI P. Requirements management using ibm® rational® requisitepro®[M]. New York: IBM Press, 2007.
[16] 文志诚, 缪淮扣, 张新林. 基于Object-Z的形式化验证方法[J]. 计算机科学, 2007, 34(5): 247-251.
WEN Z C, LIAO H K, ZHANG X L. Formal verification based on object-Z specification[J]. Computer Science, 2007, 34(5): 247-251.