（计算机软件与理论专业论文）自动化dmarf系统的形式化需求规范及性质验证.pdf

f i | i i i i | j f f l f f 舢f i f | 删 y 19 0 3 9 81 t h e s i sf o rm a s t e rd e g r e ei n2 01 l u n i v e r s i t yc o d e ： 10 2 6 9 r e g i s t e rn u m b e r ：5l0 8l5 0 0 0 0 4 e a s tc h i n an o m a l u n i v e r s i t y f o r m a ls p e c i n c a t i o na n dv e r i 6 c a t i o n o fa u t o m a t i cd m a r f s y s t e m a d v i s o r ： j a n u a 2 0 l l 华东师范大学学位论文原创性声明 郑重声明：本人呈交的学位论文自动化d m a r f 系统的形式化需求规范 及性质验证，是在华东师范大学攻读颈庶博士( 请勾选) 学位期间，在导师 的指导下进行的研究工作及取得的研究成果。除文中已经注明引用的内容外，本 论文不包含其他个人已经发表或撰写过的研究成果。对本文的研究做出重要贡献 的个人和集体，均已在文中作了明确说明并表示谢意。 作者签名： ：1 选璋 日期：幻，年，月厂。日 华东师范大学学位论文著作权使用声明 自动化d m 触珂系统的形式化需求规范及性质验证系本人在华东师范 大学攻读学位期间在导师指导下完成的砸左博士( 请勾选) 学位论文，本论文 的研究成果归华东师范大学所有。本人同意华东师范大学根据相关规定保留和使 用此学位论文，并向主管部门和相关机构如国家图书馆、中信所和“知网”送交 学位论文的印刷版和电子版；允许学位论文进入华东师范大学图书馆及数据库被 查阅、借阅；同意学校将学位论文加入全国博士、硕士学位论文共建单位数据库 进行检索，将学位论文的标题和摘要汇编出版，采用影印、缩印或者其它方式合 理复制学位论文。 本学位论文属于( 请勾选) () 1 经华东师范大学相关部门审查核定的“内部”或“涉密”学位论文 拳，于 年月日解密，解密后适用上述授权。 ( 2 不保密，适用上述授权。 导师签名 本人签名王垄鱼 沙，年月幻日 “涉密”学位论文应是已经华东师范大学学位评定委员会办公室或保密委员会审定 过的学位论文( 需附获批的华东师范大学研究生申请学位论文“涉密”审批表方 为有效) ，未经上述部门审定的学位论文均为公开学位论文。此声明栏不填写的，默认 为公开学位论文，均适用上述授权) 。 工渲堕硕士学位论文答辩委员会成员名单 姓名职称单位备注 曾振柄教授华东师范大学主席 软件学院 刘静教授华东师范大学 软件学院 蒲戈光副教授 华东师范大学 软件学院 摘要 现今，计算机系统日趋复杂，对其进行有效的管理变得越来越困难。随着人 们需要的日益增加，系统中会同时存在更多的应用软件，服务器，存储器等。要 想有效的管理这些要素，确保可靠性，系统就需要具有自我管理的功能。 2 0 0 1 年i b m 公司提出了自动化计算( a u t o n o i i l i cc o m p u t i n g ) 的概念。自动 化计算主要由几个核心组成，自我保护、自我优化：自我配置和自我恢复。自我 保护，即系统能够保护自己，防止外界的恶意袭击；自我优化，即系统能够自动 调度资源，以达到降低系统运行消耗的目的；自我配置，即系统配置能够自动完 成，并能根据需要自动调整，来适应动态变化的运行环境；自我恢复，即系统能 够自动从常规和意外的故障中恢复，正常继续运行。 自动化计算系统通过严格的控制各个部分之间的交互来达到自治。但是构 造，控制这些交互十分困难。如何开发一个具有高预测性的，安全可靠的i t 系 统呢? 在这个问题上，我们可以运用严格的数学技术一一形式化方法。 c o n u n u n i c a t i n gs e q u e n t i a lp r o c e s s e s ( c s p ) 是一种形式化方法。其对模块间的通 讯进行刻画，从而模拟整个系统的性质及行为。在描述分布式并发系统中，起到 了很大的积极作用。 本文以分布式声音识别系统( d m a i u ) 为实例，从自保护，自优化，自恢 复三个方面，利用c s p 方法描述其自治性质，给出形式化自治需求规范。从而 实现在分布式声音识别系统上，添加一个自治层，以达到减少维护系统的工作量 的目的。在此基础上，运用p r o c e s s a n 山s i s t o o u 【i t ( p a t ) 工具，对自动化性质 进行检验。 关键词：自动化，形式化方法，c s p ，性质验证 a b s t r a c t n o w a d a y s ，a l o n gw i t hc o m p u t i n gs y s t e m sb e c o m em o r ea 1 1 dm o r ec o m p l e x ，t h e r e a r em o r ea p p l i c a t i o n s ，s e r v e r sa l l dm e m o r i z e r si i lm es y s t e i i lw l l i c hm a k e si t e v e l l h 莉e rt om a i l a g ee 临c i e n t l y i no r d e rt ok e e pr e l i a b i l i t y o u rs y s t 锄n e e d st 0b e s e l f 二m a n a g e d i b mr a i s e da u t o n o m i cc o m p u t i n gt e c l l i l o l o g yi n2 0 0 l ，w h i c hi sc o n s i s t e do ff o u r m a i np a n s ： s e l f p r o t e c t i o n ，s e l o p t i m i z a t i o n ， s e l f - c o n f i g u r a t i o na 1 1 ds e l f h e a l i n g s e l f - p r o t e c t i o nm e a n st h a tm es y s t e l l lc a np r o t e c ti t s e l f 舶mb a l e 如la t t a c ka n dv i m s ： s e l f - o p t i m i z a t i o np r e d i c a t e st l l es y s t e mc a nr e a s s i g nr e s o u r c e sa c c o r d i n gt ou s e r s r e q u i r e m e n t si nd i f f 旨e n tt i m ei no r d e rt ok e 印e m c i e n t ；s e l f h e a l i n gi n d i c a t e st h e s y s t e mc a nd e t e c te n - o r sd u r i n gi u n t i m ea n dr e c o v e rb yi t s e l s e l f c o n f i g u r a t i o n m e a l l st h a tt l l es y s t 锄c a nc o n f i g u r e b yi t s e l ea n dc h a n g ei t sc o n f i g u r a t i o na c c o r d i n g t ot h ee n v ir 0 】f l l n e n td ”a m i c a l l y a u t o n o m i cc o m p u t i n gs y s t 锄a c h i e v e s s e l f - m a n a g e n l e n tb yc o n t r 0 1 l i n gt h e i n t e r a c t i o n sb e t w e e na l lt h ec o m p o n e n t s ， w h i c hi s v e r yh a r dt oc o n s t r u c ta j l d c o l m a i l d h o wt ob u i l du pal l i 曲l yp r e d i c t a b l ea n ds e c u r es y s t e m ? w ec a i la p p l y f 0 衄a lm e t h o dt oa c c o i n p l i s ht h a t c o m n m n i c a t i n gs e q u e n t i a lp r o c e s s e s ( c s p ) i sa f o m a lm e t h o d ，w h i c hd e s 砸b e st h ec o c a t i o n sb e 觚e e n c o m p o n e n t st os i m u l a t e t 1 1 ef e a t u r e sa i l da c t i v i t i e so ft h ew h o l e s y s t e m c s pm e t h o dp l a y sa ni m p o r t a l l tr o l ei n d 印i c t i n gd i s t r i b u t e da n ds u b s c q u e n ts y s t e m s 1 1 1t 1 1 i s p a p e r ，it a l 【ed m 趾强s y s t e ma sa 1 1e x a i 】1 p l e ；d e s c m es e l f - p r o t e c t i o n ， s e i f - o p t i m i z a t i o na i l ds e l o h e a l i n gf e a t u r e su s i n gc s pm e t h o da i l dp r o v i d et h ef o m l a l s p e c i f i c a t i o n m o r e o v e r iu s e 隧r t o o l t ov 嘶黟t h ea u t o n o m i cf e a t u r e s k e y w o r d s ：a u t o n o m i c ，f o 珊a lm e t h o d ，c s p ，p r o p e n yv 谢f i c a t i o n 2 目录 摘要1 a b s t r a c t 2 目录3 第一章引言：5 1 1 自动化计算简介5 1 2 自动化计算系统的结构7 1 3 本文研究目标及贡献8 1 4 本文结构1 0 第二章d m a r f 技术及进程代数c s p 1 l 2 1d m a r f 技术1 l 2 2 进程代数c s p 1 4 2 3p a t 工具1 7 第三章d m a r f 系统抽象模型构架及自保护性质模型分析1 9 3 1d m a r f 系统抽象模型构架1 9 3 2d m a r f 系统自保护性质分析及模型2 0 3 3 本章小结2 6 第四章d m a r f 系统自优化及自恢复性质分析2 7 4 1d m a r f 系统自优化性质分析及模型2 7 4 2d m a r f 系统自恢复性质分析及模型2 9 4 3 本章小结3 5 第五章自动化性质验证3 7 5 1 前提条件的设置3 7 5 2 基于p a t 的模块表达3 7 5 3 可达性断言及验证3 9 5 4 本章小结4 2 第六章总结及展望4 3 6 1 总结4 3 6 2 展望4 4 3 参考文献4 5 附录可达性验证代码4 8 作者研究生阶段参加的项目及发表文章情况5 0 后记5 1 4 第一章引言 1 1 自动化计算简介 随着科技的发展和需求的不断提升，软硬件的复杂度越来越大。特别是在维 护大型复杂系统时，工作量非常巨大。自动化计算，即计算机系统的自我管理能 力，是近期新兴的研究课题。自动化计算技术可以将复杂的系统转化为自治的系 统，从而减少维护的工作量【1 7 ，2 3 ，2 4 1 。 自动化计算是指系统在无人干预的情况下按照规定的程序或指令自动进行 操作或控制的过程。自动化技术广泛用于工业，军事、科学研究、交通运输、智 能家庭等方面。采用自动化技术可以减轻人的繁重的劳动。因此，自动化是工业 国防和科学技术现代化的重要条件和显著标志。 一个系统想要达到自动化，必须要实现一个循环，保证系统中的每个组成部 分在发生变化的时候，系统都能够知道，以便采取正确的行动。系统应提供一定 层次上的自动化管理，来减少解决问题时人为因素的介入。同时，能够正确的表 示系统的执行策略也是自动化系统的重要方面，执行策略提供了系统是如何达到 所期望的结果，也是系统判断何时进行相应的行为的依据。正因如此，任何一个 自动化计算系统都要知道自己的状态，行为，以及运行的环境。下表给出了传统 计算和自动化计算在这四个方面的比较。 表1 传统计算v s 自动化计算 r 渺l e11 r a d i t i o n a lc o m p u t i n gv sa u t o m a t i cc o m p u t i n g 性质传统计算自动化计算 自配置性质数据中心有多种平台，安装，配置，自动的配置各个组成部分，是系统遵循 整合整个系统，耗时又容易出现错误。上层规范。自主的调整系统。 自优化性质系统中有数百个手动设置，非线性调组件和系统不断寻求机会提高自身性 谐参数，并且其数目逐步增加。能和效率。 自恢复性质大型复杂系统的问题检测需要一个团系统自动检测，诊断，并且修护本地的 队的程序员很多的时间。软件硬件问题。 自保护性质对于恶意攻击和级联故障的检测，恢系统自动抵御恶意攻击和级联故障，通 复全部都是手动的。 过早期预警来预防整个系统的失败。 5 自动化计算系统中有四个主要的性质是目前被广泛认可和应用的。 ( 1 ) 自优化性质【2 5 1 ，指系统能够自动的利用资源，并且平衡工作量来提高运行 的效率【2 1 。 ( 2 ) 自恢复性质【2 6 1 ，即主动的发现，诊断，并修复由于系统中的硬件或者软件 而引起的问题【1 4 】。 ( 3 ) 自保护性质，主动的保护系统，以防止外界的恶意攻击，并且防止错误的 级联失败所带来的损伤 8 9 ，1 1 1 。 ( 4 ) 自配置性质，能够自动调节配置信息，使系统能够适应动态变化的环境。 致力于自动化计算的研究有很多，如自动化计算平台的研究，运用自动化计 算的实际应用的研究等。目前看来，自动化计算是应对当今规模越来越大，复杂 度越来越高的计算机系统的可行方法。 美国福特公司的机械工程师哈德于1 9 4 6 年最先提出“自动化”一词，用来 描述发动机汽缸的自动传送和加工的过程。5 0 年代，自动调节器和经典控制理 论的发展使自动化进入到局部自动化阶段。6 0 年代，随着电子计算器的推广应 用，自动控制与信息处理结合起来，使自动化进入到生产过程的最优控制与管理 的综合自动化阶段。7 0 年代，自动化的对象变为大规模、复杂的工程和非工程 系统。这些问题的研究，促进自动化的理论、方法和手段的革新，于是出现了大 系统的系统控制和复杂系统的智能控制，出现了高级自动化系统，如办公自动化 、智能机器人、专家系统、决策支持系统、计算器集成制造系统等( 引自自动化 技术史) 【2 9 ，3 0 1 。 于此同时，在2 0 0 5 年，i b m 推出p m a c ( p o l i c ym a n a g e m e n tf o r a u t o n o m i c c o m p u t i n g ) 构架来丌发和管理智能自动化软件。运用p m a c ，这些软件系统可 以动态的改变行为，并给出自动化调节策略的形式化需求规范。在2 0 0 9 年，i b m 提出了系统全而的通j | j 标准语苦s m l ( s e i c em o d e l i n gl a n g u a g e ) 来描述复杂 i t 系统与服务的模型。在2 0 0 9 年，v a s s e v 等人提出了a s s l ( a u t o n o m i cs v s t 锄 s p e c i f i c a t i o nl a n g u a g e ) 语言，来描述自动化系统的需求规范，使得代码的生成 更加简便【l o 1 8 ，19 1 。 自动化系统根据管理者的需求目标来自我管理。自我管理的质量高低与自动 化计算设计有关，缺陷的设计方针会导致自我管理不能实现，相互矛盾的方针将 会给自动化系统带来巨大的损害。因此对自动化性质设计的正确性的检验十分重 6 要。目前也有很多针对验证自动化计算系统设计正确性的研究。如使用事件微积 分学( e c ) 来验证设计方针。这种方法在构架中添加了时间的概念。但是所有 的非确定性都要事先描述出来。然而在未检测之前，将所有的非确定的可能性都 找出来是很难做到的。除此之外，还有针对方针冲突的检测以及相应的解决方法 的研究等。总而言之，目前对自动化计算系统的设计方针的验证工作还不是非常 成熟。 1 2 自动化计算系统的结构 总体来讲，整个自动化计算系统包含两个部分，控制模块和被控制的系统。 控制模块通过前馈控制策略和反馈控制策略来控制系统。如图l 所示，根据前馈 策略，系统根据输入被控系统的数据来决定执行准则，根据反馈策略，系统根据 比较预期的结果和被控系统输出的数据来决定所要执行的操作。 图1 自动化计算系统构架 f i g u r e1a r c h i t e c t l l r eo f 钒l t o m a t i cc o m p u t i n gs y s t e m 接下来我们简单的介绍基于j 2 e e 实现的自动化计算系统的白优化性质构 架。如图2 所示，d a t ac 0 1 l e c t o r 是存放系统侦测到的数据。搜集实时的性能数 据，以便之后提供给d a t ap r o c e s s o r 来计算平均的应答时间和吞吐量等。这些存 在数据库中的数据也可以被其他组件使用。p r e d i c t o r 通过性能数据来预测未来的 工作量，从而帮助d e c i s i o nm a k e r 处理实时变化的工作量。c o m p a r a t o r 用来比较 实时性能数据，如吞吐量，s e r v i c el e v e la 野e e m e n t ( s l a ) 等的差值。d e c i s i o n m a l ( e r 应用算法，结合p r e d i c t o r ，c o m p a r a t o r 和s l a 所提供的结果数据来选择 k n o w l e d g eb a s e 中的调控性能的方法。t u n e r 将这些方法转化为行为，并且嵌入 到j 2 e e 的应用服务器中，从而实现系统调控性能的需求【5 2 0 2 1 1 。 7 图2 自优化性质构架 f i g u r e 2a u t o n 0 1 【n i cp e r f o 衄a n c et i l l l i n ga r c _ h i t e c t l l r e 随着自动化技术的逐步提高，其应用也越来越广泛。在实际工作中，自动化 系统能够减少人为的参与，自主的控制自身工作，大大的减少了工作量，降低人 为因素引起的错误率。由此可见，合理的设计自动化系统，保证自动化性质萨确 的实现非常的重要【2 5 2 7 ，2 引。接下来，本文将基于自动化d m a r f 系统，对自动化 性质进行分析建模，给出形式化需求规范，并对自动化性质进行验证。 1 3 1 研究目标 本文将以分布式声音识别系统( d m a r f ) 为实例，从自保护，自优化，自 恢复三个方面着手，进行性质描述。从而实现在分布式声音识别系统上，添加一 个自治层，使声音识别系统在原有的基础上实现自动化。并利用c s p 方法，给 出分布式声音识别系统的形式化自治需求规范。从而说明，c s p 方法同样适用于 对自动化系统的描述。并为之后再形式化模型的基础上进行性质验证提供了有力 的理论依据。同时，本文也将运用仿真分析工具p a t ，针对系统的主要自动化性 质进行验证。从而验证自动化分布式声音识别系统是否能够达到自动化性质预期 的目标。 1 3 2 本文贡献 1 ) 对自动化计算进行研究，给出了自保护，自优化及自恢复性质规范，运用c s p 语言对其进行形式化建模。 本文以分布式声音识别系统为例，给出自保护，自优化，自恢复性质规范， 并运用c s p 语言，对自保护，自优化及自恢复性质规范进行正确的描述和刻画， 从而得到形式化需求规范。 通过上述研究，我们可以看到c s p 方法能够对自动化性质进行刻画，使得自 动化系统的设计有了坚实的理论依据。同时，得到的形式化模型也为之后自动化 性质的验证和自动化系统的实现提供了研究基础。 2 ) 利用p a t 工具对主要性质规范进行验证。验证系统是否达到自动化性质预期 目标。 p r o c e s sa n a l y s i st 0 0 1 k i t ( 汀) 是一个支持对实时，并行系统进行仿真，分析 的工具，能够对于死锁，可达性，l t l ，精化等进行验证。p a t 的主要功能如下： 提供支持多种语言的编辑环境，用以引入模型。 提供用以仿真系统行为的仿真器。可以自动仿真，用户引导仿真，生成完 整的状态图，展现t r a c e 路径等。 能够进行死锁分析，可达性分析，时序逻辑检验和精化验证。 给出了多个内设的例子，以便用户参考。 本文运用p a t 工具，利用可达性对d m a r f 系统的自保护性质进行验证。首 先提出断言，即不安全的输入能够导致系统到达不安全的状态。之后，利用p a t 工具，对断言进行可达性验证，判断系统能否满足白保护性质预期的目标。从而 检测自动化系统的设计是否合理有效。 9 1 a 本文结构 本文第二章介绍了d m a i 强系统的发展，技术和其应用。随后，我们引入进 程代数c s p 方法，并给出了c s p 语言的基本语法。c s p 是本文研究的基础，也 是形式化方法中的一个有效工具。在第二章最后一节，本文介绍了用于自动化性 质验证的仿真分析工具w 盯。 第三章给出了d m a r f 系统的抽象构架。并对自动化d m a r f 系统中的自 保护性质进行详细的分析，利用c s p 方法进行建模，从而给出了自保护性质的 形式化需求规范。 第四章第一节对自动化d m a i u 系统的自优化性质进行分析，建模，给出其 形式化需求规范。本章第二节详细分析了自动化d m a i 强系统中的自恢复性质， 并利用c s p 方法对其建模。 第五章运用p a = r 工具，利用可达性对系统的自保护性质进行验证。在这里， 我们的验证方法是不合法的输入数据会导致系统到达非安全状态。从而检验自动 化d m a r f 系统是否能够达到白保护性质预期的目标。 第六章为全文的总结，并对未来的工作进行展望。 1 0 第二章d m a r f 技术及进程代数c s p 2 1d m ar f 赫 2 1 1 声音识别系统的发展 早在计算机发明之前，人们已经设想能够自动的对声音进行识别，早期的声 码器可被视做声音识别及合成的雏形。我们所熟悉的”r a d i or e x ”玩具狗在1 9 2 0 年代问世，可能是最早出现的声音识别器，当呼唤玩具狗的名字的时候，它可以 从底座上弹出来。最早基于计算机系统的语音识别系统( 贝尔实验室开发的 a u d r e y 语音识别系统) ，通过跟踪语音中的共振峰，能够识别1 0 个英文数字。 其正确率达到了9 8 ，效果还是十分可观。 伦敦学院( c 0 1 1 e g eo fl o n d o n ) 的d e n s e 在5 0 年代末将语法概率加入语音识 别中，使声音识别系统更加的准确。在6 0 年代，出现了两大重要的突破：动态 时间弯折d y l l a m i ct i m ew a 印( d t w ) 技术和线性预测编码l i n e a rp r e d i c t i v e c o d i n g ( l p c ) 技术，同时人们将人工神经网络引入了声音识别系统。声音识 别系统最主要的飞跃是隐含马尔科夫模型h i d d e nm 破o vm o d e l ( h m m ) 的应用。 其基本原理是首先对现实世界中的人类语音进行大量的分析，并且在系统中进行 建模，在有数据输入后，系统会对输入数据进行分析，并从中提取声音特征，之 后通过之前建立好的模型来识别出用户所说的话。卡内基梅隆大学的李开复实现 了第一个基于h m m 的声音识别系统s p h i i l 】【，这个系统可以识别大量的词汇。这 以后，严格来说，声音识别技术没有完全脱离过隐含马尔科夫( h m m ) 模型。 2 1 2 声音识别系统技术 声音识别是指计算机能够识别人类所发出的话音，并将其转化成书面的语 言。即从声音到文本的转化。简单来说，就是让计算机能够听懂人类的语言。这 里的“听懂”主要包含两个层次，一是指系统将用户所说的逐字逐句的翻译成为 文字，另一种是指系统能够正确的理解用户所说的内容，但是不要求将所有的词 句都正确的翻译过来。 声音识别技术顾名思义是以声音为研究对象，设计到诸多领域，如语言学， 计算机科学，信号处理，生物学，神经学等等。甚至还可以涉及人体语言学，比 如人们在说话的时候的动作，表情，可以帮助理解其所要表达的意思。 声音识别的过程中，系统中已建立的声音模型可以用来指导识别引擎进行声 音识别，这些声音模型限定了一个识别系统所能识别的语句类型。声音模型通过 1 l 语法的形式来表示，系统将这些规则转化成词图，从而来指导声音的识别。这里 的词图是一个由多个词组成的图，图中每个节点都是一个词，并且图中的任意一 个起始节点到终结节点的路径都是一个有效合法的句子。 在很多领域中，声音识别系统具有一个共同的特点，即这些系统中所用到的 句型很典型，并且句型数目有限，可以总结出规则。如自动电话查询系统，机票 预订系统，股票查询系统等等。这类系统在声音识别的时候，采用语法的方式来 指导可以达到很高的识别率，并且能够达到较快的识别速度，从而提高系统效率， 满足实际的需求。这也是基于语法方式进行声音识别的技术能够广泛应用的原 因。 传统的声音识别系统m a i 心是一个开源的研究平台，集中了各种模式识别， 信号处理，以及自然语言处理等等的算法实现。整个系统是由j a v a 语言实现的。 是一个模块化，可扩展的平台，并且其中的算法可以替换，更方便用于科学研究。 声音识别系统可以分步的运行，也可以独立执行，或者作为库被应用程序所 利用。其中包含了流水线的阶段，这些阶段相互交互，来得到运行中所需要的数 据。总的来说，主要包含四个主要阶段：样品导入，处理，性质分析，分类。 将传统的声音识别系统进行扩展【2 1 1 ，使各个阶段可以像分布式节点一样同时 运行，如图3 所示。基本的阶段没有实现恢复机制，只是在利用j a v ar m i ， c o r b a ，x m l r p c 等进行通讯。 n 潮a p 叫c 确o n c “目n t t 瞰e r ；a p p “n o na 悖瞧 t h i i 皓r f ) p l m 。nc l i 刚 f 。t i m 科 + 纠i o nc f 酶确 丁h i d 憎r 、a 州i 自o nc l 岫n l it h 撕： a p p i i c a b c l h l 图3d m a r f 构架图【2 1 】 f i g u r e3d m a r f a r c h i t e c t l j r e 1 2 现在有很多应用用来检验声音识别系统的功能和服务。其中一个最常用的应 用s p e a k 盯i d e i i 认p p ，则是用来检验发言人身份的。包括识别发言人的性别，口 音，语言。分布式的扩展可以用在处理录音带，文字信息，或者图像数据中。声 音识别系统的主要重点在于对于声音的处理，如会议录音，或者电话录音，可以 利用m 舢心识别讲话者的信息。目前，用户可以通过从笔记本，p d a ，手机上 将声音数据传到网络d m a r f 系统的服务器上，在网络上实现所需的功能【2 6 1 。 2 1 3 声音识别系统的应用 随着声音识别技术日渐成熟，在日常生活中的各个领域都得到了广泛的应 用，涉及面越来越广，如新闻业，金融业，电信业，通讯业，公共事业等。通过 运用声音识别技术，诸多行业的工作流程得到了简化，节省了大量的人力，并且 提高了系统的工作效率和准确率。 在中高档的移动电话，车载电话上，普遍具有语音拨号的功能，随着技术的 普及，产品价格的降低，普通电话上也将具有语音拨号功能。此外，在汽车上对 车载系统，包括卫星导航系统( g p s ) ，音响，空调，照明等的控制，都可以使 用声音识别技术。这样一方面提高了用户的控制效率，另外一方面，可以使司机 在手不离开方向盘的基础上，对汽车进行有效的操作，提高了驾驶的安全性。 同时，在工业控制和医疗领域中，当操作者的手被占用的情况下，通过声音 与机械硬件进行交互，控制，由操作者发出声音命令，机器做出相应的反应，则 是很好的，高安全性的措施。 目前智能家庭中，声音识别技术也是主要的应用之一，通过识别主人的声音 命令，可以对家庭中的电器，如电视，空调，窗帘，影碟机等进行统一的管理和 控制，从而使对多种不同电器用多个遥控器来操作的繁琐过程变得简单易行。 还有我们常用的个人数字助理( p d a ) ，p d a 的体型较小，这个轻便的特点 使得在其上的人机交互变得困难不便，因为在p d a 上使用键盘很不方便。虽然 目前很多的解决方案是提供了手写输入和查询的识别，但是其过程还是让人感到 不适。而声音识别技术，正式解决这个问题的最佳方法，现在业界人士一致认为， p d a 中的人机交互功能，使用声音识别技术是最好的选择。既可以达到交互的 目的，又不需要键盘或者手写的输入，是用户的操作体验更加舒适。可以预见， 将来声音识别系统将是p d a 人机交互界面的主导。 除了上文所述的应用领域外，声音识别技术在其他方面的应用也是不胜枚 举，随着这项技术的同渐提高，将为人们带来巨大的益处。 1 3 2 2 进程代数c s p 2 2 1c s p 背景介绍 随着计算机系统的不断扩大，其功能也日趋的复杂，导致系统出现问题和不 确定性的几率也越来越高。对系统的维护变得更加的困难。为了提高系统的可靠 性，对系统进行严格的验证愈加重要，也受到了广泛的关注。 我们都知道，多数的i t 系统，不论是在研究领域或是在生产过程中，其实 现高层需求控制目标是结合经验和验证来完成的。传统的验证方法通过实验的方 法对系统进行查错，在系统的某个切入点给予输入，观察在另一点的输出，从而 验证系统是否有错误存在。但是如今的大型并发系统，会同时协调调度多个独立 的组成部分，在执行过程中，不确定性使得系统变的更为复杂，因此传统的方法 难以对发系统进行验证。在设计和开发分布式并发系统的时候，人们通常采用科 学严谨的形式化验证方法来进行验证口1 2 1 引。 形式化方法对现实世界进行形式化的描述，在此基础上，对系统的性质进行 验证。其中主要包括演绎验证和模型检测。演绎验证是将系统的性质用逻辑公式 表述出来，再从公理出发，推导出这些逻辑表达式，从而实现对性质的验证。模 型检验则是对系统状态空间进行穷尽搜索，从而完成性质验证。形式化方法中包 含很多种形式化语言，如进程代数，时序逻辑语言等等。 进程代数是将系统进行抽象，描述系统中各个组件之间的交互通信。经常在 并发式系统和分布式系统中使用。进程代数在处理并发进程时，将多个并发进程 看做一个进程的行为的所有可能的组合。从而将并发处理为非确定性选择。进程 代数主要分为三个流派：c s p ( c o m m 1 i c a t i n gs e q u e n t i a lp r o c e s s e s ，通信顺序 进程) ，c c s ( c a l c u l u so f c o m m u n i c a t i n gs y s t e m s ，通信系统演算) ，a c p ( a l g e b r a o fc o m m l m i c a t i n gp r o c e s s e s ，通信进程代数) 1 5 3 。 c c s 是m i l n e r 在19 8 0 年提出的。其主要特征是将系统进程用基本的算子表 达出来，从而得到简单的模型。同时，c c s 可以针对进程行为的等价性进行刻 画，利用这个特点，我们可以验证系统实现是否满足需求。 a c p 是j a n b e r g s t r a 等人在1 9 8 2 年提出的。相对于c c s 和c s p 来说，a c p 主要针对递归方程运算进行研究，更加注重对系统的抽象 c s p 是c a r h o a r e 在1 9 7 8 年提出的并行理论，作为一种形式化方法，被 1 4 广泛的应用于并发系统及分布式系统中。分布式系统很复杂，它包含了很多个组 成部分，这些部分可能同时的执行，并且这些部分之间通讯交互方法的结合使用， 使分布式系统更加的复杂。对于这样的系统的设计，需要能够控制这些交互。 系统中的并发性会引起很多问题，如死锁和活锁。当系统中的一些组成部分 在等待使其能够继续执行的交互或者信息的时候，死锁可能发生。活锁则是组成 部分进入了一个无穷的相互交互的循环。这些问题不是由独立的组成部分引发 的，而是和他们的组成方式有关。与此同时，非确定性同样会由并发的组成部分 引发，例如，当出现竞争情况时。 在对并发问题和复杂的分布式系统的理解上，c s p 起到了很大的积极作用。 并提供了一种能够使需求规范和设计清楚的表达和理解的符号和方法，使其可以 分析并证明需求规范和设计的正确性。 c s p 语言描述组件与组件之间的交互，并且其有基本的理论来支持验证。c s p 构架的理念是将组件或者进程看作是独立的实体，并且拥有特定的接口，通过这 些接口，这些组件与周围的环境进行交互。这便是c s p 用来分析世界的构架。 c s p 语言在开发过程中的不同阶段都可以进行系统描述： 需求规范描述了系统或者组成部分需要或者期望的行为。这些c s p 语言可以 表达出来；设计则注重以怎样的方式将各个部件结合起来，提供一个能够达到特 定需求规范的系统；实现部分指那些可以直接转化成编程代码的c s p 。 这些层次不是严格定义的，很难准确的说一个c s p 描述是需求规范还是抽象 的设计，或者是详细的设计还是一个实现。我们可以从需求到实现阶梯式的进行。 在整个过程中使用一种语言的好处在于描述的不同层次可以进行比较并且同时 属于一个构架。 c s p 语言的符号可以在不同的层次使用。并行符号可以用在需求规范中，表 示组成，在设计层可以用来表示并行构架，在实现层可以表示进程必须同步。内 部选择在需求规范层次可以表示多种可能性，在设计层可以表明完成一项服务， 有多种可达的方法，在实现层则可以表示运行中的不确定性。还有其他一些c s p 符号，只在开发过程中的某个阶段适用。 c s p 语言从刚刚出现开始不断的进化，现在可以利用进程分析工具p a t 对其 进行验证，并且在原有的c s p 符号基础上增加新的符号，使语言的表达能力更 加强大i i 4 j 。 2 2 2c s p 语法简介 一个c s p 进程描述为通过通信与其他进程或者外部环境相互交互，一个进 程是一系列的动作。c s p 还提供了一种描述进程可达状态的方法。为了帮助理解， 下面列出c s p 中关于处理进程的相关运算符。 a - p 表示系统先执行动作a ，之后再进行p 操作。 p i i q 表示进程p 与q 并行。这两个进程通过共同的动作来达到同步。 p 川q 表示进程p 与q 并发交错。执行的过程中，p 与q 不进行交互，相互间 没有关联。 p ；q 表示进程p 与q 顺序执行。当p j i 顷利完成后，q 进程开始。 c ? x 表示通道c 上输入x 。 c ! x 表示通道c 上输出x 。 s k i p 表示进程成功终止。 s t o p 表示进程死锁。 x 一 p i y 一 q 表示系统执行x 一 p 或者y 一 q 。实际如何选择，取决于在运行中动 作x 和y 哪个发生。 u x f ( x ) 用来表示循环体。其中x 为进程。 c a s ed o 表示当c a s e 语句后面的条件成立的时候，系统所进行的操作。 peq 表示( 确定性) 进程q 能完成p 能完成的任务。 ( 非确定性) 进程q 能如p 一样或更好完成任务。 在上述理论的基础上，第一位基于信息系统，在形式化理论上迈出步伐的是 z 锄b o n e l l i 和o m i c i n i 。他们将世界分为三个层次，系统层，交互层，和实体层。 这样，便将复杂的系统一层一层的剖析开来，正如物理学的研究方式。系统中的 每个组成部分都有自己确定的任务目标，这样的技术在面向对象的系统中，能够 被很好的运用。在这里我们所运用的由上至下的分析方法有一个特点，及同一个 性质，在一个层次中可能被认为是原子操作，而在另外的层次罩有可能被分解为 多个。这种思想在之前就已经有过先例。在整个系统中，每个组成部分我们将其 看为一个单元实体，每个实体都可以和周围直接相邻或者间接相邻的邻居实体进 行交互，并且可以存储信息。所有的实体节点组成了一个联系网，这样确保了实 体可以通过一个交互序列实现与另外一个实体间的通讯【1 2 13 1 。 这是将形式化方法运用于传统的信息系统的一个简单的例子。那么形式化方 1 6 法也适用于自动化计算系统吗? 本文将基于d m u 江系统，对其三个自动化性 质：自保护，自优化，自恢复进行建模，并在这些形式化模型基础上，对性质进 行验证。 2 3 脚麒 p r o c e s sa n a l y s i st o o l k i t ( p a t ) 由新加坡国立大学研发而成，是一个支持对实 时，并行系统进行仿真，分析的工具。它的主要组成部分包括用户界面，性质模 型编辑器和仿真器。w 汀实现了多种模型检验的技术，能够对于死锁，可达性， l t l ，精化等进行验证。 p a t 的主要功能如下： 提供支持多种语言的编辑环境，用以引入模型。 提供用以仿真系统行为的仿真器。可以自动仿真，用户引导仿真，生 成完整的状态图，展现仃a c e 路径等。 能够进行死锁分析，可达性分析，时序逻辑检验和精化验证。 给出了多个内设的例子，以便用户参考。 p a t 是一个可扩展的工具，允许用户建立自定义的模型检验器。在工具里提 供了模型检验算法的库，并且支持用户自定义语言语义，语法，算法等。目前 p a t 能够在1 1 种模型中使用：实时系统，网络服务模型，传感器网络等。目前， p a t 已积极的进行自动化系统的形式化分析技术的研究。 运用p a t 进行模型检验，需要使用p a t 特定的语言。下面我们简单的介绍p a t 中的主要语法。 m o d e ln 锄e 模型名称的定义： m o d e ln 硼e c o n s t a n t s 常量的定义：# d e f i n em a x5 ：定义了常量m a x ，其值为5 。 v a r i a b l e s a r r a y s 变量和数组的定义： v a rk n i g h t = 0 ：定义了变量k n i g h t ，其初始值为0 。 v a rb o a r d = 3 ，5 ，6 ，o ，2 ，7 ，8 ，4 ，1 ：定义了数组b o a r d ，其初 始元素为3 ，5 ，6 ，o ，2 ，7 ，8 ，4 ，l 。 v a rl e a d e r 3 ：定义了数组1 e a d e r ，长度为3 ，初始元素均为0 。 1 7 u s e rd e f i n e dt y p e 用户自定义类型： v a r x ：t y p e 类的默认构造函数被调用。 v a r x = n e wt y p e ( 1 ，2 ) ：带有两个i n t 类型参数的构造函数被 调用。 c h a n n e l s 通道的定义： c h a n n e lc5 ：c 为c h a n n e l 的名称，5 为此通道中同时 可以接受发送的消息数目。 p r o p o s i t i o n s 前提条件的设置：# d e f i n eg o