（计算机软件与理论专业论文）基于运行时验证的aop程序检测框架研究.pdf

兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 摘要 面向对象编程( o b j e c t o r i e n t e dp r o g r a m m i n g ，o o p ) 是一种实现软件模块 化和可重用的编程规范，较好地解决对象和数据的封装问题。但是随着编程实 践的日益丰富，o o p 也表现出缺陷：在加入横切关注之后的代码容易产生交织、 分散问题，使得代码难以理解和维护。面向切面编程( a s p e c t o r i e n t e d p r o g r a m m i n g ，a o p ) 方法应运而生，为上述问题提供了一种有效和可行的方法： a o p 支持软件模块化和可重用，能有效地消除代码的交织和分散问题。a o p 将 程序被描述成对象和切面的集合，通过织入器把切面织入到程序中。由于切面 如何描述在很大程度上影响到系统的关键行为( 比如性能和同步) ，与此同时， 系统的关键行为使得切面的描述复杂化，b u g s 可能存在于程序中而难以发觉。 因此a o p 程序的验证工作相对复杂。我们需要一种方法来测试或验证a o p 程 序的正确性。 目前对a o p 的研究侧重于语言本身的实现和应用，而对程序进行检查和验 证的相关研究十分缺乏。针对目前的需求，本文提出一种基于运行时验证的框 架来检测a o p 程序，使得a o p 程序中横切关注点的验证得以实现。在这种框 架中，程序的性质由线性时序逻辑公式描述，并在程序执行时使用运行时验证 技术来验证。本文给出该框架的整体流程和核心算法，并使用一个详细的案例 对研究内容进行分析介绍。 关键词：面向切面编程，运行时验证，模型检测，连接点，线性时序逻辑， 注解。 兰州大学硕士研究生毕业论文 基于运行时验证的a o p 程序检测框架研究 a b s t r a c t o b j e c t - o r i e n t e dp r o g r a m m i n g ( o o p ) i sap r o g r a m m i n gc r i t e r i af o rs o f t w a r e m o d u l a r i z a t i o na n dc o d er e u s e o o pi sav e r yg o o ds o l u t i o nt ot h ed a t aa n do b j e c t e n c a p s u l a t i o n s h o w e v e r ，w i t h t h er a p i d d e v e l o p m e n to ft h ep r o g r a m m i n g m e t h o d o l o g y , a d d i n gc r o s s c u t t i n gc o n c e r n ss u c ha so p t i m i z a t i o n st e n d st oc a u s e t a n g l i n ga n ds c a t t e r i n go fo p t i m i z i n gc o d eo v e rap r o g r a m c o n s e q u e n t l y , i ti s d i f f i c u l t t ou n d e r s t a n d t h ec o d e sa n dm a i n t a i n p r o g r a m s a s p e c t - o r i e n t e d p r o g r a m m i n g ( a o p ) i sp r o p o s e dt oa l l e v i a t et h i sp r o b l e ma n dp r o v i d e sa ne f f e c t i v e a n df e a s i b l em e t h o d m o r e o v e r , a o ps u p p o r t sr e u s ea n dm o d u l a r i t yo fc o d e ，w h i c h e l i m i n a t ec o d et a n g l i n ga n ds c a t t e r i n g w i t ha o p , p r o g r a md e s c r i p t i o n sa r ed i v i d e d i n t oo b j e c t sa n da s p e c t s ac o m p i l e r , c a l l e daw e a v e r , w e a v e sa s p e c t sa n do b j e c t s t o g e t h e ri n t oo n ep r o g r a m h o w e v e li t i s n o te a s yt ov e r i f yt h ec o r r e c t n e s so fa w o v e np r o g r a mb e c a u s ec r u c i a lb e h a v i o r si n c l u d i n gp e r f o r m a n c ea n ds y n c h r o n i z a t i o n a r es t r o n g l yi n f l u e n c e db ya s p e c td e s c r i p t i o n s b u g st e n dt ob ee m b e d d e di na s p e c t s t h a tm a yh a v ec o m p l e xs t r u c t u r e st od e s c r i b ec r u c i a lb e h a v i o r s i no r d e rt os o l v es u c h p r o b l e m s ，a na u t o m a t i cv e r i f i c a t i o na p p r o a c hw i l lb eu s e dt oc h e c kw h e t h e raw o v e n p r o g r a mc o n t a i n su n e x p e c t e db e h a v i o r s t h ec u r r e n tr e s e a r c ho fa o ph a sf o c u s e do nt h el a n g u a g ei t s e l f , b u tt h e r ea r e q u i t eaf e wt e c h n i q u e st h a tp r o v i d es p e c i f i c a t i o nc h e c k i n ga n dv e d f i c a t i o n t os o l v e t h ep r o b l e ml i s t e da b o v e ，t h i sp a p e rp r e s e n t saf r a m e w o r kb a s e do nt h er u n t i m e v e r i f i c a t i o nt e c h n i q u et ov e r i 矽t h ea o p p r o g r a m sa n de n a b l e st h ev e r i f i c a t i o n0 n c r o s s - c u t t i n gc o n c e r n so fa o pp r o g r a m s i nt h i sf r a m e w o r k , t h es p e c i f i c a t i o no fa p r o g r a m i sd e s c r i b e db yl i n e a r t e m p o r a ll o g i cf o r m u l a e ，a n dt h er u n t i m e v e r i f i c a t i o no ft e m p o r a lp r o p e r t i e so c c u r sw h i l et h ei m p l e m e n t a t i o np r o c e d u r eo ft h e p r o g r a m w ed e s i g nt h ew h o l ef l o w c h a r t , s t r u c t u r ea n dt h ec o r ea l g o r i t h m sa n da d e t a i l e dc a s es t u d yw i l lb ea l s op r o v i d e dt oi n t r o d u c et h er e l a t e dr e s e a r c ht o p i c s 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 k e y w o r d s ：r u n t i m ev e r i f i c a t i o n ；a s p e c t - o r i e n t e dp r o g r a m m i n g ；m o d e l c h e c k i n g ；j o i np o i n t ；l i n e a rt e m p o r a ll o g i c ；a n n o t a t i o n i i i 原创性声明 本人郑重声明：本人所呈交的学位论文，是在导师的指导下独立 进行研究所取得的成果。学位论文中凡引用他人己经发表或未发 表的成果、数据、观点等，均己明确注明出处。除文中已经注明 引用的内容外，不包含任何其他个人或集体已经发表或撰写过的科研 成果。对本文的研究成果做出重要贡献的个人和集体，均己在文中以 明确方式标明。 本声明的法律责任由本人承担。 论文作者签名：翌盎 e l 期：论文作者签名：签盆期： 关于学位论文使用授权的声明 本人在导师指导下所完成的论文及相关的职务作品，知识产权归 属兰州大学。本人完全了解兰州大学有关保存、使用学位论文的规定， 同意学校保存或向国家有关部门或机构送交论文的纸质版和电子版， 允许论文被查阅和借阅；本人授权兰州大学可以将本学位论文的全部 或部分内容编入有关数据库进行检索，可以采用任何复制手段保存和 汇编本学位论文。本人离校后发表、使用学位论文或与该论文直接相 关的学术论文或成果时，第一署名单位仍然为兰州大学。 保密论文在解密后应遵守此规定。 论文作者签名：坚宝 导师签名： 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 1 1 研究背景 第一章绪论 面向对象编程( o b j e c t o r i e n t e dp r o g r a m m i n g ，o o p ) 是一种实现软件模块 化和可重用的编程规范。o o p 很好地解决对象的数据和封装问题。但是随着编 程实践的日益丰富和对开发认识的不断深入，o o p 也出现问题：程序中经常出 现几个紧密相关的模块的行为，它们分散在各个模块之间，具有多个类的功能， 比如日志记录、事务管理、安全性等。开发人员通常无法将它们集中在一个类 中进行处理。我们将这些模块称为系统的横切关注点( c r o s s c u t t i n gc o n c e r n s ) 。 横切关注点无法在o o p 编程中进行合适地描述，因此无法将各个模块完成相似 功能的代码进行分离，从而形成分散而纠缠的代码( s c a t t e r e da n dt a n g l i n gc o d e ) ， 并且这导致代码无法重用，可维护性差且产生大量代码冗余。 面向切面编程( a s p e c t - o r i e n t e dp r o g r a m m i n g ，a o p ) 方法的出现为解决上 述问题作出了重要贡献。在1 9 9 7 年，它由美国施乐的p a l o a l t o 研究中心( x e r o x p a r c ) 的g r e g o e rk i c z a l e s 等人在实践的基础上于提出i l ，2 1 。在a o p 中，程序被描 述成包括对象( o b j e c t ) 和切面( a s p e c t ) 的集合。切面就是多个对象都要实现的 操作，比如权限检查、日志记录、安全功能等。系统要访问对象都要经过这个 切面作出相应的处理，处理的过程我们称为通知( a d v i c e ) 。使用切面可以减少 对这些公用代码的重复编写，能够提高编程的效率。在a o p 中一般是使用静态 或动态织入技术将横切关注点自动注入到系统中，从而可以实现对横切关注点 的封装和集中管理。a o p 织入器( w e a v e r ) 能够自动将这些横切关注点织入到系 统中，使最后得到的代码体现出核心关注和横切关注共同组合而成的行为。在 使用a o p 设计开发的系统中，开发人员只需集中精力实现程序的核心业务逻辑 和横切关注点。因此，我们说面向对象程序设计实现了对核心关注点的封装和 重用，而面向切面程序设计则实现了对横切关注点的封装和集中管理。 随着a o p 技术的发展，目前出现了多种a o p 的实现。比较著名的有a s p e c t j 【3 j 、 s p r i n g a o p l 4 、j b o s s a o p t 5 1 、a s p e c t w e r k z l 6 1 等。每种编译器使用不同的策略和技 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 术实现其织入器。随着更多的系统开发使用a o p 技术，其复杂度不断增大，因 此开发人员难以预澳i j a o p 程序的执行流程，这样b u g s 有可能存在于程序中而不 易察觉。 许多软件开发者使用断言来验证程序执行路径上的某个状态是否满足给定 的约束条件。但是这种约束条件一般用于限制某个变量的取值范围，或者测试 该变量的取值是否落于某个区间。使用断言的另一个缺点是无法对程序执行路 径上的多个连续状态进行描述和推理。 另外一种常用的验证方法是模型检测。很多学者的研究着重于使用模型检 测技术来检测系统是否符合一定的性质规范。模型检测固然有很多优点，但是 仍然有其不足之处：要验证系统所有可执行的路径，其算法的复杂度是随着系 统的状态进行指数级的增长。而且对于一般软件开发者来说，模型检测技术过 于复杂。 为了克服上述缺点，我们需要一种轻量级的、高效的检测方案来对a o p 程 序进行验证。 1 2 相关研究 面向切面编程是一种全新的编程模式，目前仍然处于研究和发展阶段，所 以并不是所有a o p 工具都足够成熟并适用于商业开发。虽然开发者对a o p 投 入了前所未有的研究热情，但是这些研究往往侧重于a o p 语言本身的实现和应 用，很少涉及对a o p 程序的检查和验证，对此进行的研究也相对缺乏。尽管如 此，许多学者在程序验证的研究还是为我们的课题提供了有力的理论支持和有 益的启发。 ( 1 ) d h l o r e n z 和t s k o t i n i o t i s 【7 8 】等人在这个方面进行了一些早期的工 作。他们在面向切面的程序设计中引入了契约式设计【7 】( d e s i g nb yc o n t r a c t ， d b c ) 的思想。他们对a s p e c t j 程序的执行过程进行了分析，并在此基础上定义 了通知( a d v i c e ) 所应遵守的契约并提出了契约的实现思路。 ( 2 ) n u b a y a s h i 和t t a 啪a i 【9 】对通过使用模型检测( m o d e lc h e c k i n g ) 技术 来验证a o p 程序的方法进行初步讨论：他们将模型检测技术应用在织入过程完 成后的切面和类，同时提出了一个基于a o p 的模型检测框架。在这里，他们将 2 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 需要检测的性质放在到一个预先定义的切面( a s p e c t ) 中，并利用这个切面来进 行检测。 ( 3 ) j i a n j t i nz h a o 和m a r t i nc r i n a r 为a s p e c u 设计出p i p a 语言，这为验证 o o p 程序提供一种形式化的规格语言的支持。这一点对于程序的检查和验证是 不可或缺的。正如a s p e c t j 对j a v a 进行扩展来实现对a o p i 拘支持一样，p i p a 语言采 用了同样的策略对j m l 进行了面向切面的无缝扩展。p i p a i j i 入了少量新的语言结 构来实现对a o p 的支持。p i p a 对切面，通知( a d v i c e ) ，切面不变量( a s p e c t i n v a r i a n t ) ，引介( i n t r o d u c t i o n ) 提供了比较完善的规格机制，p i p a 还对切面的继 承和横切提供了支持。 ( 5 ) w a n gy i 和z h a oj i a n j u n t l l 名e j i a n j u nz h a o 并b m a r t i nc r i n a r 研究基础上为 p i p a 语言引入了少量新的语言结构来实现对a s p e c t j 的支持，使得p i p a 支持a o p 程 序的验证。由- 于a s p e c t j 的复杂性，且p i p a 尚未成熟，使得p i p a 的实现相对复杂， 而_ h p i p a 缺少对程序时序相关性( t e m p o r a li n t e r d e p e n d e n c i e s ) 的描述。 ( 6 ) s s h i n o t s u k a t 眨1 等人提出了c o w 语言。该语言可以用来描述在织入过 程中所应遵守的织入约束，c o w 语言描述了由织入过程的前置条件和后置条件 所构成的织入契约。通过对契约进行基于谓词逻辑的验证，就可以判断织入过 程的正确性，以提高系统整体的可靠性。 ( 7 ) e b o d d e n 1 3 1 提出一种针对j a v a 程序的运行时验证( r u n t i m e v e r i f i c a t i o n ) 【1 4 ，1 5 1 框架。他们在j a v a 程序的注解( a n n o t a t i o n ) 里使用线性时序 逻辑( l i n e a rt e m p o r a ll o g i c ，l t l ) 公式来刻画程序性质，并通过b t i c h i 自动机 对l t l 公式进行建模，即将u l 公式转化为确定性b i a c h i 自动机，并使用运行时验 证技术来验证j a v a 程序。 1 3 本文主要工作 上述学者的工作为我们提供了有意地启发：可以使用一种形式化的方法用 于程序验证当中；程序性质的刻画可以通过契约或者时序逻辑来完成。这些都 为我们的工作奠定了基础。本文所做的主要工作是将e b o d d e n1 1 3 】提出的j a v a 程 序验证框架运用到a o p 程序检测中，从而实现对a o p 程序的运行时刻的验证及 检查。在这个框架中，程序的注解部分使用l 1 乙公式刻画a o p 程序的时序性质， 3 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 然后将程序编译成字节码，通过预处理器将l t l 公式转换成相应的验证代码，这 些代码由切面描述，并织入到字节码中，最后在程序运行时进行验证性质刻画 是否符合m 公式的描述。 使用该框架检测a o p 程序有以下优点；不需要程序测试人员具备建立和验 证严格数学模型的能力，又能避免出现模型检测中的状态空间爆炸问题；在注 解中书写l t l 公式符合程序的书写规范，易于理解，能提高软件质量。该框架 的创新之处在于将时序逻辑和a o p 结合的运行时验证技术应用到验证a o p 程 序中。 本文涉及到的研究内容包括： ( 1 ) 对a o p 常用的语法以及a o p 织入机制的介绍。 ( 2 ) 对运行时验证的研究。 ( 3 ) 对线性时序逻辑以及交替自动机在运行时验证的环境中如何使用的研 究。 ( 4 ) 设计一个针对a s p e c t j 的运行时研究框架。 1 4 本文组织结构 本文共分为以下六个章节： 本章介绍了该课题的研究背景、其他学者的相关工作。然后介绍了本文的 主要工作。 本文第二章介绍a o p 语言的相关概念，包括其背景，语言核心概念及a o p 织入的实现机制。 第三章介绍运行时验证技术的背景和及其相关理论，并将运行时验证和模 型检测、软件测试进行了初步地比较。 第四章引入本文的理论基础一一u 1 l 和自动机的相关理论。这里介绍的是 他们的经典定义，即在模型检测中各自的定义。在l t l 部分，我们介绍了m 的语义、语法和n n f 范式；在有限状态自动机部分，介绍了n f a 、d f a 的定义 以及n f a 到d f a 的幂集构造算法；在无限状态自动机部分，介绍了b t i c h i 自动 机的各种定义以及交替自动机的定义；最后介绍在模型检测中如何将l 1 l 转换 为b i i c h i 自动机。 4 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 第五章提出了使用运行时验证技术检测a o p 程序的方法。我们以模型检测 中u l 和自动机理论为基础，给出了适合于有限状态路径上的m 语义，介绍 了l 1 乙转换成交替自动机的算法。有了这些理论基础，就可以将验证相关的算 法用功能等价的切面实现。 第六章对全文进行总结和展望，提出了本文的不足之处以及今后的研究方 向。 5 兰州大学硕士研究生毕业论文基丁二运行时验证的a o p 程序检测框架研究 第二章a o p 语言及其实现机制 2 1a o p 产生的背景 2 1 1 传统编程方法学面临的问题 当前，人们广泛使用的是面向对象编程( o b j e c t - o r i e n t e dp r o g r a m m i n g ，o o p ) 的编程思想和技术。0 0 ( o b j e c t o r i e n t e d ) 是对现实世界抽象层次不断发展和提 高的结果。它将系统看成一组相互协作的对象，通过包、类、方法等概念来组 织系统，方法被定义在类中，而类被组织在包里。这种封装性、层次性能更好 地描述现实世界，也更符合人们的认识习惯，因此，0 0 的思想一经提出就得到 了各界广泛地支持和深入地发展。同时，o o p 在代码的可重用性、可维护性等 方面都有着突出的优点。当前，许多大型软件的开发和设计均采用o o p 。但o o p 也产生了以下两个问题： ( 1 ) 代码交织( c o d et a n g l i n g ) ：一个软件系统的模块可能同时与数个需求 交互。 ( 2 ) 代码分散( c o d es c a t t e r i n g ) ：由于横切关注点跨越多个模块，所以与 这些横切关注点相关的实现代码也跨越所有这些模块。 由于以上这些问题的存在，就需要研究一种全新的程序设计方法，以从更 高的层次上对软件系统进行抽象，将传统的按功能或按对象划分程序模块的方 法转化为按系统关注点来划分程序模块的方法，这就是a o p 的基本思想。 2 1 2a o p 的产生 在1 9 9 7 年的欧洲面向对象编程大会( e c o o p 9 7 ) 上，施乐公司的p a l o a l t o 首席科学家、大不列颠哥伦比亚大学教授g r e g o rk i c z a l e s 等人首次提出了a o p 的 概斜1 1 ，a o p 从编程方法学的角度对横切关注点问题进行了有效地解决。此后， 在每年的e c o o p 上都有与a o p 相关的专题研讨会，各大公司、大学和研究机构 也纷纷投入人员进行研究。 6 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 2 2a o p 核心概念 a o p 思想的本质是用一种松散耦合的方式来实现独立的关注点，通过组合 这些关注点来建立最终的系统。a o p 构筑在现有的编程技术o o p 之上，同时赋 予这些技术一些新的概念和元素。a o p 围绕着下述相关概念： 2 2 1 横切 横切就是对织入规则的实现。在a s p e c t j 中提供两类横切类型： ( 1 ) 第一类是对己有的j a v a 对象类型，改变其功能或者结构，比如增加类 的数据成员。这类横切称为静态横切( s t a t i cc r o s s c u t t i n g ) 。 ( 2 ) 第二类是在某些明确定义的程序执行点上，定义附加操作或者是允许 条件。这类横切称为动态横切( d y n a m i cc r o s s c u t t i n g ) 。动态横切非常类似于 c o r b a t l 6 】的拦截器( i n t e r c e p t o r ) ，其功能是在执行程序中的特定点拦截并获得 控制权。 2 2 2 核心关注点和横切关注点 关注点( c o n c e r n ) 是软件设计中经常触及的重要概念。一般而言，可以把 关注点理解为满足用户需求、关系软件实现的事项；或者说一个关注点就是一 个软件需要解决的问题。 软件开发最重要的步骤是鉴别关注点和分离关注点。使用“横切”技术， a o p 把软件系统分为两个部分：核心关注点和横切关注点。业务处理的主要流 程是核心关注点，即软件所要实现的主要功能和目标。与核心关注点有横切作 用的是横切关注点。横切关注点的一个特点是，他们经常发生在核心关注点的 多处，而功能都基本相似。比如权限认证、日志、事务处理就是常见的横切关 注点。 2 2 3 切面 a o p 将多个核心业务模块中完成相似功能的代码抽取出来并进行模块化， 这些模块称为切面( a s p e c t ) 。切面和对象有如下不同：对象的主要功能是访问 7 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 数据对象，并进行相应的操作。面切面是系统的一个纵向切面，涉及到许多类 和方法。图2 1 是切面和对象的对比示意图： 场獭 2 2 4 连接点和切点 图2 1 切面和对象的对比 定义在应用程序流程某处用于执行切面的地方称为连接点。连接点是代码 中激活通知( a d v i c e ) ，使得通知代码得以执行的触发点。 而切点就是一组连接点的集合。一旦捕获到连接点，可以指定与这些连接 点相关的织入规则，比如在执行连接点之前或者之后采取一定的动作。 2 2 5 通知 通知实际上就是一种处理逻辑，为程序定义了新的行为。它由切点和通知 代码组成。通知类似于事件处理机制的a c t i o n ：当应用程序到达匹配到的连接点 处时，切面将执行通知中定义的逻辑行为，并将这个通知行为插入在调用者和 被调用者之间。通知主要有在连接点执行之前执行( b e f o r ea d v i c e ) 、在连接点执 行之后执行( a f t e ra d v i c e ) 和代替连接点处的执行( a r o u n da d v i c e ) 三种。 8 兰州大学硕士研究生毕业论文 基于运行时验证的a o p 程序检测框架研究 2 2 6 织入 为了有效地开发整个a o p 系统，必须将核心关注点和切面合二为一。a o p 提供一种将核心关注点和切面的自动合并的机制，也就是将两类关注点转换为 可执行的形式。通常这一合并过程被称为织入( w e a v i n g ) 。 织入是实现a o p 的关键，它拦截正常的方法调用，将需要额外附加的功能 透明地织入到这些方法中，以完成一些额外的需要。织入的规则说明了在程序 执行到某个点时，需要采取的行动。使用这些规则可以将横切关注点的实现织 入到核心业务逻辑中。a o p 的织入分为静态织入与动态织入两种：前者指在业 务代码运行前，相应的切面代码插入到业务代码的适当位置，形成最终运行需 要的代码；后者指业务代码运行时插入相应的切面代码。由于织入方式可以是 静态的也可以是动态的，这也正是目前各个a o p 规范实现的主要差异。 2 。3a o p 织入实现机制 目前a o p 有多种不同的实现。有针对c 语言i 拘a s p e c t c 1 7 】；针对c + + 语言的 a s p e c t c + + t l s ；针对j a v a 语言的a s p e c t j 、a s p e c t w e r k z 、j b o s sa o p 和s p r i n ga o p 等。本文主要针对j a v a 的a s p e c o 来展开说明。 所有的计算机程序语言在成为可执行形式之前要经过编译或解释，a o p 程 序也不例外。a o p 程序要能在j a v a 平台上正确执行必须经过a o p 工具进行相 应的处理将其转换成j a v a 编译器能识别的形式。在a o p 工具中，一般是由切面 织入器( a s p e c tw e a v e r ) 来处理织入的过程：按照切面中连接点指定的方式自动 调用相应的通知。一般来说，切面织入器可以接受源代码或二进制形式的a o p 代码。图2 2 是a o p 织入过程的示意图： 图2 2 a o p 的织入实现 从上图我们可以看到，a o p 织入的实现流程可分为以下三步： 9 兰州大学硕士研究生毕业论文 基于运行时验证的a o p 程序检测框架研究 ( 1 ) 核心模块分解和实现一这里使用传统程序设计技术，将需求划分为 多个核心关注点。核心关注点实现为类。 ( 2 ) 切面分解和实现根据第一步核心模块的设计，分析系统级需求， 确定各个横切关注点。在这里开发者将定义、设计以及实现切面。 ( 3 ) 切面织入一通过使用a o p 的织入器，将横切关注点模块织入到核 心关注点模块中的适当位置，以生成最终系统。 2 4a s p e c t j 简介 在x e r o xp a l oa l t o 研发中心成立之后，a o p 才算是真正步入发展的正规， 它标志着计算机业的一次革命。x e r o x 初期专注于开发专用的面向切面语言，随 后转为针对j a v a 开发通用模型，因此a s p e c t j 随之应运而生。a s p e c t j 是第一个 a o p 的实现，于2 0 0 2 年底被捐献给开放源码组织e c l i p s e 。以下是a s p e c t j 的特 点： ( 1 ) a s p e c t j 对j a v a 语言进行了扩展，通过引入切面、连接点、通知等基 本元素，使其成为面向切面编程语言。 ( 2 ) a s p e c t j 是j a v a 语言的超集，所有合法的j a v a 程序都是一个合法的 a s p e c t j 程序。a s p e c t j 生成的标准j a v a 类文件可以在任何j a v a 虚拟机上运行。 2 5j a v a5 注解 注解( a n n o t a t i o n ) ，也称为元数据( m e t a d a t a ) ，在j s r 1 7 5 规范中提出。 注解是添：i i i ! i 程序元素如方法、字段、类和包上的额外信息，通常用于文档编 制，编译器检查和代码分析。该机制允许在j a v a 代码中添加自定义注释，并允 许通过反射( r e n e c t i o n ) ，以编程方式访问注解。注解允许开发人员不用修改核 心语言的语义，就能够在j a v a 中添加新功能。此外，注解能编译进j a v a 字节码 中，可以更好地被其它第三方工具来处理。 每一个注解都有一个对应的注解类型。为了使用一个注解类型，开发人员 必须先声明该注解( 使用 i n t e r f a c e 来声明) 。为了使用同一类具有相同性质的 注解，可以声明一个注解类型的接口。注解类型还可以嵌套使用：在一个注解 l o 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 类型中声明新的注解类型。 例如下面就是一个注解类型的声明： p u b l i c i n t e r f a c et r a f f i c l i g h t p u b l i ce u u mc o l o r r e d , g r e e n ，y e l l o w ) ； s t r i n gn a m e ( ) ； c o l o rc o l o r ( ) d e f a u l tc o l o r g r e e n ； ， 和对象一样，注解有相应的生存周期和使用范围。生存周期在注解里定义 为保持策略( r e t e n t i o np o l i c y ) ，它是实现注解的重要一环。根据数据在内存中 保持时间的长短，有三种类型的保持策略： ( 1 ) r u n t i m e ：一直保留数据，可以通过反射来访问。 ( 2 ) c l a s s ：数据保留在字节码中，无法在运行时访问。 ( 3 ) s o u r c e ：编译器不保留该数据。 要使用保持策略，应在注解声明中加入如下类似语句： r e t e n t i o n ( v a l u e = x x x ) 使用范围在注解里定义为注释类型t a r g e t ，也就是注解类型所适用的程序元 素的种类。如果注释类型声明中不存在t a r g e t 元注释，则声明的类型可以用在 任一程序元素上。如果存在这样的元注释，则编译器强制实施指定的使用限制。 t a r g e t 的取值如下： a n n o t a t i o nt y p e ：注释类型声明。 c o n s t r u c t o r ：构造方法声明。 f i e l d ：字段声明( 包括枚举常量) 。 l o c a lv a r i a b l e ：局部变量声明。 m e t h o d ：方法声明。 p a c k a g e ：包声明。 p a r a m e t e r ：参数声明。 t y p e ：类、接口( 包括注释类型) 或枚举声明。 要使用注解类型，应在注解声明中加入如下类似语句： t a r g e t ( v a l u e = x x x ) 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 第三章运行时验证概述及验证方法 3 1 运行时验证产生的背景 长期以来，软件的正确性一直是计算机科学界和工业界最关注的问题之一。 自2 0 世纪6 0 年代起，就有很多计算机科学家对程序验证进行了研究，提出了 各种理论和方法。一般来说，测试和验证是保证软件质量的两种主要方法。软 件测试是为了发现程序中的错误而执行程序的过程，通过定义各种测试充分性， 可以提高我们对被测软件质量的信心，但无法回答系统一定没有错误这样一类 问题，因而无法从根本上确保系统的可靠性。而且测试在很多情况下都停留在 手工测试阶段。程序验证基于数学的形式化方法，揭示系统的不一致性、歧义 性和不完备性，可以从某一个角度回答系统一定没有错误这样一类问题。这要 求通过推理或者穷举的手段来判定程序的行为是否符合规约。由于要涵盖所有 可能情况，而程序设计语言的复杂性使得程序的复杂性随着程序尺寸的增大呈 指数级增长，同时证明任一程序正确与否本身是一个不可判定问题，因此程序 验证目前只用于证明一些关键的核心模块的正确性而没有得到更广泛的应用。 就目前而言，程序验证方法虽然可以保证软件质量，但是往往需要有一定经验 的用户花费相当多的时间，因而并不一定能提高软件的生产率。很多开发者， 研究人员都在如何保证软件的正确性和提高软件生产率上做出很多研究。 很多学者已经对形式化方法应用在验证计算机程序上作出了有实用价值的 相关研究：将形式逻辑( f o r m a ll o g i c ) 应用在计算机程序的分析以及设计方面； 为形式逻辑设计出一个语义框架，并证明计算机程序是否满足该逻辑。模型检 测( m o d e lc h e c k i n g ) 1 1 9 、定理证明( t h e r o e mp r o v i n g ) 【2 0 】都是比较常用的、重 量级( h e a v y w e i g h t ) 的形式化方法。模型检测的目的在于验证一个程序的所有 执行路径是否满足相应的性质。目前该领域的研究方向是将模型检测技术直接 应用在使用c 和j a v a l 2 1 ，2 2 】的程序上。但是模型检测也存在着不足：状态空间爆炸 就是一个众所周知的问题。虽然可以使用偏序规约( p a r t i a l o r d e rr e d u c t i o n ) 2 h 技 术来减少系统模型中的状态数目，从而降低模型检测算法所搜索的状态空间规 1 2 兰州大学硕士研究生毕业论文 基于运行时验证的a o p 程序检测框架研究 模。但是偏序规约技术仍然在研究之中，状态空间爆炸问题只能得到暂时缓解 而不能根本上解除。定理证明依赖于程序语义以及证明系统，用于验证程序在 所有可能输入的情况都能正常执行。不幸的是，这种技术无法全自动进行。 静态分析【2 3 】是一种软件测试技术。使用该技术不编译运行程序，而是通过 对程序源代码进行分析，根据程序的结构来确定程序的性质，然后发现其中的 错误。使用该技术，可以很好的控制程序规模，如果预计会出现的问题存在， 则保证能监测出错误。但是这种技术通常只能检测出有限的错误，比如死锁问 题和数组越界问题。有时该技术也会产生错误的结果。 针对上述的情况，学者希望使用一种轻量级( 1 i g h t w e i g h t ) 的形式化方法。 他们希望这种方法有如下特点： ( 1 ) 该方法在短期内是实际可操作的。 ( 2 ) 该方法能够自动完成。 ( 3 ) 该方法的复杂度和待验证程序的大小无关。 ( 4 ) 该方法具有可伸缩性( s c a l a b i l i t y ) ：能够应用在多种数量级( 比如百 万行或千万行) 的程序验证中。 目前，常见的轻量级的验证技术有程序监测( p r o g r a mm o n i t o r i n g ) 2 4 1 。其 思想是监测程序的执行路径。因为只有一条执行路径需要监测，相于模型检测 来说，这种方法所需要的代价相对较小。 3 。2 运行时验证概述 运行时验证是一种软件测试和形式化方法相互结合的方法【1 4 1 。运行时验证 是一种在程序执行时刻进行动态分析程序b u g s 的技术，是一种保证程序可靠性的 轻量化方法，其基本思想是收集程序运行中的相关信息并得到与程序相关的测 试或操作中的某些性质。它不会为程序建立严格的数学模型，它的主要关注点 在于程序的可执行性。对于一个给定的程序执行轨迹，它将断言转化为验证代 码，验证该轨迹是否满足程序规约。如不满足或违反该性质，则检查器应该给 出程序违反规范的结果。该技术可以用于部署、分发软件之前的测试，也可以 用于分发之后的软件检测。从本质上来说，运行时验证属于程序监测的范畴。 因此，这项技术易于开发入员学习和使用，并不需要他们具备丰富的数学 1 3 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 和逻辑知识。同时书写形式化的规格也对程序员明确实现思路大有裨益，也便 于他人理解代码，由此降低了软件的实现成本并且提高了软件质量。 运行时验证可以看作是契约式设计技术的一种自然扩展。契约式设计最早 由b m e y e r 2 5 】提出。契约式设计将面向对象程序中的类和其客户之间的关系看作 一种形式化的约定，该约定明确表示了各方的权利和职责。契约一般由前置条 件，后置条件和不变式构成，并将这些契约变成可执行的程序。这样，就可以 在程序执行时根据契约的值来判断系统中是否存在缺陷，以及缺陷发生在系统 中的那些位置，从而提高查错和维护的效率。我们可以看出，契约式设计在本 质上，也是一种运行时验证技术。 运行时验证技术在契约式设计技术的基础上计一步拓宽了概念和范畴。在 运行时验证技术中，并不仅仅将检查的对象局限在契约的范围内，而是通过规 格对程序行为进行详尽描述，将这些规格转变为可执行的代码，并通过这些代 码的执行来验证程序是否违反了它所应有的行为，从而发现系统的缺陷之所在。 3 3 运行时验证的执行流程 在运行时验证的框架中，性质刻画通常是由时序逻辑公式表示。而系统的 性质在程序运行时由具体的处理逻辑来验证。图3 1 描述了该流程： 翰入 远 i 配礁缓 l 中l ， 图3 1 运行时验证流程 从上图我们可以看到，运行时验证处理的是程序的输出部分，它不关注程 序的输入部分。我们可以对运行时验证的执行过程用一句话来描述：在程序运 行后，通过监测其运行状态来验证是否满足其性质刻画。 1 4 兰州大学硕士研究生毕业论文基于运行时验证的a o p 程序检测框架研究 3 4 运行时验证特点 运行时验证有如下特点： ( 1 ) 它收集信息的过程就是一个观察程序输出的过程。这个观察的过程非 常详细地记录程序的执行流程以及所涉及到数据。 ( 2 ) 程序执行时这个观察过程是被动的，也就是说程序无法干涉观察的进 程。 ( 3 ) 要验证被监测的系统是否满足性质需求( r e q u i r e m e n t s ) 。性质需求通 常是需要具有时序约束( t e m p o r a lc o n s t r a i n t s ) 性质的数学方法来表达。比如线 性时序逻辑公式( l i n e a rt e m p o r a ll o g i cf o r m u l a e ) ，自动机( a u t o m a t o n ) 和状态 转换图( s t a t ec h a r t s ) 。 ( 4 ) 运行时验证必需要在系统运行的过程中完成检测功能。它不会出现模 型检测中的状态空间爆炸问题