《实时模型检测中精确加速的研究》由会员分享，可在线阅读，更多相关《实时模型检测中精确加速的研究（60页珍藏版）》请在金锄头文库上搜索。
1、At h e s i ss u b m i t t e dt o Z h e n g z h o uU n i v e r s i t y f o rt h ed e g r e eo fM a s t e r I SS 7 0 72 S t u d yo n E x a c tA c c e l e r a t i o no f R e a l - T i m eM o d e lC h e c k i n g B yC h u a n l o n g Y i n S u p e r v i s o r ：P r o f L e iZ h u a n g C o m p u t e r S
2、o f t w a r ea n dT h e o r y S c h o o lo fI n f o r m a t i o nE n g i n e e r i n g M a y 2 0 1 0 原创性声明 本人郑重声明：所呈交的学位论文，是本人在导师的指导下，独立进行研 究所取得的成果。除文中已经注明引用的内容外，本论文不包含任何其他个人 或集体已经发表或撰写过的科研成果。对本文的研究作出重要贡献的个人和集 体，均已在文中以明确方式标明。本声明的法律责任由本人承担。 学位论文作者：尹传龙日期：彬年妫。日 学位论文使用授权声明 本人在导师指导下完成的论文及相关的职务作品，知识产权归属郑州
3、大学。 根据郑州大学有关保留、使用学位论文的规定，同意学校保留或向国家有关部 门或机构送交论文的复印件和电子版，允许论文被查阅和借阅；本人授权郑州 大学可以将本学位论文的全部或部分编入有关数据库进行检索，可以采用影印、 缩印或者其他复制手段保存论文和汇编本学位论文。本人离校后发表、使用学 位论文或与该学位论文直接相关的学术论文或成果时，第一署名单位仍然为郑 州大学。保密论文在解密后应遵守此规定。 学位论文懈穸磅蔻 日期：彬年；- n 岁口同 摘要 摘要 实时系统经常会出现不同的时间度量。然而，当这些系统建模成时间自动 机，然后运用符号模型检测技术进行验证时，验证速度会由于不必要的符号状 态空间
4、分裂( 片段问题) 而明显下降。 精确加速可以解决由于不同时间度量而造成的模型检测时出现的片段问 题，而且它不改变时间自动机的可达性，并可以有效地加速前向符号可达性分 析。本文中，我们对精确加速原理进行了剖析，提出了一种基于驻留环实现精 确加速的方法，解决了原来精确加速中附加环的大小需要依赖于可加速环窗口 的问题，使得时间自动机精确加速模型的构造更加的简单快捷。同时我们还利 用得出的推论，探讨了一种快速计算驻留环边界条件的方法，虽延时了加速的 时机，但避免了可加速环窗口的复杂计算。 此外，为了实现精确加速，还提出了一种识别时间自动机中可加速环的方 法。针对时间自动机规模较大的问题，在识别可加速
5、环的方法中引入拓扑排序 的思想，通过简化时间自动机的规模，提高了识别时间自动机中可加速环的效 率。通过实例验证和复杂度分析说明该方法是可行的。 关键字：模型检测；时间自动机；精确加速；可加速环；窗口；回路 A b s t r a c t A b s t r a c t D i f f e r e n tt i m es c a l e sd oo f t e no c c u ri nr e a l - t i m es y s t e m s H o w e v e r , w h e nt h e s e s y s t e m sa r em o d e l e da s ( n e t
6、 w o r k so f ) t i m e da u t o m a t a ，t h ev a l i d a t i o nu s i n gs y m b o l i c m o d e lc h e c k i n g t e c h n i q u e sc a ns i g n i f i c a n t l yb es l o w e dd o w nb yu n n e c e s s a r y f r a g m e n t a t i o no ft h es y m b o l i cs t a t es p a c e ( f r a g m e n t a t
7、i o np r o b l e m ) E x a c ta c c e l e r a t i o nc a na d d r e s st h ef r a g m e n t a t i o np r o b l e mi n t h em o d e l c h e c k i n gw h e nd i f f e r e n tt i m es c a l e so c c u ri nr e a l t i m es y s t e m s ，a n di td o e sn o ta l t e r r e a c h a b i l i t yp r o p e r t i
8、 e s ，a n da l s oc a ns p e e d - u pf o r w a r ds y m b o l i cr e a c h a b i l i t ya n a l y s i s i nas i g n i f i c a n tw a y I nt h i sp a p e r , w ep r o p o s ean e ww a yt oc o n s t r u c tt h ea d d i t i o n a l c y c l ei nt h ee x a c ta c c e l e r a t i o nt e c h n i q u e ，w
9、h i c hc a nr e s o l v et h ep r o b l e mt h a tt h es i z e o ft h ea d d i t i o n a lc y c l ed e p e n d so nt h ew i n d o wo ft h ea c c e l e r a t a b l e c y c l e ，a n d m a k i n gt h ec o n s t r u c t i o no fa d d i t i o n a lc y c l e si sm o r es i m p l e ra n dq u i c k e r W ea
10、 l s o e x p l o r eaf a s tm e t h o do fc a l c u l a t i n ge d g ec o n d i t i o n s ，t h u se s c a p et oc o m p u t et h e w i n d o wo ft h ea c c e l e r a t e dc y c l e I na d d i t i o n ，t oc a r r yo u te x a c ta c c e l e r a t i o n ，aw a yt o i d e n t i f ya c c e l e r a t a b l
11、 e c y c l e si nt i m e da u t o m a t ai sp r o p o s e d I n s p i r e db yt h et o p o l o g i c a ls o r t ，t h em e t h o d i m p r o v e st h ee f f i c i e n c yt oi d e n t i f ya c c e l e r a t a b l ec y c l e si nt i m e da u t o m a t ab y r e d u c i n gt h es i z eo ft i m e da u t o
12、 m a t a T h ev a l i d i t yo ft h i sm e t h o db ye x a m p l e sa n dt h e c o m p l e x i t ya n a l y s i si l l u m i n a t et h ef e a s i b i l i t y K e yw o r d s ：M o d e lc h e c k i n g ；T i m e da u t o m a t a ；E x a c ta c c e l e r a t i o n ；a c c e l e r a t e d c y c l e ；w i n
13、d o w ；l o o p I I 目录 摘要l A B S T R A C T ：I I l 引言1 1 1 研究背景1 1 2 研究现状2 1 3 研究内容“5 1 4 本文结构6 2时间自动机“7 2 1 相关背景7 2 2 时间自动机7 2 3 区域自动机1 0 2 3 1 区域等价1 0 2 3 2 区域自动机1 1 2 4 带自动机1 2 2 5 可达性分析1 4 2 6 小结”1 6 3 加速技术分析1 7 3 1 片段问题1 7 3 2 模型增量1 8 3 3 精确加速2 1 3 3 1 环2 2 3 3 2 可加速环2 2 3 3 3 加速”2 3 3 4 加速技术分析2 6 3 5 小结2 8 I I I 目录 4 基于驻留环的精确加速2 9 4 1 精确加速缺陷分析2 9 4 2 精确加速原理分析3 0 4 3 基于驻留环的精确加速3 1 4 4 对比分析3 4 4 5 小结3 6 5一种快速计算边界控制条件的方法3 7 5 1 窗口的计算3 7 5 2 一种快速计算边界控制条件的方法3 8
