（计算机科学与技术专业论文）基于监控的可信软件构造技术研究与实现.pdf

国防科学技术大学研究生院学位论文 摘要 随着计算机技术的飞速发展，软件已经渗透到国民经济和国防建设的各个领 域并发挥着重要作用。然而，随着软件规模和复杂度的增加，软件失效和故障问 题日益加剧，极大的增加了软件维护和使用的代价，甚至影响用户对软件的信心。 如何在开发阶段提高软件可信性，确保软件的行为与预期相一致，已成为软件工 程领域的热点问题，研究可信软件构造技术具有重要的理论意义与应用价值。 可信软件的本质特征在于软件的行为与使用者的期望保持一致。对软件实施 有效的监控以获得软件的运行状态，并通过将监控结果与预期行为进行比较，可 以有效的掌握软件行为的可信程度，且有助于准确分析和定位软件故障。因此在 软件中以适当的方式注入监控能力，将是提升软件可信性的一种重要途径。但是 目前监控技术尚处于发展初期，在技术和实践方面还存在很多局限性，主要面临 监控需求表达能力不强、缺乏有效的监控编程模型、支持监控的平台和工具通用 性不够等亟待解决的问题。 针对上述问题，本文在深入研究监控技术的基础上，提出了基于监控的可信 软件构造模型t s c m ，并以此为基础设计实现了基于监控的可信软件开发环境 t s i d e 。t s i d e 能够借助源代码表示( s r c m l ) 技术和面向方面编程( a o p ) 技 术为软件注入监控能力，具有一定的通用性和可扩展性。本文主要研究工作包括 以下几个方面： ( 一) 分析了s r c m l 技术的基本原理，并且本文利用该技术辅助编程人员表 达监控需求。深入研究了a o p 技术的基本原理和若干关键技术，通过对a o p 典 型开发环境的分类和比较，本文选择a o p 开发环境x w e a v e r 作为实现监控能力注 入的支撑技术。 ( 二) 提出了基于监控的可信软件构造模型t s c m 。该模型由两部分组成： 源代码分析、监控需求表达、监控代码生成和监控代码织入模块组成第一部分， 各个模块松散耦合；支撑工具为第二部分，主要为其它模块功能的实现提供工具 和模板支持。t s c m 能够通过监控能力注入机制为软件注入监控能力，并以此为 基础通过软件运行监控机制提供软件运行的监控能力。 ( 三) 基于t s c m 模型，本文设计并实现了基于监控的可信软件开发环境 t s i d e 。t s i d e 能够图形化展现软件源代码信息，帮助编程人员表达监控需求，生 成a o p 监控代码，并在编程人员无需手动修改软件源代码的情况下将其织入软件 内部，为软件提供对进程、线程、函数和关键变量进行监控的能力。 在上述工作成果的基础上，本文使用一个生产者消费者程序对t s i d e 进行了 验证，结果表明：t s i d e 能够帮助编程人员输入监控需求，自动为该程序注入监 控能力，并在程序运行时对程序状态进行有效监控，初步验证了本文工作的可行 国防科学技术火学研究生院学位论文 国防科学技术大学研究生院学位论文 a bs t r a c t a l o n gw i t ht h er a p i dd e v e l o p m e n to fc o m p u t e rt e c h n o l o g y , s o f t w a r e h a s p e n e t r a t e d i n t ov a r i o u sd o m a i n so ft h en a t i o n a le c o n o m ya n dd e f e n s ea n dp l a y sa ni m p o r t a n tr o l e h o w e v e r , w i t ht h ei n c r e a s ei ns i z ea n dc o m p l e x i t y , s o f t w a r ef a i l u r e sa n d m a l f u n c t i o n s g r o w , w h i c hg r e a t l yi n c r e a s et h e c o s to fs o f t w a r em a i n t e n a n c e ，e v e na f f e c tu s e r s c o n f i d e n c ei ns o f t w a r e h o wt oi r e p r o v et h ec r e d i b i l i t yo fs o f t w a r ei nd e v e l o p m e n t p h a s et oe n s u r et h a tt h es o f t w a r ea c t si nl i n ew i t hu s e r s e x p e c t a t i o n s ，w h i c hh a s b e c o m e ah o ti s s u ei ns o f t w a r ee n g i n e e r i n gf i e l d t h u s ，i ti so fg r e a tt h e o r ym e a n i n ga n d p r a c t i c a lv a l u et om a k er e s e a r c h e so n c o n s t r u c t i o n so ft r u s t e ds o f t w a r e t h ec o n s i s t e n c eo fs o f t w a r e sb e h a v i o ra n du s e r s e x p e c t a t i o ni s t h ee s s e n t i a l f e a t u r eo ft h et r u s t e ds o f t w a r e t h r o u g ht h ei m p l e m e n t a t i o no fe f f e c t i v em o n i t o r i n gt o o b t a i ns o f t w a r e sr u n t i m es t a t e ，a n dc o m p a r i n gt h em o n i t o r i n gr e s u l t sw i t ht h ee x p e c t e d b e h a v i o r , w ec a ne f f e c t i v e l yi n c r e a s et h ec r e d i b i l i t yo fs o f t w a r e ，a n a l y z ea n dl o c a t e s o f t w a r ef a i l u r e sa c c u r a t e l y t h e r e f o r e ，i n j e c t i n gt h em o n i t o r i n gc a p a c i t yi n t os o f t w a r e i na na p p r o p r i a t ew a yw i l lb ea ni m p o r t a n ta p p r o a c ht oi m p r o v et h ec r e d i b i l i t yo f s o f t w a r e b u tt h ec u r r e n tm o n i t o r i n gt e c h n o l o g y i ss t i l li nt h ee a r l y s t a g e s o f d e v e l o p m e n t ，a n dt h e r e a r es t i l lm a n yt e c h n i c a la n dp r a c t i c a ll i m i t a t i o n s w ea r e c o n f r o n t e dw i t h i nm a n yc h a l l e n g e sd e s i d e r a t e dt ob es o l v e d ，s u c ha st h es i c km o n i t o r i n g r e q u i r e m e n t sd e s c r i b i n gc a p a b i l i t y , t h el a c ko f e f f e c t i v em o n i t o r i n gp r o g r a m m i n gm o d e l a n dt h et h el a c ko fu n i v e r s a lp l a t f o r ma n dt o o l sw h i c hs u p p o r tm o n i t o r i n g b a s e do ni n d e p t hs t u d yo ft h em o n i t o r i n gt e c h n i q u e ，t h i sp a p e rp r o p o s e sat r u s t e d s o f t w a r ec o n s t i t u t i o nm o d e lb a s e do nm o n i t o t i n g ( t s c m ) t os o l v et h i sp r o b l e m a n do n t h i sb a s e ，w ed e s i g na n di m p l e m e n tat r u s t e ds o f t w a r ei n t e g r a t i o nd e v e l o pe n v i r o n m e n t n a m e dt s i d e t s i d ei sa b l et oi n j e c tt h em o n i t o r i n gc a p a c i t yi n t os o f t w a r ew i t h s o u r c ec o d em a r k u pl a n g u a g e ( s r c m l ) t e c h n o l o g ya n da 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 ) t e c h n o l o g y , a n dh a sv e r s a t i l i t ya n ds c a l a b i l i t y n ec o n t e n to ft h i sp a p e r c a nb e g e n e r a l i z e da sf o l l o w s ： 1 i nt h i sp a p e r , w ea n a l y z et h eb a s i cp r i n c i p l e so fs r c m lt e c h n o l o g y , a n dw e u s e si tt oa s s i s tp r o g r a m m e r st od e s c r i b em o n i t o r i n gr e q u i r e m e n t s a n dt h e n ，w e i n d e p t hm a k er e s e a r c h e so nb a s i cp r i n c i p l e s o fa o pt e c h n o l o g ya n ds e v e r a lk e y t e c h n o l o g i e s t h r o u g hc l a s s i f i c a t i o n a n dc o m p a r i s o no ft y p i c a la o pd e v e l o p m e n t e n v i r o n m e n t ，w ec h o o s et h ea o pd e v e l o p m e n te n v i r o n m e n tx w e a v e ra st h eb a s e t e c h n o l o g yf o rt h er e a l i z a t i o no fm o n i t o r i n gc a p a b i l i t yi n j e c t i o n 2 w r ep r o p o s eat r u s t e ds o f t w a r ec o n s t i t u t i o nm o d e lb a s e do nm o n i t o r i n gn a m e d t s c m t i l i sm o d e lc o n s i s t so ft w oc o m p o n e n t s ：t h es o u r c ec o d ea n a l y s i sm o d u l e ，t h e m o n i t o r i n gr e q u i r e m e n td e s c r i p t i o nm o d u l e ，t h em o n i t o r i n gc o d eg e n e r a t i o n m o d u l ea n d t h em o n i t o r i n gc o d ew e a v i n gm o d u l ec o m p o s et h ef i r s tp a r t t h e s em o d u l e sa r el o o s e l y c o u p l e d 1 1 1 es u p p o r tt o o l sa r et h es e c o n dp a r t ，m a i n l yu s e d t op r o v i d es u p p o r tt o o l sa n d 围防科学技术大学研究生院学位论文 t e m p l a t e sf o r t h er e a l i z a t i o no fo t h e rf u n c t i o n a lm o d u l e s t s c mi n j e c t st h em o n i t o r i n g c a p a c i t yi n t os o f t w a r eb yt h em o n i t o r i n gc a p a c i t yi n je c t i n gm e c h a n i s m ，a n db a s e do n t h i s ，i tp r o v i d es o f t w a r er u n t i m em o n i t o r i n ga b i l i t yb yt h em o n i t o r i n gm e c h a n i s m 3 b a s e do nt s c mm o d e l ，w ed e s i g na n di m p l e m e n tat r u s t e ds o f t w a r ei n t e g r a t i o n d e v e l o pe n v i r o n m e n tn a m e dt s i d e t s i d ei sa b l et og r a p h i c a l l yd i s p l a ys o f t w a r e s o u r c ec o d ei n f o r m a t i o nt oh e l pp r o g r a m m e r st od e s c r i b em o n i t o r i n gr e q u i r e m e n t s ， p r o d u c tm o n i t o r i n ga o pc o d e ，a n dw e a v et h ec o d ei n t ot h ei n t e r i o ro fs o f t w a r ea st h e p r o g r a m m e r sd on o tm o d i f yt h e s o u r c ec o d em a n u a l l y , p r o v i d i n gt h em o n i t o r i n g c a p a b i l i t yt ot h es o f t w a r ep r o c e s so nt h r e a d s ，f u n c t i o n sa n dt h ek e yv a r i a b l e sl e v e l o nt h eb a s i so ft h ea b o v ew o r k ，t h i sp a p e ru s ea p r o d u c e ra n dc o n s u m e rp r o g r a m t o v e r i f yt s i d e ，t h et e s tr e s u l t ss h o wt h a tt s i d ec a nh e l pp r o g r a m m e r si n p u tc o n t r o l r e q u i r e m e n t ，a u t o m a t i c a l l yi n j e c tm o n i t o r i n gc a p a c i t yi n t ot h i sp r o g r a ma n de f f e c t i v e l y m o n i t o ri t sr u n n i n gs t a t e t h i sp r e l i m i n a r yv e r i f i e dt h ef e a s i b i l i t ya n de f f e c t i v e n e s so f t h i sp a p e r sw o r k k e y w o r d s ：c o n s t r u c t i o n so ft r u s t e ds o f t w a r e ，m o n i t o r i n g ，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 ，s o u r c ec o d ee x p r e s s i o n ，x w e a v e r i v 国防科学技术大学研究生院学位论文 表目录 表2 1w i n d o w s 多线程序示例1 1 表2 2 示例程序源码中间形式| 2 表2 3 实现监控的a s p e c t x 方面代码1 9 表2 4 插入了监控代码的多线程序源码2 0 表4 1 开发环境提供的监控功能31 表5 1 解析算法相关定义。4 6 表5 2x m l 文档解析算法4 7 表5 3 存放线程监控需求信息的链表4 8 表5 4 “t h r e a d d e m a n d 类4 8 表5 5 线程监控需求模板5 0 表5 6 线程监控探针模板51 表5 7 保存线程监控信息的数据结构5 2 表5 8 线程监控信息管理a p i 。5 3 表5 9 线程控制信息访问a p i 5 4 表5 1 0c o r b a 接口5 4 表5 11 基于a o p 的存储空间管理代码5 5 表5 1 2 基于a o p 的信息获取更新实现方法5 6 国防科学技术大学研究生院学位论文 图目录 图2 1s r c m l 工作原理图1 1 图2 2 关注点的分离实现和合并模型1 3 图2 3 传统a o p 编织过程1 7 图2 4x w e a v e r 编织过程。18 图2 5p u r e 的内存监视( 左) 和c p u 监视( 右) 图2 1 图2 6g t m p 的监控界面2 1 图2 7o r b 结构示意图2 2 图3 1 基于监控的可信软件构造模型t s c m 2 4 图3 2 监控能力自动注入机制2 6 图3 3 监控需求表达方法2 7 图3 4 软件运行监控机制。2 8 图4 1 可信软件开发环境t s i d e 体系结构图3 3 图4 2 通用模板库的组成3 4 图4 3 监控服务单进程模式工作原理图3 5 图4 4 监控服务分布模式工作原理图3 5 图4 5 开发环境各模块间的交互关系3 6 图4 6 监控能力自动注入模块体系结构图3 7 图4 7 代码分析模块结构图3 8 图4 8 需求表达模块结构图3 8 图4 9 监控代码自动生成模块结构图3 9 图4 1 0 软件运行监控模块体系结构图4 0 图4 1 l 背板服务模块构成4 1 图4 1 2 监控客户端模块构成4 1 图4 13 监控需求表达过程4 2 图4 1 4 监控需求模板构成4 3 图4 1 5 基于a o p 技术的监控信息存储管理4 5 图5 1 监控需求输入界面4 8 图5 2 监控信息存储模块类图5 3 图5 3 验证程序类图5 7 图5 4 源代码分析及需求输入结果5 7 图5 5 探针生成和代码注入过程显示5 8 图5 6 编织时间显示5 8 图5 7 监控状态信息显示5 8 独创性声明 本人声明所呈交的学位论文是我本人在导师指导下进行的研究工作及取得的研 究成果尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已 经发表和撰写过的研究成果，也不包含为获得国防科学技术大学或其它教育机构的学 位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文 中作了明确的说明并表示谢意 学位论文题目基王鳖揎数互焦筮住掬造挂盔丑究生塞理 一 学位论文作者签名：盎垒查 日期：留年j 月7 日 学位论文版权使用授权书 本人完全了解国防科学技术大学有关保留、使用学位论文的规定本人授权国 防科学技术大学可以保留并向国家有关部门或机构送交论文的复印件和电子文档，允 许论文被查阅和借阅；可以将学位论文的全部或部分内容编入有关数据库进行检索， 可以采用影印、缩印或扫描等复制手段保存、汇编学位论文 ( 保密学位论文在解密后适用本授权书) 学位论文题目： 基王些整鲍互焦筮佳掏造撞苤盈塞生塞煎 学位论文作者签名：盔垒垒日期：少超年1 月j7 日 作者指导教师警多豳逝 日期：加舻年，月卿 国防科学技术大学研究生院学位论文 第一章绪论 1 1 研究背景 随着计算机与网络技术的飞速发展，软件已经渗透到了国民经济和国防建设 的各个领域，在信息社会中发挥着至关重要的作用i l j 。一方面，软件应用的普及程 度增加，软件成为信息基础设施，例如网上银行、电子商务和电子政务等，离开 了软件，这些应用都不会出现。另一方面，软件和关键领域的结合程度增加，为 大型复杂逻辑系统的设计提供了强有力的实现手段。例如在航空航天、工业过程 控制、核电站监控与安全保护、交通运输、医疗卫生等关键领域，软件的作用不 可替代。相应地，人们越来越依赖软件，对软件质量及服务的要求也越来越高。 然而，随着软件规模和复杂度的增加，软件失效和故障问题日益加剧，给人们的 工作生活带来许多不利影响，甚至给人类生命、财产和环境造成灾难性的损失。 1 9 9 6 年6 月4 日，欧洲阿里安5 首发失败，起飞后3 7 秒，火箭由于飞行软件错误 在空中爆炸 2 1 。2 0 0 3 年5 月4 日，搭乘俄罗斯“联盟圳a 1 载人飞船的国际空 间站第七长期考察团的宇航员们在返回途中，由于计算机软件设计中的错误，飞 船偏离了降落目标地点约4 6 0 公里p j 。2 0 0 3 年8 月1 4 日，软件错误导致美国及加 拿大部分地区大规模停电( 5 0 0 0 万居民受到影响，三大汽车公司停止生产) ，一 天经济损失3 0 0 亿美元 4 1 。2 0 0 2 年6 月2 8 日，美国商务部的国立标准技术研究所 ( n i s t ：n a t i o n a li n s t i t u t eo fs t a n d a r d sa n dt e c h n o l o g y ) 发表了有关软件缺陷的损 失调查报告。报告表示，“据推测，由于软件缺陷而引起的损失额每年高达5 9 5 亿 美元。这一数字相当于美国国内生产总值的o 6 ”【5 j 。因此，人们对软件的可信 性质给予了十分的关注。 什么是软件可信? 自2 0 世纪7 0 年代初期，a n d e r s o n 首次提出可信系统 ( t r u s t e ds y s t e m ) 的概念以来 6 1 ，软件的可信性问题就一直受到学术界和工业界 的广泛关注1 1 1 1 。多年来，从不同的角度，人们对于可信的概念提出了很多不同的 表述【l l 】：从系统的角度，i s o i e c1 5 4 0 8 标准【7 j 将可信定义为：一个可信( t r u s t e d ) 的组件、操作或过程的行为在任意操作条件下是可预测的，并能很好地抵抗应用 软件、病毒以及一定的物理干扰造成的破坏；可信计算组织( t r u s t e dc o m p u t i n g g r o u p ) 认为：一个实体在实现其给定目标时，若其行为总是如同预期，则称这个 实体为可信的1 8 j ；从用户体验的角度，微软公司的比尔盖茨认为可信计算是一种 可以随时获得的可靠安全的计算，并包括人类信任计算机的程度，就像使用电力 系统、电话那样自由、安全 9 1 ；从网络行为的角度，林闯等认为可信的网络应该是 网络系统的行为及其结果是可以预期的，能够做到行为状态可监测，行为结果可 第l 页 国防科学技术大学研究生院学位论文 评估，异常行为可控制【i 叫。概括而言，我们认为如果一个软件系统的行为总是与 预期相一致，则可称之为可信( t r u s t w o r t h y ) l l 。可信软件构造技术是指保证软 件系统的行为总是与预期相一致的软件开发技术和过程技术。 从影响范围来看，软件可信性研究受到了国内外的广泛关注。在美国，d a r p a 、 n s f 、n a s a 、n s a 、n i s t 、f a a 、f d a 和其他d o d 机构都积极参与关于高可信 软件和系统的研究开发【l j 。美国n s t c 先后形成一系列报告：a m e r i c ai nt h ea g eo f i n f o r m a t i o n ：af o r u m 1 2 1 、r e s e a r c hc h a l l e n g e si nh i g hc o n f i d e n c es y s t e m s 1 3 1 、s e t t i n g a l li n t e r a g e n c yh i g hc o n f i d e n c es y s t e m s ( h c s ) r e s e a r c ha g e n d a 1 4 】和h i g hc o n f i d e n c e s o f t w a r ea n ds y s t e m sr e s e a r c hn e e d s ”儿1 1 。国内目前有多家单位从事高可信软件研 究：中科院软件所林惠民院士开展了基于形式化的高可信软件研究【1 6 】【r 7 】南京大 学李宣东教授领导的课题组主要针对建模阶段的系统开展运行时刻校验研究【1 8 】； 国防科技大学陈火旺、王戟教授等领导的课题组【l 】、北京航空航天大学蔡开元教授 领导的课题组【l9 j 也在高可信软件方面取得了良好进展。国家高技术研究发展计划 ( 8 6 3 计划) 在信息技术领域“高可信软件生产工具及集成环境”重点项目2 0 0 7 年 度课题申请指南中就明确提出，高可信软件开发工具及集成环境是基础软件的重 要组成部分，既是软件技术发展的技术制高点之一，也是我国软件产业发展的关 键基础，具有重要的现实意义和长远的战略意义。 从研究内容和现状来看，国内外针对高可信软件的研究大致分为以下几类： 高可信程序语言及编程环境；传统语言程序的分析、验证与测试；可信软 件的开发方法及运行支撑平台；软件可靠性测试与评估；仿真与容错技术。 其中，对可信软件的开发方法及运行支撑平台的研究在国内外目前仍然属于起步 阶段。美国总统信息技术顾问委员会( p i t a c ) 在2 0 0 5 年报告中就指出，目前的 商业软件工程缺乏生产高质量、高可靠的软件产品所需要的科学基础和严格手段 【2 们。而且随着网络技术和i n t e m e t 的迅猛发展，软件运行从封闭、静态的主机桌 面逐步走向开放、多变的分布环境1 2 i 】。应用规模急剧增长的同时，软件的复杂度 也不断提升，表现出开放性、动态性、不可预测性、潜在不安全性等诸多特性， 给我们构造高可信软件带来了诸多困难。软件作为人类连续的高度复杂的智力产 品，其科学原理和工程规律远未得到充分的认识，从而缺乏有效地生产高可信软 件的软件技术。 综上所述，可信软件构造技术是当前软件技术面临的重大挑战。从科学意义 上，它要求人们对软件系统开发和运行等规律有更深一步的认识；从应用价值上， 它关系到人们在信息社会对信息基础设施的依赖和可信程度的提高【l 】。研究如何构 造可信软件已经成为当前软件工程领域的热点问题之一，具有重要的理论意义与 应用价值。 第2 页 国防科学技术大学研究生院学位论文 1 2 研究现状 可信软件系统在很大程度上不会因为系统中存在的错误、环境的异常或恶意 的攻击而导致系统的失效，这要求系统的行为能够得到准确的把握，即系统的行 为是可预计的【l 】。经过多年的研究，目前人们对于造成软件不可信的原因、机理已 有基本认识，并研究出了一些对策。例如，形式化方法、软件测试方法、过程管 理方法和软件监控方法等都是提高软件可信性的方法：形式化方法用形式化的语 言来描述软件的需求和特征，通过推理验证来保证最终的软件满足这些需求和具 备这些特征；软件测试方法通过静态的源代码分析以及动态的目标码运行等不同 的途径查找软件的缺陷；过程管理方法则主要针对开发者，提高开发过程的规范 性，从而减少缺陷；软件监控方法是本文实现可信软件构造的支撑技术，主要通 过对软件实施有效的监控，获得软件的运行状态，并通过将监控结果与预期行为 进行比较，从而有效的掌握软件行为的可信程度，并在发生问题时准确分析和定 位软件故障。 形式化方法：形式化方法是关于在软件系统的开发中进行严格推理的理 论、技术和工具，它主要包括形式化规约技术和形式化验证技术【l 】【2 2 】。形式化规约 是对程序“做什么 的数学描述，使用精确语义的形式语言刻画软件系统及其性 质，可以尽早发现需求和设计中的错误、不一致、歧义和不完全。目前主要的形 式化规约技术有c s p 、c c s 、s t a t e c h 2 3 1 、r a i s e 语言和方法l 2 4 j 等。形式化验证与 形式化规约之间具有紧密的联系，形式化验证就是验证已有的软件系统是否满足 其规约要求。目前常见的形式验证方法主要有两类：模型检验( m o d e lc h e c k i n g ) 和演绎验证( d e d u c t i v ev e r i f i c a t i o n ) 。模型检验技术的基本思想是通过搜索待验证 软件系统模型的有穷状态空间来检验系统的行为是否具备预期性质【1 6 1 2 5 1 。目前的 模型检验工具主要有s m v 2 6 、s p i n 27 。、m u r p h y ( s t a n f o r d ) 、s p i n ( b e l l ) 、 v i s ( b e r k e l e y ) 2 8 j 等。演绎验证基于定理证明( t h e o r e mp r o v i n g ) 的基本思想， 通过基于公理和推理规则组成的形式系统，以如同数学中定理证明的方法来证明 软件系统是否具备所期望的关键性质。目前主要演绎验证工具有：基于 m a n n a 2 p n u e l i 证明系统的s t e p ( s t a n f o r dt h e o r e mp r o v e r ) 、t l v 、机器定理证明器 ( a c l 2 、c o q 、h o l 、i s a b e l l e 、l a r c h 、n u p d 、p v s 、t p s ) 等幽j 。形式化方法的 一个重要优点是能以一种严格的方式保证软件可信性，并且其中的模型检验技术 为自动化软件工程提供了新的途径。2 0 世9 0 年代以来，在国际上，形式化方法已 经成为软件开发中重要的可信软件技术之一l l 】。 软件测试方法：软件测试是通过静态的源代码分析以及动态的目标码运行 来判断软件是否具备所期望的性质的过程，是可信软件开发中一个行之有效的、 第3 页 国防科学技术大学研究生院学何论文 必不可少的、客观地评估软件可信性的方法【1 1 。一方面，软件测试作为发现并定位、 进而排除导致软件可信性降低的直接因素软件缺陷的有效手段，能迅速提高 软件的可信性；另一方面，通过对软件在测试过程中所表现行为的观察和对测试 数据的分析，可以获得软件可信性验证和评价的直接佐证【2 圳。正如b r o o k s 所说， 对于普通性质的软件开发项目，有5 0 以上的资源要花费在软件测试上，而对于 高可信软件，则高达8 0 以上1 3 0 】。软件测试方法可以分为两类：静态测试和动态 测试。静态测试的主要特征是测试时并不真正运行被测试的程序，可以用于对各 种软件的文档进行测试，是软件开发中十分有效的质量控制方法之一。动态测试 的基本思想通过运行软件来检验软件的动态行为和运行结果的正确性，它必须包 括三个要素：被测试的程序、用于运行软件的测试数据以及软件需求和规约【3 1 1 。 软件测试是当前开发高可信软件不可或缺的关键技术之一，但是该技术本身在满 足高可信软件开发方面也面临着诸多挑战。 过程管理方法：软件过程是指实施于软件开发和维护中的阶段、方法、技 术、实践以及相关产物( 计划、文档、模型、代码、测试用例和手册等) 的集合【3 2 1 。 通过对软件过程的管理和控制，可以将软件开发人员、工具和方法进行有机结合， 提高软件的生产质量和效率。因此，软件过程对高可信软件开发有着重要的影响。 卡内梅隆大学软件工程研究所提出的c m m 3 3 】根据一个软件企业的软件开发过程 与生产组织结构的特点来定性地刻画其软件生产的成熟程度，并将成熟程度与所 能够生产的软件规模、所能够达到的软件质量以及软件生产的开销与质量的稳定 性联系起来【l j 。目前国际上上已经开始将软件过程模型与可信软件开发联系起来。 例如面向可靠性，净室软件工程法( c l e a n r o o ms o f t w a r ee n i n e e f i n g ) 【3 4 】将软件开发 过程置于统计质量控制之下，可以用于开发有可靠性认证的高质量软件。面向安 全性，有软件开发过程错误发生机制与软件质量定量预测模型( f a s g e pm o d e l ) 【3 5 】。但是，无论是对于软件可信性质的度量，还是在软件过程中进行工程化的跟 踪，过程控制策略和技术手段现在都很缺乏【l j 。 软件监控方法：针对软件实施合理的监控，及时获得软件系统的状态，掌 握系统的实时行为，提高系统的可监控性是提升软件可信性的重要手段和方式。 只有获得了系统的状态，才能够准确分析和定位系统的故障，从而实施系统维护， 也只有在获得了系统状态的前提下才能够准确分析被监控软件的行为，并与其被 期望的行为进行比较，来判断软件是否处于可信状态。不具备可监管能力的系统 不仅会大幅度增加维护软件产品的成本，而且会对系统的可信特性带来威胁。微 软最新的操作系统v i s t a 就通过集成的性能与稳定性监视器( p e r f o r m a n c ea n d r e l i a b i l i t ym o n i t o r ) 3 6 1 来收集运行信息，并将其以易于阅读的分类格式提供给用户， 从中用户可以对系统的健康状态作出评估，并找出系统中可能存在的潜在问题。 p r o g r e s s i v es t r a t e g i e s 实施的一项独立研究也表明，o r a c l el o g 中出色的软件可 国防科学技术大学研究生院学位论文 管理性使其日常维护成本比其它同行( 如s q ls e r v e r2 0 0 0 ) 少3 0 到2 0 l j 。这 些都是通过监控来提高系统可信性的实例。 越来越高的维护成本和对软件可信性的要求已使人们充分认识到软件监控的 重要性，并使其成为可信研究领域内的热点问题。当前，国际上有许多著名组织 和公司正在开展监控技术的研究，取得了一些有益成果，涌现出了一些有助于对 软件实施有效监控的新技术新手段。概括而言，软件监控技术目前主要有以下发 展趋势： 趋势一：监控逻辑和功能逻辑的隔离程度越来越高。 早期，对软件实施监控主要依靠开发者将监控逻辑直接硬编码在系统中，通 过记录日志等方式为系统维护人员提供获取系统状态的手段。这种方式要求在许 多地方分散重复的监控代码，通用性、模块性差，监控逻辑和业务逻辑紧密耦合。 当系统变化时，这种方式很难维护，造成添加或修改应用程序的代码变得很困难。 简单地说，系统监视是经典的横切关注点，非模块化的实现使得软件代码相互纠 结，难以维护。 针对上述问题，基于方面的编程( a o p ) 技术的迅速发展与成熟成为监控技 术发展的契机【4 3 1 。a o p 技术旨在解决面向对象技术中不可避免的“横切关注点” 问题 6 0 】。a o p 允许定义“横切关注点”，将监控模块以“方面 ( a s p e c t ) 的形式加 以实现，达到和功能方面解耦的效果。a o p 在更高的抽象和分解层次上，进一步 提高了软件的可维护性、可复用性和可扩展性。将软件监控作为非功能a s p e c t 实 现，能够有效实现监控代码的模块化，能够有效保证监控逻辑和功能逻辑的隔离。 趋势二：运行平台对监控的支持越来越丰富。 随着中间件等技术的发展，基础运行平台提供了很多对软件实施运行监控的 能力。 一方面，运行平台提供丰富的系统级监控手段和方法。监控信息通常包括c p u 利用率、吞吐量、内存使用，以及对各种系统事件( 比如相应的堆分配、线程启 动) 的通知。比如j a v a 虚拟机( m ) 通过j v m p i ( j a v av i r t u a lm a c h i n ep r o f i l e r i n t e r f a c e ) 提供系统监控能力1 3 引。j v m p i 是j a v a 系统监控程序代理获取系统信息 的双向函数调用接口。监视程序通过j v m p i 能获取多种信息，例如用于综合性能 分析的堆内存分配址、c p u 使用热点、不必要的对象保持及监控器竞争等。 另一方面，运行平台通过反射等机制，使得管理人员能够在不依赖开发人员 硬编码的情况下，对基于该平台运行的构件实施监控。比如c o r b a 的截获器机 制能够在不改变对象实现的情况下，获得远程请求的信息，以及对象对远程请求 的处理情况【3 引。j a v a 管理扩展j m x ( j a v am a n a g e m e me x t e n s i o n s ) 是一种旨在简 化和标准化企业j a v a 应用程序运行时的管理基础架构的j a v ac o m m u n i t yp r o c e s s ( j c p ) 规范【3 9 l 。j m x 定义了一种用于让应用程序公开管理功能的标准方法，具 国防科学技术火学研究生院学位论文 有一定的通用性和灵活性。 趋势三：监控能力的注入方式越来越灵活。 传统监控主要依赖开发人员的硬编码，监控能力的注入主要在编码阶段实施， 需要获得系统的源代码。现在借助于运行平台的反射机制和工具支持，人们可以 在编译前、编译后、