（计算机软件与理论专业论文）网构软件系统构建的形式化分析研究.pdf

ad i s s e r t a t i o ns u b m i t t e dt os h a n g h a ij i a ot o n gu n i v e r s i t yf o rt h e d e g r e eo fp h i l o s o p h yd o c t o r f o r m a la n a l y s i sa n dc o n s t r u c t i o nf o r i n t e r n e t w a r e b a s e ds o f t w a r es y s t e m a u t h o r ：惭，j i a n k u n s p e c i a l t y ：c o m p u t e r s o f t w a r ea n dt h e o r y a d v i s o r ：p r o f h u a n gl i n p e n g s c h o o lo fe l e c t r o n i c sa n de l e c t r i ce n g i n e e r i n g s h a n g h a ij i a ot o n gu n i v e r s i t y s h a n g h a i ，e r c h i n a a p r ，2 0 0 9 m肿l3 唧75洲3删8耵i_y 上海交通大学 学位论文原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下， 独立进行研究工作所取得的成果。除文中已经注明引用的内容外，本 论文不包含任何其他个人或集体已经发表或撰写过的作品成果。对本 文的研究做出重要贡献的个人和集体，均己在文中以明确方式标明。 本人完全意识到本声明的法律结果由本人承担。 炽 1 矿 o 。 动 秒 r r r “j q 钥 签 f 利 悔 作 1 文 沙 做 沙 位 期 学 日 上海交通大学 学位论文版权使用授权书 本学位论文作者完全了解学校有关保留、使用学位论文的规定， 同意学校保留并向国家有关部门或机构送交论文的复印件和电子版， 允许论文被查阅和借阅。本人授权上海交通大学可以将本学位论文的 全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫 描等复制手段保存和汇编本学位论文。 保密口，在一年解密后适用本授权书。 本学位论文属于 ， 不保密瓯 ( 请在以上方框内打“4 ”) 学位论文作者签名：彳屯4 蟛u 指导教师签名： 日期：少口，蓐垆月o z s e 1 日期：口、，7 年咱奠歹日 - 上海交通大学博士学位论文答辩决议书 所在 姓名伍建煜学号0 0 6 0 3 3 2 0 0 5计算机软件与理论 学科 指导教师黄林鹏 答辩 2 0 0 9 0 4 1 9 答辩 浩然1 1 楼 日期地点 论文题目 网构软件系统构建的形式化分析研究 投票表决结果：，j _ r( 同意票数实到委员数应到委员数)答辩结论：日筵过 口未通过 妒期日 职务姓名职称 单位 签名 主席 宋国新 教授华东理工大学 锄 震 荔撕彩 口 委员李明禄教授上海交通大学 一辩 委 委员 陆朝俊副教授上海交通大学 隍撇 员 a 委员 童维勤 教授上海大学 一锄鳓 口 成 骗，秒乞 员 委员虞慧群 教授华东理工大学 j l 签 委员 名 委员 秘书 王德俊讲师上海交通大学矽傍仙 答辩决议书 伍建煜同学的论文研究了网构软件的构造过程以及网构软件的 整个生命周期，并基于抽象状态机进行形式化分析，提出相应的理论 模型。论文选题新颖，所研究的问题具有重要的理论意义和应用价值。 论文的主要创新如下： 1 、提出了基于抽象状态机的网构软件的基础模型。 2 、提出了基于抽象状态机网构软件模型的精化机制。 3 、提出了基于抽象状态机网构软件模型的验证方法，从精化正 确性验证以及模拟执行验证两个角度来保证目标网构软件的正确性。 4 、作为上述模型和方法的应用，设计了基于o s g i 与r o s g i 平台的普适网构智能家庭体系结构。 论文结构合理，论证充分，结论可信，表明作者具有坚实宽广的 基础理论和系统深入的专门知识，独立从事科研能力强。 答辩过程中叙述清晰，回答问题正确。经答辩委员会无记名投票， 一致同意通过伍建煜同学的博士论文答辩，并建议授予工学博士学 位。 么彬 p 7 一牛一f7 e 海交通大学博 学位论文 摘要 网构软件系统构建的形式化分析研究 摘要 随着i n t e r n e t 广泛应用和普及，软件开发、部署、运行和维护的计算平台已经 逐步由封闭、静态、可控走向开放、动态、难控。i n t e r n e t 平台上软件系统已经呈 现为柔性可演化、连续反应式、多目标适应的新形态。中国软件工程领域将这样一种 新的软件形态称之为网构软件。本文对网构软件的构造过程以及网构软件整个生命周 期进行研究，基于抽象状态机理论提出一套适合分析、构造以及验证可靠网构软件系 统的形式化模型，同时给出普适环境下智能家庭系统的原型案例。 论文的主要研究工作和创新性包含以下几个方面： ( 1 ) 本文采用分布式抽象状态机进行刻画目标网构软件系统，建立分布式抽象状 态机与网构软件之间的映射关系，在这个模型中每个子抽象状态机对应为网络平台中 的一个构件，而构件内部的输入输出又进一步分解成子抽象状态机，它们之间通过监 督函数进行交互。在该环境中，除了构件本身，其它所有与此构件有交互关系的构件 及网络状况都构成了该构件的运行环境。环境中的普通函数通过成为该构件子状态机 中的监督函数来对该构件提供环境信息。通过这些映射关系，建立了基于抽象状态机 的网构软件模型。该模型具有可抽象执行验证的特征，使得目标系统在需求高抽象层 次各种属性能够得到验证。在模型中对构件之间的交互模式，交互仲裁模型等进行了 详细的分析，该模型的建立使得网构软件在构造之前需求能够准确清晰。 ( 2 ) 由于采用抽象状态机刻画网构软件系统往往从抽象程度极高的自然层次开 始，为了使模型能够逐步向可执行的目标系统逼近，本文提出基于抽象状态机网构软 件抽象模型的精化机制，并给出交互模式的精化模型和构件精化模型。通过研究基于 第1 页 上海交通大学博十学位论文 摘要 抽象状态机网构软件抽象模型的通用精化机制，本文进一步给出了智能家庭体系结构 中协作模型的精化模型以及基于o s g i 的普适网构基础平台的精化模型。在这些模型 中保证了精化步骤不丢失或变化系统的原有特性和性质，从而确保精化的正确性，最 终保证高层次抽象网构软件模型与最终网构软件模型的一致性。 ( 3 ) 为了在网构软件设计的早期阶段尽量的避免和消除错误，本文采用抽象状态 机的可抽象执行机制，提出网构软件精化设计过程中在不同抽象层次的可执行验证模 型。因此，通过该模型可以在不同的抽象层次对网构软件设计模型进行模拟执行，从 而尽早的发现设计中的问题，在设计的早期阶段保证软件的正确性，避免后期错误带 来的巨大损失。另一方面，为了在设计的精化过程中不丢失目标系统的各种属性，精 化前后保持一致性，本文提出了基于抽象状态机的网构软件模型精化验证模型，通过 该模型能够确保设计精化过程的正确性，由此也可以由过程的正确性来保证目标系统 的正确性。 ( 4 ) 为了采用网构软件理论有效的解决普适计算领域中的问题以及使网构软件理 论在新的领域进一步得到验证和丰富，本文采用o s g i 和r - o s g i 作为普适网构软件平 台，并提出合理的智能家庭体系结构。在该结构中，结合r - o s g i 技术优点给出了三 种重要的协作模型：a ) 直接服务请求协作模型，b ) 基于远程事件的发布订阅形成 的协作模型，c ) 被动协作模型，并且在原型系统中得到了实现。通过系统实验验证 可以看出，本体系结构对于指导普适网构软件的开发具有一定现实意义。 关键词：网构软件，抽象状态机，构件组装，精化模型，模型验证，o s g i ，智能家 庭系统，普适计算，基础模型 第1 i 页 上海交通大学博十学位论文 a b s t r a c t 皇曼曼i i ii ii 曼曼曼曼皇葛曼 f o r m a la n a l y s i sa n dc o n s t r u c t i o nf o ri n t e r n e t w a r e b a s e ds o f t w a r e s y s t e m a b s t r a c t 晰t ht h ee x t e n s i v ea p p l i c a t i o no fi n t e m e t , t h ed e v e l o p m e n t ，d e p l o y m e n t a n dm a i n t e n a n c eo fs o f t w a r eb e c o m e so p e nd y n a m i ca n du n c o n t r o l l a b l e t o a c c o m m o d a t et h en e wr e q u i r e m e n t s ，s o f t w a r es y s t e m sn e e de v o l v i n ga n d m u l t i a d a p t i v e w h i c h i ss o c a l l e di n t e r n e t w a r ew i t hc h a r a c t e r i s t i c so f a u t o m a t i o n ，c o o r d i n a t i o na n de v o l u t i o n t h i sp a p e rm a k e sr e s e a r c ho nt h e c o n s t r u c t i o na n dl i r ec y c l eo fi n t e m e t w a r ea n da l s op r o p o s e so n ef o r m a l m o d e lb a s e do na b s t r a c ts t a t em a c h i n et oa n a l y z ec o n s t r u c ta n dv e i l f y i n t e r n e t w a r e s y s t e m i na d d i t i o n ，s o m e s m a r th o m es y s t e mc a s e sa r e d e s c r i b e d m a j o rw o r ki nt h i sp a p e r i n c l u d e s ： ( 1 ) b u i l d i n gd a s m ( d i s t r i b u t e d a b s t r a c ts t a t em a c h i n e ) t of o r m i n t e r n e t w a r es y s t e ma n dm a p sb e t w e e nd i s t r i b u t e da b s t r a c ts t a t em a c h i n ea n d i n t e m e t w a r e i nt h i sm o d e l ，o n ec o m p o n e n tm a p st oo n es u b a s mw h o s e i n p u t o u t p u t a r ea l s os u b s u b a s mi n t e r w o r k i n gw i t hm o n i t o rf u n c t i o n i n t e r n e t w a r ec o m p o n e n ti t s e l fa n di t sr e l a t e dc o m p o n e n t sc o n s t i t u t et h e r u n n i n ge n v i r o n m e n t n o r m a lf u n c t i o np r o v i d e sb a c k g r o u n di n f o r m a t i o nb y b e c o m i n gm o n i t o rf u n c t i o ni ni t sa b s t r a c ts t a t em a c h i n e t h i si n t e r n e t w a r e m o d e lb a s e do na s mc a nb ee a s i l yv e r i f i e d a b s t r a c tp r o p e r t i e so ft a r g e t s y s t e mr e q u i r e m e n t sa n dm a k er e q u i r e m e n tc l e a rb e f o r ec o n s t r u c t i o n ( 2 ) t om a k ei t a sa c c u r a t ea sp o s s i b l ew h e nb u i l d i n gm o d e lf r o mt h e h i 曲l e v e lt o t h ee x e c u t a b l et a r g e ts y s t e m ，o n ea c c u r a c ym e c h a n i s mi s p r o p o s e do ni n t e m e t w a r em o d e lb a s e do na s m b ys t u d y i n gt h eg e n e r i c a c c u r a c ym e c h a n i s mo fi n t e r n e t w a r em o d e l ，t h i sp a p e ra l s og i v ea c c u r a c y m o d e lo fc o o p e r a t i o nm o d e li ns m a r th o m ea r c h i t e c t u r ea n dp e r v a s i v e 第1 i i 页 上海交通大学博七学位论文 a b s t r a c t i n t e r n e t w a r ep l a t f o r mb a s e do no s g i t h e s ea c c u r a c ym o d e l sk e e pt h e o r i g i n a lc h a r a c t e r i s t i c so ft a r g e ts y s t e ma n dm a k ec o n s i s t e n tb e t w e e nt h eh i 曲 l e v e la b s t r a c ti n t e m e t w a r em o d e la n df i n a lm o d e l ( 3 ) t of i n da n df i xt h ee 咖r sa t a se a r l y s t a g ea sp o s s i b l e ，a b s t r a c t e x e c u t i v em e c h a n i s mi s d e s i g n e d t o v e r i f yd i f f e r e n tl e v e la b s t r a c t i o ni n i n t e r n e t w a r ea c c u r a c y b ye x e c u t i n gt h i sm o d e l ，p r o b l e m sw i l lb ef o u n d d u r i n ge a r l yd e s i g n i na n o t h e ra s p e c t ，a c c u r a c ym o d e l s ，w h i c hk e e pt h e p r o c e d u r ea c c u r a t e ，a l s om a k ef i n a ls y s t e mc o r r e c t a t i o n ( 4 ) b e s i d et h ea b o v em o d e l s ，t h i sp a p e ra l s oa p p l i e si n t e m e t w a r et o s o l v ep r o b l e m si np e r v a s i v ec o m p u t i n g s m a r th o m ea r c h i t e c t u r eb a s e do n o s g ia n dr - o s g ii sd e s i g n e d ，i nw h i c ha ) d i r e c ts e r v i c er e q u e s tc o o p e r a t i v e m o d e l ，b ) c o o p e r a t i v em o d e lb a s e do nt h ep u b l i s h s u b s c r i b ep a t t e r no fr e m o t e e v e n t s ，c ) p a s s i v ec o o p e r a t i v em o d e l ，t h r e ec o o p e r a t i o nm o d e l sa r es u p p o r t e d e x p e r i m e n t a lr e s u l t ss h o wi ti ss i g n i f i c a n tt od e v e l o p m e n to fi n t e r n e tw a r e k e y w o r d s ：i n t e r n e t w a r e - b a s e ds o f t w a r e ，a b s t r a c ts t a t em a c h i n e ( a s m ) ， c o m p o n e n t - b a s e dc o m p o s i t i o n ，r e f i n e m e n tm o d e l ，v e r i f i c a t i o nm o d e l ，o s g i ， s m a r th o m es y s t e m ，p e r v a s i v ec o m p u t i n g ，g r o u n dm o d e l 第页 上海交通大学博士学位论文 目录 量量曼曼曼曼曼曼曼曼量曼曼曼曼曼曼曼曼寡曼曼皇皇曼皇量量曼m i ii i 摘要 目录 a b s t r a c t 第一章引言 i i 1 1 研究背景1 j ，功眵麴学捞衣j j j 2 刀枸q 野律模垄省嗲搀矛考浆3 ，3o s g f 臌务乎台3 j j 4 撒象敖恭扔l 爹硷， 1 2 需求与目标7 ，2 j 需毙豸彰画穆正功丝一7 ，2 2 蒡；溺皇意手秀 c 穆矗三豸旁癌皇8 ，2 3 正r 磊矛盾哥4 i ；钐豆f 蠡争西i 勺丝8 1 3 关键问题8 j 3 ，厢撇：静荭9 j 3 2 描象犹吞祝痢么豸祝蒯j d j 3 3 善声a 麦j 否聋营啄勺骘“g 望爹蠡争z 芒：i l 主豸表j d 1 4 本文的研究内容及主要贡献1 0 1 5 本文结构1 2 1 6 本章小结1 3 第二章基于构件的形式化技术 1 5 2 1 构件的定义1 5 2 2 构件库1 6 2 3 构件形式化目前的现状1 8 2 4 网构软件构建对形式化方法的挑战2 2 2 5 本章小结2 3 第三章网构软件形式化抽象模型 3 1 构件模型及基础模型( g r o u n dm o d e l ) 概念。2 6 3 j j 为孵馍型巧 3 j 2 盔妾砀妇烫翌喜? g m z f d 如如f j 穆 念2 7 第v 页 上海交通大学博十学位论文 日录 3 2 抽象状态机相关概念2 7 3 2 1 办朦施鼢搦玩麓2 7 3 z 2 描象犹忝纪的转移施彤彩运行猡 3 2 j 勇旁豸2 步e i i i 规9 画i 蠢驴，身言i 2 臣巫方童f 毋多：；i 煮3 d 3 3 构件的基础模型( g r o u n dm o d e l ) 31 i i j 为7 钧移到晕准偿3 ， 3 3 2 嫠臼指4 雾勺丝3 2 ，3 3 尹歹夕分名! z 等3 2 3 3 4 历绺为弹镐宏钐锹刀 3 3 5 矗雾z 喜翟枣：垂蔓垂 ；矛2 瑟名露当i ： 谚乒，5 3 3 6 描象蔗宣发学扔蒯筘 3 3 7 友诧徽钟惑祝3 7 3 3 8 塞吞刃庳窆虿蕉艽? 7 ，3 9 互蔓互瀵i f z 宇罗譬j ；，：题3 9 3 4 网构软件的基础模型( g r o u n dm o d e l ) 4 0 3 4 j 笱绺缛裳融芷功拦私形苛纪登记方麓卯 3 4 2 缉裳禊鳓彩架椽4 j 3 4 3 区饲曰祝蒯钳 3 4 4 旃励蒯钉 3 4 5 意层魈象犹恭扰据删宕匕4 3 。z 幺艿彳z 菇孝鸦色萄勃9 譬型4 6 3 5 本章小结4 9 第四章网构软件抽象模型的精化5 1 4 1 精化机制简介5 l 4 2 精化过程5 2 4 3 网构软件形式化精化模型5 4 4 3 1 霓互麓芘钓组炭耢 幺弼 4 3 2 钙瑶钧努铭5 8 4 a 基于r - o s g i 智能家庭协作模型精化案例。5 9 4 4 1 桑够兄，争绍锣 4 4 2 岿记名枣型6 j 4 5 基于o s g i 的网构软件平台模型6 2 4 5 1o s g i 乎分远行扣l 曼卯 第v i 页 上海交通大学博 ：学位论文 目录 4 5 2o s g if r a m e w o r k 主要缛名酣 4 5 3o s g if r a m e w o r k 塞? 堀集。6 4 4 5 4 目办i 劳纪貘垄饬缁锨钐 4 5 6 琚宕动态恿苏枥乒劳纪案例猡 4 6 本章小节7 1 第五章模型验证 5 1 验证方法7 3 5 2k i v 7 4 5 2 j 逻辅馐微疆赶祝蒯乃 只2 2 验赶禁钐矽。7 7 5 3 可执行验证机制8 0 ：；：了jc o r e a s m 8 1 5 3 2 真白鲂譬执行多整邵 5 3 3 耋善于j 可犹存珊z 磲蒯8 3 5 4 本章小结8 7 第六章基于r - o s g i 的案例研究 6 1 应用背景8 9 6 21 i - o s g i 9 0 6 2 j 友彳勺鳜港9 d 6 2 2 远茬缎务瑾：衍移发刃筷型9 j 6 2 3 运翟事斧勉髫簇驾酸9 2 6 2 4 基于r - o s g i 学 7 ：学辅1 b u n d l e 房就钐刃 6 3 关键技术9 6 6 2 本章小结9 9 第七章总结 1 0 1 7 1 主要结论1 0 1 7 2 研究展望1 0 3 参考文献 致谢 攻读博士学位期间已发表或录用的论文 第v i i 页 1 0 5 1 1 7 1 1 9 第v i i i 页 上海交通大学博士学位论文 目录 图表目录 图1 1o s g i 体系结构4 图2 1 构件模型1 5 图2 2 通用软件设计过程2 2 图3 1 抽象状态机中函数、关系及位置的分类3 0 图3 2 构件抽象状态机模型3 3 图3 3 发送模式3 8 图3 - 4 接收模式3 8 图3 5 发送接收模式3 9 图3 - 6 接收发送模式3 9 图3 7 组装模型整体映射架构4 l 图3 8 匹配示意图4 2 图3 - 9p r o c e s sa s m 基础模型4 5 图3 1 0 基于仲裁组装的示意图4 7 图3 1 1 基础构件模型向仲裁模型的基础模型精化4 7 图4 1 抽象状态机不同抽象层次宏观描述。5 1 图4 2 抽象状态机精化流程。5 2 图4 3 抽象状态机精化方法。5 3 图4 4 基本扩展多向交互模式5 4 图4 5 智能家庭仲裁者示例6 0 图4 - 6 协调b u n d l e 基础模型6 2 图4 7 业务b u n d l e 更新过程基础模型6 3 图4 8 运行示例6 9 图4 9 示例的b u n d l e 依赖图7 0 图5 1 验证层次结构示意图7 3 图5 2 精化正确性证明结构7 8 图5 3i n v 结构7 9 图5 - 4 其它谓词结构1 7 9 图5 5 其它谓词结构2 8 0 图5 - 6 基于可执行引擎层次结构8 l 图5 - 7 c o r e a s m 体系结构图8 2 图5 8c o r e a s m 规约程序结构8 3 图6 1 智能家庭网络拓扑结构8 9 图6 2 基于r - o s g i 的分布式体系结构9 1 图6 3 基于r - o s g i 的远程服务注册和发现模型9 2 图6 4 基于r o s g i 的远程事件处理模型9 3 图6 5b u n d l e 的启动级别9 3 图6 _ 6 基于r - o s g i 的智能家庭体系结构9 4 第页 上海交通大学博l 学位论文 目录 图6 7 基于r - o s g i 以服务为中心的家庭应用中间件体系结构。9 4 图6 8 基于远程事件的家用设备协作模型9 5 图6 - 9r - o s g i 服务注册9 7 图6 - 1 0 远程服务注册9 7 图6 1 1e v e n t h a n d l e r 服务注册9 8 图6 1 2 注册d i s c o v e r y l i n s t e n e r 服务9 8 图6 1 3 间接远程服务访问平均延迟9 9 图6 1 4 显示在p d a 上的中国象棋服务9 9 第x 页 上海交通大学博仁学位论文 第一章引言 曼鲁曼! 皇- - ： i m i i_ 皇舅 1 1 研究背景 1 1 1 网构软件技术 第一章引言 随着i n t e r n e t 广泛应用和普及，软件开发、部署、运行和维护的计算平台已经 逐步由封闭、静态、可控走向开放、动态、难控。与传统计算平台不同的是，i n t e r n e t 计算平台的特征主要表现为：无统一控制的“真 分布，节点高度自治，节点之间链 接的开放性和动态性，用户、网络设备和软件资源的多重异构性，网络实体行为的不 可预见性以及环境的潜在不安全性，用户使用方式的灵活性和个性化等。如何在难控、 动态、开放的i n t e r n e t 平台中实现各类软硬件资源的共享和协同已经成为计算机软 件技术面临的重要挑战之一。 如果需要在i n t e r n e t 平台下进行软件系统的开发、运行和维护，同时提供直接、 自然和有效的方法支持，需要在传统面向对象技术体系的基础上，从有限自主性和固 定封装性转变到软件实体主体化、交互方式实现内嵌性和单调性转变到协同方式的分 离性与多样性、从封闭可控的软件结构转变到开放协同软件结构；在前面转变的基础 上进一步完成从基于实体的结构分解转变到基于协同的实体聚合、从静态的系统运行 转变到系统的动态、演化性运行、从确定的系统目标转变到多重不确定性等等。 i n t e r n e t 平台上应用需求的基本形态表现为开放、动态、难控，为了适应开放、 动态、难控的网络环境的需求，软件系统已经呈现为柔性可演化、连续反应式、多目 标适应的新形态。从技术层次看，以面向对象、构件等为技术支撑的软件实体以主体 化的软件服务形式存在于i n t e r n e t 环境中的各节点上，各软件实体通过协同机制实 现跨网络的互联、互通、互操作，形成一种与w w w 类似的软件w e b ( s o f t w a r ew e b ) 。 i n t e r n e t 环境的开放性、动态性以及多变性，以及用户使用方式的个性化要求使得 这类软件w e b 已不再像经典软件那样一蹴而就，需要对外部环境的动态变化进行感 知，并按照功能指标、性能指标或可靠性指标等进行静态( 离线) 的调整和动态( 在线) 的演化，以使系统具有尽可能的满足用户的需求。这种软件形态具有自主性、协同性、 第l 页 卜海交通大学博b 学位论文 第一章引言 反应性、演化性和多目标性等特征。在技术方面，针对网构软件的研究已经广泛展开， 如何从需求到目标系统乃至整个生命周期提供一套形式化的方法用来指导网构软件 的开发是该领域当前需要觉得的问题之一。 南京大学吕建教授在文献 1 中对网构软件进行了如下总结：网构软件是开放、动 态和难控网络环境下的分布式软件系统的一种抽象，它包括一组分布于i n i e m e t 环境 下各个节点的、具有主体化特征的软件实体，以及一组用于支撑这些软件实体以各种 交互方式进行协同的连接子；整体而言，它能够感知外部环境的变化，通过体系结构 演化的方法( 主要包括软件实体与连接子的增加、减少与演化、以及系统拓扑结构的 变化等) 来适应外部环境的变化，展示上下文适应的行为，从而使系统能够以足够满 意度来满足用户的多样性目标。 北京大学梅宏教授等在文献 2 中正式提出了a b c ( a r c h i t e c t u r eb a s e d c o m p o n e n tc o m p o s i t i o n ) 方法来有力支持网构软件的开发。a b c 是一种以软件复用为 核心思想、以软件构件为基本实体、以软件体系结构为中心、以软件中间件为运行支 撑的软件开发方法；是软件体系结构( s o f t w a r ea r c h i t e c t u r e ，简称s a ) 研究和基于 构件的软件开发( c o m p o n e n tb a s e ds o f t w a r ed e v e l o p m e n t ，简称c b s d ) 途径的结合。 a b c 方法的主要思想是将软件体系结构引入到软件开发的各个阶段，作为系统开发的 蓝图，利用工具支持的自动转换机制缩小从高层设计到实现的距离，而后在构件运行 平台( 软件中间件) 的支持下实现自动的系统组装。文献 3 中进一步指出尽管a b c 的 初始目标是传统软件系统，但网构软件是传统软件自然延伸，且a b c 从2 0 0 2 年开始 逐步考虑对网构软件主要特征的支持 4 - 6 。因此，a b c 方法在理念、主旨、过程上 与网构软件的开发是匹配的，能有效支持网构软件的开发。a b c 方法转型为一种网构 软件开发方法的关键在于对网构软件主要特性的支持。结合前面对网构软件开发挑战 的分析，a b c 方法重点开展了3 个方面的研究：在开发过程方面，基于特征的需求建 模支持网构软件自底向上、从“无序”到“有序”的构造过程中，“无序 资源实体 的建模及其组织和管理；以软件体系结构为中心的设计、实现、部署、维护与演化充 分支持网构软件交付后的持续开发。在开发方法方面，自适应软件体系结构设计能够 开发出具备结构自适应性的网构软件，该设计方法也能导出自适应软件实体必须支持 的功能与质量目标。在支持技术方面，a b c 软件体系结构建模工具支持可视化的设计、 实现、部署、维护和演化，a b c 运行平台在支持e j b ，w e bs e r v i c e s 等主流构件模型 的基础上，还提供实时显示与操纵底层平台与上层构件运行状态和行为的反射式框 架，以及基于规则的构件自主运行机制。 第2 页 卜海交通大学博b 学位论文 第一章 引言 1 1 2 网构软件模型的设计需求 在i n t e m e t 的分布式计算环境下的网构软件形式化模型应满足如下所述的需求： ( 1 ) 支持工程化的形式化描述语言，能够实现从需求到功能及其交互关系的准确 映射。在系统架构中，构件及其相互之间的关系应当有准确的描述，这样才能够有效 的表示、开发、理解、修改和复用构件。 ( 2 ) 方便快捷的映射方式，该方式使得形式化描述工具的组件与网构软件中的组 件能够快速映射建模，从而有效的为后续设计过程提供基础。最有效的办法是建立一 套自动或半自动的映射工具。 ( 3 ) 一套有效的网构软件设计过程精化机制，该精化机制使得能够从高层抽象需 求向抽象层次较低的目标层次进行精化。因此，提出一套适合网构软件的精化模型是 网构软件模型的重点需求之一。 ( 4 ) 由于网构软件部署在i n t e r n e t 环境中，服务提供者与服务请求者之间往往存 在不完全匹配的情况，因此，网构软件设计中，构件之间的仲裁机制显得尤为重要， 它能够解决和仲裁服务请求者与服务提供者之间的关系。 ( 5 ) 支持高抽象设计层次的可验证性以及向目标层次精化过程正确性的可验证 性，这两方面的特性是确保软件正确性，可信性的最基本要求。 基于上述问题可以看出，网构软件形式化系统模型对网构软件的研究具有重要意 义，在目前的研究中，主要致力于软件形态的表现，系统开发的技术性等层面，从系 统工程的角度，采用形式化的方法进行分析设计的研究还相对较少，本文将从这个出 发点进行展开研究，提出一套形式化的建模机制及分析验证方法，采用的形式化工具 为抽象状态机，抽象状态机是一种高度工程化，自然化的形式化语言，比较容易被软 件工程人员所接受和掌握。 1 1 3o s g i 服务平台 o s g i 7 规范提供了通用和开放的框架，可作为部署网构软件中基础构件的平 台，作为网构软件节点而存在，尤其是在分布式扩展方面，已经取得了许多重要的成 果，比如r - o s g i 方面已经得到了广泛的认可，在o s g i 中，b u n d l e 其实就是能对外 提供