（计算机应用技术专业论文）基于进程代数和模型检验的系统建模与评价.pdf

摘要 性能评价的目的是描述和分析系统的动态及与时间有关的行为。尽早将功能、时序行为检验与设计相 结合，可以在很大程度上消除不必要的错误，提高设计质量。评价模型常采用变迁模型描述系统的动态行 为在实时系统性能( 包括可靠性) 的分析中，连续时间马尔可夫链模型被得到广泛应用。但目前软件系 统和硬件系统的规模和复杂度增长迅速，企图直接获得系统的马尔可夫模型极为繁琐且易出错，这就需要 一种合适的建模技术，能形式化地描述系统且易获得系统的马尔可夫模型。而进程代数面向行为，提供了 结构化操作语义，可借助自动推理展开状态空间，无需直接面对状态，同时具有很自然的合成和抽象的能 力，能有效压缩状态空问，更可将进程代数模型映射到带标号的变迁系统，从而可方便地获得马尔可夫模 型，因此进程代数成为复杂系统性能评价的建模利器。 在进行性能评价时，获取如失效时闻、系统吞吐量和利用率等性能指标是一件很棘手的工作，且基本 上是非形式化的、非专用的方法。因此通常只有一些基于状态的度量相对简单一点基于时序逻辑的模型 检验可以很好地解决这个问题。模型检验是一种自动验证方法，避免建立复杂的证明过程，并在规格说明 不满足系统模型的要求时能提供反例。目前很多实时系统性能评价的工作基于连续时问马尔可夫链，直接 分析实时系统获得性能参数是非常困难的事情，因此需要在建模和性能评价之间搭建一个桥梁，能很好地 结合实时系统的形式化建模和实时系统的性能评价分析这两种技术，降低性能评价复杂度，提高效率将 进程代数与模型检验相结合，可以解决传统性能评价工作中若干难点，例如：建模困难且易出错，描述不 规范，缺乏合成和抽象的能力，难以进行基于路径的度量等等，本文就并发系统的进程代数建模与实时随 机系统的模型检验作了一定的研究 使用进程代数描述了a d a 会合机制，a d a 保护对象及j a v a 多线程机制，并提出了一种基于进程代数的 a d a 并发程序静态死锁检测方法文中详细分析了会合通信，在每条导向同步的控制边附加一个代理 同步通信过程的通信原子动作，从而构造了进程代数会合机制模型再根据会合通信进程代数模型 原理对源程序逐层扫描，提出了一种新的扫描源程序的层操作算法，实现了a d a 并发程序到进程代数形 式化描述的转换，并在转换过程中，通过进程代数的自动等价推导代数表达式以模拟运行，找出系统中 可能触发死锁的死通信，进一步结合控制依赖分析死通信的各类组合情况，检测出潜在的死锁环路。这 种a d a 并发程序的静态死锁检测方法的最大优势是能利用进程代数的形式化建模和自动等价推理，并在 需要时通过合成和抽象降低状态空间。由于进程代数具有很强的处理抽象，过程合成及隐藏内部细节的 能力，因此以进程代数形式化系统为基础，可支持我们在可达性分析、依赖性分析、通信关系分析、切 片分析及控制流分析等领域的研究。 提出一种带动作标号的随机变迁系统a l s t s ( a c t i o l ll a b e l e ds t o c h a s t i ct r a n s i t i o ns y s t e m ) 及其扩展 a l s t s ，并对a l s t s 系统进行随机进程代数建模与隐马尔可夫模型分析应用。文中提出的带动作标号 的随机变迁系统( a l s t s ) 包含动作和随机时间信息，可用于表达系统的变迁行为、时序信息、概率特 征及随机性，a l s t s 的每个状态可对应连续时间马尔可夫链( c t m c ) 的一个节点，状态之间的变迁对 应c t m c 节点之间的弧，从而可获得用于性能评价的转换速率矩阵。由于系统往往会因各种缺陷或误差 等面失效，因此将a l s t s 系统扩展为a l s t s 系统，允许状态内原子命题服从一定的概率分布，使德系 统包含双重随机特性。随后使用随机进程代数对a l s t s 系统进行了建模。本文还依据a l s t s 系统的概 率特性和随机性进行了隐马尔可夫模型的分析，提供的随机分析参考可辅助测试人员对实时系统进行黑 盒观测，例如，在设计测试用例时，根据若干次观测，可以估得该测试用例对路径的覆盖率，进而调整 测试用例，修正覆盖率，对重点模块增强覆盖；也可根据若干次观测，估得下一次系统最可能的执行路 径，从而能加快调试定位。正因为建立了这样的隐马尔可夫模型，使得很多分析测试成为可能或更为便 捷。且对于非常复杂的黑盒系统，可以结合进程代数的合成能力采用逐步分解的方法来进行观测分析。 提出了一种基于迹的连续随机时序逻辑t c s l ( t r a c eb a s e dc o n t i n o u ss t o c h a s t i cl o 西c ) ，并给出了a l s t s 系统从随机进程代数建模到t c s l 模型检验的性能评价方法c s l ( c o n t i n u o u ss t o c h a s t i cl o g i c ) 时序逻 辑不含动作的概念，因此无法针对变迁动作进行分析。a c s l ( a c t i o nl a b e l e dc o n t i n u o u ss t o c h a s t i cl o g i c ) 虽然可以分析变迁过程中的动作，但不能分析动作的执行顺序，本文在c s l 和a c s l 的基础上增加了动 作的概念、关键路径的概念及迹关键动作的概念，描述了t c s l 的词法和语义。对不限时与限时的。n e x t ” 和“u n t i l ”时序操作给出了基于关键路径和关键动作的稳态概率分析，重点阐述了针对路径的t c s l 模 型检验的方法，并通过实例分析，结合a l s t s 系统的随机进程代数建模，实现了对关键动作序列有要 求的路径相关的系统性能评价。并给出了t c s l 模型检验平台支撑工具原型。 借助迹关键动作和瞬时内部动作，给出了种非确定性随机系统向a l s t s 系统转换的方法，从而可使 用t c s l 模型检验方法对重构后的非确定性系统进行路径相关的系统性能评价。本文还提出了迹互模拟 等价的概念，给出了迹瓦模拟等价性定理。利用迹互模拟等价性，可对系统的状态窄问进行压缩，并能 保留关键路径和关键动作的信息。 关键词进程代数、模型检验，并发、随机、马尔可夫模型 a b s t r a c t t h ei n t e n t i o no f p e r f o r m a n c ee v a l u a t i o ni st od e s c r i b ea n da n a l y z et h es y s t e m s d y n a m i ca n dt i m er e l a t e d b e h a v i o r s t h es o o n e ru s i n gf u n c t i o n a la n dt e m p o r a lb e h a v i o rc h e c k i n gi nt h ed e s i g np h a s e ，t h eb o r e rq u a l i t yw e g e tw i t hf e w e rd e f e c t s u s u a l l ye v a l u a t i o nm o d e l sa t es o m e k i i n do f t r a n s i t i o nm o d e l sw h i c ha r eu s e dt od e s c r i b e s y s t e m sd y n a m i cb e h a v i o r s i np r a c t i c a l ，s y s t e mp e r f o r m a n c ea n a l y z i n g , i n c l u d i n gr e l i a b i l i t ya n a l y z i n g , m a r k o v c h a i ni sw i d e l yu s e d p a r t i c u l a r l yc o n t i n u o u sm a r k o vc h a i ni nm o s tr e a lt i m es y s t e m s w i t hr a p i d l yi n c r e a s e d s c a l ea n dc o m p l e x i t yo f s o f t w a r ea n dh a r d w a r e s y s t e m s ，d i r e c t l ya c q u i r i n gm a r k o v i a nm o d e l si sr a t h e ru n l i k e l y a n de r r o rp r o n e ，s oh i g h e rl e v e lm o d e l i n gt e c h n i q u e sa r er e q u i r e d p r o c e s sa l g e b r am o d e l sa r eb e h a v i o ro r i e n t e d , h a v i n gt h ea b i l i t yo f s u p p o r t i n gs t r u c t u r a lo p e r a t i o n a ls e m a n t i c s ，s y s t e mc o m p o s i t i o na n da b s t r a c t i o n i tc a n e x p a n ds t a t es p a c ea u t o m a t i c a l l yw i t ht h eh e l po f p r o c e s sd e d u c t i o n f u r t h e r m o r e , i tc a nm a pp r o c e s sa l g e b r a m o d e l st ol a b e l e dt r a n s i t i o ns y s t e m s ，s ot h a tm a r k o v i a nm o d e l sc a nb ea c q u i r e de a s i l y t h u sp r o c e s sa l g e b r ai sa p o w e r f u lm o d e l i n gt o o lf u rc o m p l e xs y s t e mp e r f o r m a n c ee v a l u a t i o n d u r i n gp e r f o r m a n c ee v a l u a t i o n , a c q u i r i n gp e r f o r m a n c em e t r i c s , s u c ha sf a i l u r et i m e ，s y s t e mt h r o u g h p u ta n d s y s t e mu t i l i z a t i o nr a t i o ，i sah e a v yw o r k , b e c a u s eo ft h eu s u a li n f o r m a la n dn o n s p e c i f i cm e t h o d s o n l ys t a t e o r i e n t e dm e a s u r e sa r cr e l a t i v e l ys i m p l e h o w e v e r , b a s e do nt e m p o r a ll o g i c ，m o d e lc h e c k i n gt e c h n i q u ei sag o o d a s s i s t a n c e m o d e lc h e c k i n gi sa na u t o m a t e dv e r i f i c a t i o n m e t h o d ，a v o i d i n gc o m p l e xf o r m u l ap r o v i n g , a n d p r o v i d i n gc o t m t e r e x a m p l ew h e np r o p o s i t i o n sa r en o ts a t i s f i e d m o s ts y s t e mp e r f o r m a n c ee v a l u a t i o nm o d e l sa r e b a s e d 伽c o n t i n u o u st i m em a r k o vc h a i n ( c t m c ) ，w h i c hi sn o t 锄e a s yj o bd i r e c t l yd e a l i n gw i t hr e a lt i m e s y s t e m s w h e nu s i n gt r a d i t i o n a lm e t h o d s t oc a r r yp e r f o r m a n c ee v a l u a t i o n , w ed on o th a v et h ec a p a b i l i t yo f f o r m a l s p e c i f i c a t i o n c o m p o s i t i o na n da b s t r a c t i o n s oi ti sah a r dw o r kt og e tt h er i g h ta n dp r o p e rm o d e lo ft h es y s t e m f u r t h e r m o r e ，s o m em e a s u r e m e n t ss u c ha st h o s eb a s e do np a t hc a l lb ev e r yh a r dt oo b t a i n h o w e v e r , t e c h n i q u e s c o m b i n i n gp r o c e s sa l g e b r aw i t hm o d e lc h e c k i n gh a v eg r e a ta d v a n t a g ei nt h e 锄慨o fp e r f o r m a n c ee v a l u a t i o n c o m p a r e dt ot r a d i t i o n a lm e t h o d s , w h i c hw i l lb ed i s c u s s e di nt h i st h e s i s p r o c e s sa l g e b r ai sa d o p t e dt om o d e la d ar e n d e z v o u s ，a d ap r o t e c t e do b j e c t sa n dj a v at h r e a d s a l s oan e w a p p r o a c ho fs t a t i cd e a d l o c kd e t e c t i o no fa d ac o n c u r r e n tp r o g r a m si sp r o p o s e d i nt h i st h e s i s ，d e t a i l e d r e n d e z v o u sc o m m u n i c a t i o ni sa n a l y z e d ，a n de v e r ys y n c h r o n i z a t i o nc o n t r o le d g ei sa t t a c h e dw i t h 锄a t o m i c c o m m u n i c a t i o na c t i o nw h i c hw i l lb ei n c h a r g eo ft h ec o m m u n i c a t i o np r o c e s s b a s e d o nr e n d e z v o u s c o m m u n i c a t i o n , a l lt h ec o m m u n i c a t i o nb e h a v i o r si nt h ec o n c u r r e n tp r o g r a m sa r es i m u l a t e da n dd e d u c t e d s o u r c ef i l e sa 糟s c a n n e dl a y e rb yl a y e rw i t hah i e r a r c h i c a lo p e r a t i o na l g o r i t h m s ot h a tt r a n s f o r m a t i o nf r o ma d a c o n c u r r e n tp r o g r a m st op r o c e s sa l g e b r af o r m a ls p e c i f i c a t i o nc a l lb em a d e d u r i n gt h et r a n s f o r m a t i o n , w i t h e q u i v a l e n c ed e d u c t i o na n ds i m u l a t i o n , s o m ep a r t i c u l a rd e a dc o m m u n i c a t i o n sa r ed u go u t f u r t h e rb ya n a l y z i n g a l lk i n d so f c o m p o s i t i o n so f d e a dc o m m u n i c a t i o n sw i t hd e p e n d e n c yi n f o r m a t i o n , p o t e n t i a ld e a d l o c kc i r c l e sc a n b ed e t e c t e d t h ea d v a n t a g eo ft h i ss t a t i cd e a d l o c kd e t e c t i o na p p r o a c hi sm a k i n gf u l l yu s eo fp r o c e s sa l g e b r a f o r m a l i z e dm o d e l i n ga n da u t o m a t i cd e d u c t i o nw h i c hl a t e rc a nb e u s e dt or e d u c es l a t es p a c et h r o u g h c o m p o s i t i o na n da b s t r a c t i o n ，a n dj sv e r yh e l p f u li no u rr e s e a r c ho no t h e ra r e a s , s u c h 勰，r e u c h a b i l i t ya n a l y s i s ， d e p e n d e n c ya n a l y s i s ，c o m m u n i c a t i o na n a l y s i s ，p r o g r a ms l i c i n ga n dc o n t r o lf l o wa n a l y s i s an o wa c t i o nl a b e l e ds t o c h a s t i ct r a n s i t i o ns y s t e ma n di t se x t e n s i o n ( a l s t sa n da l s t s 1a g op r o p o s e da n d m o d e l e dw i t hs t o c h a s t i cp r o c e s sa l g e b r a ( s p a ) a l s oh i d d e nm a r k o v i a nm o d e la n a l y s i si sp e r f o r m e do n a l s t s + a l s t s i sp r e s e n t e dw i t ht h ei n t r o d u c i n go f u c t i o na n ds t o c h a s t i ct i m ei n f o r m a t i o n ，w h i c hi su s e dt o d e s c r i b et r a n s i t i o ns e q u e n c e ，t e m p o r a li n f o r m a t i o n ，s t o c h a s t i ca n dp r o h a b i l i s t i cb e h a v i o r e v e r ys t a t ei na l s t s ( a l s t s ) i sm a p p e dt oan o d ei nc o n t i n u o u st i m em a r k o vc h a i n ( c t m c ) a n de v e r yt r a n s i t i o ni na l s t s ( a l s t s ) i sm a p p e dt oa ne d g ei nc t m c ，s ot h a tg e n e r a t o rm a t r i xg a l lb eo b t a i n e d b e c a u s eo f s y s t e me r r o ro r f a i l u r e , a l s i si se x t e n d e dt oa l s t st oe x p r e s st h ep r o b a b i l i s t i cd i s t r i b u t i o no f a t o m i cp r o p o s i t i o n si ns t a t e s t h l l sa l s t s c a nb es e e na sad o u b l es t o c h a s t i cs y s t e m b a s e do na l s t s s p am o d e l i n gi sc a r r i e do u t , w h i c h c a l ld e p i c ts y s t e mb e h a v i o r sm o r ep r e c i s e l ya n dc o n v e n i e n t l y i n s t e a do fs t a t eo r i e n t e d ，b e h a v i o ro r i e n t e d m o d e l i n gp r o v i d e sab e t t e ru n d e r s t a n d i n ga n dc o n s t r u c t i n go fp e r f o r m a n c em o d e l so fr e a lt i m ec o m p l e x s y s t e m s ，t h u si ta l l e v i a t e dt h eh e a v yw o r ko f p e r f o r m a n c ea n a l y z i n g , a c c o r d i n gt ot h es p e c i a lp r o b a b i l i s t i ca n d s t o c h a s t i cc h a r a c t e r i s t i c , w e 嘴h i d d e nm a r k o vc h a i nt or e m o d e l i n ga n da n a l y z i n ga l s t s s y s t e m sf o rs o m e p r a c t i c a l 印p l i c a t i o ns c e n a r i o s , p r o v i d i n gr e f e r e n c e so fs t o c h a s t i ca n a l y s i s ，w h i c hi sv e r yh e l p f u li nb l a c kb o x t e s t i n go f l a r g ec o m p l e xr e a lt i m es y s t e m s t r a c eb a s e dc o n t i n u o u ss t o c h a s t i cl o g i c ( t c s l ) i sp r o p o s e dw i t ht h en o t i o no f c r i t i c a lp a t ha n dc r i t i c a la c t i o n , a n dap e r f o r m a n c ee v a l u a t i o na p p r o a c hf r o ma l s t s s p am o d e l i n gt ot c s lm o d e lc h e c k i n gi sp r e s e n t e d c o n t i n u o u ss t o c h a s t i cl o g i c ( c s l ) d o e sn o th a v et h ea b i l i t yt oe x p r e s sa c t i o n s ，t h u sc a n n o tb eu s e dt oa n a l y z e t r a u s i t i o na c t i o n s m 订ea c t i o nl a b e l e dc o n t i n u o u ss t o c h a s t i cl o g i c ( a c s l ) c a nd os o b u ti tc a n n o ta n a l y z e t h ea c t i o ns e q u e n c e sa l o n gt h et r a n s i t i o np a t h i n t r o d u c e dw i t ht h en o t i o n so fc r i t i c a lp a t ha n dc r i t i c a la c t i o n s ， t c s li sf o c u s e do nt r a c i n ga n da n a l y z i n gt h es e q u e n c eo fc r i t i c a la c t i o n sd u r i n gt r a n s i t i o n , w h i c he n r i c h e d s e m a n t i c so fc s l t c s ls y n t a xa n ds e m a n t i ca r ed e s c r i b e d u n t i m e da n dt i m e d n e x t u n t i l ”t e m p o r a l o p e r a t i o n sb a s e do nc r i t i c a la c t i o n sa r ea l s oe l a b o r a t e d h e r ew ep r o p o s e dt h et c s lm o d e lc h e c k i n gt e c h n i q u e t o g e t h e rw i t ht h es t o c h a s t i cp r o c e s sa l g e b r am o d e l i n go fa l s t s ，w ee l a b o r a t e daw a yf r o ma l s t s f o r m a l m o d e l i n gt op e r f o r m a n c ee v a l u a t i o n w i t ht h eh e l po ft r a c eb a s e dc r i t i c a la c t i o n sa n di n s t a n t a n e o u si n t e r n a la c t i o n s ，an e wa p p r o a c hi sp r e s e n t e dt o t r a n s f o r mn o n d e t e r m i n i s t i cs y s t e m st oa l s t s ，s ot h a tp e r f o r m a n c ee v a l u a t i o nt h r o u g hs t o c h a s t i cp r o c e s s a l g e b r am o d e l i n ga n dm o d e lc h e c k i n gc a nb ep e r f o r m e d ，w ea l s op r o p o s e dt h ed e f i n i t i o na n dt h e o r e mo f t r a c e b a s o db i s i m u l a t i o ni n s p i r o db ym a r k o v i a nb i s i m u l a t i o n 。i tc a ne x p r e s ss e n s i t i v eb e h a v i o r sa n dt r a c ec r i t i c a l a c t i o n s ，a sw e l la sp r e s e r v et h eo u t s t a n d i n ga b i l i t yo f s t a t es p a c er e d u c t i o nb yu s i n gm a r k o v i a nb i s i m u l a t i o n k e y w o r d j ：p r o c e s sa l g e h - , l m o d e lc h e c k i n g , c o n c u r r e n t , s t o c h a s t i c ，m a r k o v i a nm o d e l 东南大学学位论文 独创性声明及使用授权说明 一、学位论文独创性声明 本人声明所呈交的学位论文是我个人在导师指导下进行的研究工作及取得 的研究成果。尽我所知，除了文中特别加以标注和致谢的地方外，论文中不包 含其他入已经发表或撰写过的研究成果，也不包含为获得东南大学或其它教育 机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何 贡献均已在论文中作了明确的说明并表示了谢意。 二、关于学位论文使用授权的说明 8 一t 一厂 东南大学、中国科学技术信息研究所、国家图书馆有权保留本人所送交学 位论文的复印件和电子文档，可以采用影印、缩印或其它复制手段保存论文。 本人电子文档的内容和纸质论文的内容相一致。除在保密期内的保密论文外， 允许论文被查阅和借阅，可以公布( 包括刊登) 论文的全部或部分内容。论文 的公布( 包括刊登) 授权东南大学研 签名：毯l 匿l 导师签名： 期： 伊呓一1 4 c 1 东南大学博士学位论文 1 1 选题依据 第一章引言 随着计算机技术的飞速发展，无论是软件系统，还是硬件系统，都日趋庞大、复杂一个火控软件发 生异常的频率多高? 一台路由器能保证在任何时候丢包率都小于0 o l 吗? 这些性能( 包括可靠性) 一直以来都是人们关心的问题。性能评价就是指描述和分析系统的动态及与时间有关的行为。性能评价可 以有效地发现系统的不足之处，从而指导对系统的改进和完善。 通常来说，绝大多数系统在设计完毕及结束功能测试后，甚至在系统实现后才进行很少的性能指标的 评价，很多中小企业甚至不进行任何评价工作，导致在开发结束后。需要付出巨大代价对软硬件系统进行 改进甚至重新设计，以致于常常延期交货。因此，性能评价应该与设计| 一步，尽可能早地将功能、时序行 为检验与设计相结合，及早消除错误，提高设计质量，降低开发代价。 这种思想在上世纪七十年代就早已得到认可和重视。当时最成功的评价模型有随机p e t r i 网，随机图模 型和随机自动机两络。然而只有很少的专家才能掌握这些方法，同时缺少成熟的支持工具，以及其自身一 些周有的弱点，并不很实用。例如排队网络支持合成但不支持形式化，随机p e t r i 网支持形式化，但不支持 合成和近似分析，且两者都不支持抽象。 一般来说，评价模型采用的都是某种( 带标号的) 变迁模型( 或自动机，一般来说，一个变迁系统和 某种自动机1 7 0 , 7 1 j 1 q 是等价的) 多年以来，各种各样的变迁模型或类似豹图表被广泛用于描述系统的动态 行为。自从上世纪八十年代，进程代数理论逐渐成熟。进程代数【1 1 提供了结构化操作语义，可以将代数项 映射到带标号的变迁系统，同时具有很自然的合成和抽象能力，为复杂系统建模带来了希望。以往的一些 变迁系统都是基于状态的，使用者需要了解和跟踪复杂的状态变迁和进程通信，而进程代数面向行为，更 贴近人的思维分析模式，且可以对并发和交互的进程进行严格的数学推理l i z 0 , 1 “，借助工具可以实现自动 推理和分析，因而使用起来更方便。从上世纪九十年代开始，一些学者开始深入研究进程代数及各种扩展 及应用1 3 , 5 7 , s 9 , “t 1 4 i ，1 5 ”，为性能评价的模型建立工作打下了坚实的基础。 在实际系统性能( 包括可靠性) 的分析中【7 l m c ( 马尔可夫链) 被得到广泛应用t 2 7 4 2 】，其中大多数实 时领域都采用了c t m c ( 连续时间马尔可夫链) i s 。但目前软件系统和硬件系统的规模和复杂度增长迅速 企图直接获得系统的m c 模型需要人工分析和跟踪复杂系统内部的状态变迁矩阵，极为繁琐且易出错，这 就需要一种合适的建模技术，能形式化地描述系统，自动推演和映射，从而方便地获得系统的马尔可夫模 型。进程代数能很方便地提供精确的、模块化的形式化规格说明，用来描述m c 。且进程代数中的强互模 拟与m c 中的划分相一致，从而可以将m c 的划分计算转换为进程代数的强互模拟计算( 有一些成熟的算 法) ，使得m c 状态空间的约简完全自动化l ，就好像是构件的合成。这种机制保证了在预先生成状态宅 问时，可以不必生成全部状态空间，在绝大多数情况下能极大地缩减状态窄间。作为副产品，在获得m c 模型的同时，可以利用进程代数对系统进行定性评价。 一般来说，在得到m c 模型后，先指定精确度，再对某螳特定性能指标进行定鼙评价，如失效时间， 系统吞吐量和利用率等。然而对这蝮特定指标进行评价是件很棘手的工作，常规方法都是避非形式化的， 专用的，一般来说，只有一些基于状态的度量可以相对简单地解决，如稳态和瞬时概率。基1 ：时序逻辑的 模型检验咿1 5 ”“】可以很好地解决这个问题h 8 舯, 6 2 , 6 3 , 6 6 , 7 4 , 8 2 , 1 0 3 , 1 0 6 , 1 5 3 , 1 7 3 1 。模型检验是一种自动验证 1 6 5 , 1 6 9 1 系统 能否满足特定性质的方法1 ”川，可以避免建立复杂的证明过程，并能在不满足系统模型的要求时提供反例。 这里，模型检验的基本思想是以c t l ( 一种分支时序逻辑) 为基础( 现有很多扩展 ，将m c 扩展为带标 签的m c ，即每个状态都附上一个原子命题集，从而将特定指标的度量转化为对满足某些原子命题的状态 的检查。采用模型检验最根本的优点有两条；一是形式化，以清晰、简洁、灵活、统一的方式说明那些特 东南大学l 礴士学位论文 定的指标，统一了说明方式：二是做到了完全自动化的检查，模犁榆验通常采用状态宅间的完全自动搜索， 但这会牵涉到状态窄问爆炸问题，目前已有一定的研究，并且在某些领域已能较好地解决实际问题 4 5 , 1 5 2 l 。 目前已有许多大公司，如i n t e l ，a t & t ，m o t o r o l a ，l u c e n t 和s i e m e n s 等，把模型检验作为设计过程的一 部分。 凶此，结合进程代数和模型检验i ”, 6 u s l ，在性能评价领域中有着很大的优势。本课题旨在研究如何基 于进程代数和模型检验进行性能评价，并探讨如何更好地融合这两种技术 1 2 国内外研究现状 虽然从上世纪七十年代就开始性能建模和评价的研究，但很长一段时间都只是停留在理论阶段，很多 模型和评价方法并不实用。直到卜世纪九十年代，随着一1 些新理论( 如随机进程代数和模型榆验) 的建立 和发展，性能建模和评价的实用化成为可能。以这些理论为基础，出现了_ 一些支持工具，在某些方面能有 效解决非常复杂的实际工程问题。 若要对系统进行性能评价，首先必须建立系统的评价模型。通常评价模型采用的都是某种( 带标号的) 变迁模型。由于普通的变迁系统不足以表达非确定性的、实时的、概率【7 9 】的或随机的系统，不适合于描述 分布式和并发系统，因此通常是在带标号的变迁系统基础上引入附加信息，扩展原有的表达能力。在实际 性能评价中，马尔可夫链【4 7 l 得到了广泛的应用。物理学、牛物学、运筹学、自动控制【1 7 1 、通信嘲和计算机 科学等f i 同的领域使用不同类趔的马尔可夫模氆。一般的有d t m c 、c t m c 、m d p ( m a d ( m rd e c i s i o np r o c e s s e s ) 【1 5 9 , 1 7 7 】及m r m ( m a r k o vr e w a r dm o d e l s ) 【“j a , 1 2 7 j 蚓。通常，马尔可夫模型中的状态由带标号的有向变迁 边所连接，这就和带标号的变迁模型非常相象。在d t m c ( 离散时间马尔可夫链) 中标号为概率，而在 c t m c ( 连续时间马尔可夫链) 中，标号为速率用以表示成指数分布的随机延时。因此马尔可夫模型可 被表示成某种变迁系统或自动机。目前已有不少变迁系统支持不同的马尔可夫模型。比较有代表性的有 j o n s s o n 等提出的一种概率变迁系统( p r o b a b i l i s t i ct r a n s i t i o ns y s t e m s ) f 3 l l ，其中强调区分了概率性和非确 定性这两种不同的概念。该模型本质卜来说就是一种非确定性的马尔可夫决策过程( m d p ) | 2 6 1 或种概率 r a b i n 自动机。b i a n c o 等提出一种概率系统一非确定性系统( p r o b a b i l i s t i c - n o n d e t e r m i n i s t i cs y s t e m s ) ，在该 模型中，非确定性和概率两种行为共存。但是这两种模型都不涉及实时信息，因而不能描述随机系统。a l f a r o 等引入了随机变迁系统( s t o c h a s t i ct r a n s i t i o ns y s t e m s ) 1 1 4 2 的概念，提供了对时b j 概率系统的更高层次的 形式化建模，可以表示具有不确定延时分布的变迁( 指变迁本身) ，以及具有零或指数分布延时的变迁的 发生，并且统一表示了非确定性、概率口9 1 、随机、公平性及时间这几项属性。虽然该系统引入了时间因素， 但并不能真正表示实时系统。s e g a t a 等则提出了概率自动机( p r o b a b i l i s t i ca u t o m a t a ) 用于描述概率实时 系统。a l u r 等提出了带有时钟的时间自动机( t i m e d a u t o m a t a ) 1 4 9 1 ，能处理非确定性的实时系统，k w i a t k o w s k a 等在此基础上进行了概率扩充，提出了概率时问自动机( p r o b a b i l i s t i ct i m e da u t o m a t a ) s q 。a r g e n i o 等提 出了随机自动机( s t o c h a s t i c a u t o m a l a ) ，结合了时问自动机和广义半马尔可夫链。舳年代初，m o l l o y 提出 了随机p e t d 网( s t o c h a s t i cp e t r in e t s ，s p n ) l ”、1 9 8 4 年m a r s a n 等人提出了广义随机p e t r i 网( g e n e r a l i z e d s t o c h a s t i c p e t r i n e t s ，g s p n ) 和1 9 8 6 年林闯等人提出了随机高级p e t r i 网( s t o c h a s t i ch i g n l e v e lp e t d n e t s ， s h l p n ) 在p e t r i 。9 摹础上引入了时间参数，并4 i 破坏原p e 埘州结构的描述和特性的分析。还有一些其 它的变迁系统，但几乎没有种系统能同时描述非确定性、实时性