（测试计量技术及仪器专业论文）基于有色petri网理论的并行自动测试系统建模研究.pdf

电子科技大学博士论文 中文摘要 提高自动测试系统的性能是当前测试领域的一个重要研究内容。随鬻测试设 备和测试方法静发展，传统的鑫渤溅试系统串行任务调度和系统组建方法已成 为限制系统性能的瓶颈。近年来，国内外学术界已开始进行白渤测试系统并行 任务调浚戳及自动灏试系统缝建方法静辑究，并敬褥了裙步成柒。本论文j 圣鑫 潮测试系统的并行任务调度及自动测试系统p e t r i 网建模中的若干重要问题进行 了深入、系统缝研究，援整了两释著 亍强务调凌算法秘稿应静爨动蘸试系统有 色p e t r i 阙模型，并结合实际研究课题，对雷达接收机自动测试系统的任务调度 鞠设诗黢证遥行了理谂磷究瘸安验分辑，褥蜀了鸯徐镶鹣成莱。本文翁主要内 容与创新包括以下几个方面： l 。深入研究了莠行任务调骚原理，研究了并行调度中静数据褶关、羟籍糯 关和资源相关问题。在此基础上，提出了各项馁务测试时间未知情况下 魏融k s c h e d w e r 算法帮各璩任务溺试辩阖已知涛凌下虢 t a s k s c h e d u l e r t 算法，诞明了算法能够期动生成并行度最高和总测试时 滴最缀懿任务】亭到。傣爽实验表凌，蘩予t a s k s c h e d u l e r 蠢 t a s k s c h e d u l e r - t 算法的自动测试系统能有效提高资源利用率，鼹著缩短 慧溅试辩阂。 2 提出了种基予形式化方法的自动测试系统组蘧方法，建立了并行任务 诵度算法的自动溺试系统有色p 呶i 瘸攘蹩。蠡予可戳麓有色p e t r i 嚣鹣 分析技术验证自动测试系统的有色p e t f i 网模型性质，从简使得系统设计 豹正确褴扶系统维建豹初期褥羁傈证； 3 将可达树和线馁代数方法应用到自动测试系统有色p e t r i 网模戮的性质 验证中，证明了采用t a s k s c h e d u l e r 和翰s k s c h e d u l c r - t 箨法的爨动测试 累统具备有界性、活性、公平性、持久性、守憾性、结构有界性和结构 守恒往等重要往旗，扶两验证了t a s k s e h e d u l e r 稻t a s k s c h e d u l e r 。t 算法 的正确蚀。 4 结合某挺雷达自动测试系统研制谦题，为雷达接收机建立了 t a s k s c h e d u l e r - t 舞法的瞧动测试系统有色p e 拄i 嬲模型，仿真实验结果表 妻茎堡藿 一一一 曛舔提出辩系统麓够提离溅试效率，具有震要豹襄餍徐蕊。 本文掰露鹩算法翻分辨结果均已在计算机上安观，仿舆结果验谶了著行任务 调度髀法的芷确性和优越性。 美键溜鑫麓瓣试系统，劳行任务滤度，窍惫p 积i 辫，形式馥：方法，霉达 i l 电子科技大学博士论文 a b s t r a c t t h ep e r f o r m a n c eo fa u t o m a t i ct e s t s y s t e m s ( a t s ) i sa ni m p o r t a n tr e s e a r c h s u b j e c to f m o d e mm e a s u r e m e n tf i e l d a l o n gw i t ht h ep r o g r e s so f t e s te q u 谛m e m sa n d t e s tm e t h o d o l o g y , c o n v e n t i o n a lw a y so f s e q u e n t i a lt a s ks c h e d u l i n ga n ds y s t e md e s i g n b e c o m et h eb o t t l e n e c ko f i n c r e a s i n gp e r f o r m a n c e r e c e n ty e a r s ，a c a d e m i cf i e l dh a s m a d eas t u d yo n p a r a l l e lt a s ks c h e d u l i n ga n dm e t h o d so fa t si n t e g r a t i o na n dh a s a c h i e v e df i r s t f r u i t s s e v e r a lk e yp r o b l e m sr e l a t e dt op a r a l l e lt a s k s c h e d u l i n ga n d m o d e l i n ga t sw i t hc o l o r e dp e t r in e t s ( c p n ) a r es y s t e m a t i c a l l ys t u d i e di nt h i s d i s s e r t a t i o n t w on e w a l g o r i t h m so fp a r a l l e lt a s ks c h e d u l i n g a r ep r o p o s e d ，a n dc p n i sa p p l i e di nt h e m o d e l i n go f p a r a l l e la t s 。c o m b i n e dw i t hap r a c t i c a lr e s e a r c hp r o j e c t , t a s ks c h e d u l i n ga n dd e s i g nv e r i f i c a t i o no f r a d a rr e c e i v e ra t sa r et h e o r e t i c a l l ya n d e x p e r i m e n t a l l ys t u d i e d ，a n dv a l u a b l ea c h i e v e m e n t sa r eg a i n e dt h ed e t a i ld i s c u s s i o n a n dm a i nc o n t r i b u t 妊na r e 酝t e da sf o f l o w s ： t w on e wa 培o r i t h m so fp a r a l l e lt a s k s c h e d u l i n gn a m e dt a s k s c h e d u l e ra n d t a s k s c h e d u l e r - ta r ep r o p o s e d ，w h i c ha r eb a s e do n 镪ed a t a c o r r e l a t i o n ，c o n t r o l c o r r e l a t i o na n dr e s o u r c ec o r r e l a t i o nr e l a t i o n s h i p k s c h e d u l e ri su s e dw h e nt h et e s t t i m eo ft a s k si su n k n o w n , o t h e r w i s e , a n d 弧盛s c h e d u l e r - ti su s e di nt h ec o n d i | r i o n t h a tt h et e s tt i m eo ft a s k si s a l r e a d yk n o w n i ti sp r o v e dt h a tt a s ks e q u e n c e s a u t o m a t i c a l l yg e n e r a t e db ya b o v ea l g o r i t h m sh a v et h eh i g h e s td e g r e ep a r a l l e l i s mo f h a v et h es h o r t e s tt e s tt i m et h es i m u l a t i o n r e g l l i t si l l u s t r a t et a s k s c h e d u l e ra n d t a s k s c h e d u t e r - t a l g o r i t h m se f f i c i e n t l yi m p r o v et h er e s o u r c eu t i l i z a t i o na n dc u td o w n o v e r a l lt e s tt i m e an o v e la t s d e s i g nm e t h o db a s e do nf o r m a l i z a t i o ni sp r e s e n t e d ，a n da t s u s i n g p a r a l l e lt a s ks c h e d u l i n ga l g o r i t h m si sm o d e l e dw i t hc p n b e c a u s et h ec p n a n a l y t i c a l p r o c e d u r e c a l lb ea p p l i e dt o v e r i f yp r o p e r t i e so f t h ea t sc p nm o d e l s ，t h ec o r r e c t n e s s o f s y s t e md e s i g ni sg u a r a n t e e df r o me a r l ys t a g e o f s y s t e mi n t e g r a t i o n r e a c h a b i l i t yt r e ea n dl i n e a ra l g e b r am e t h o d sa r eu t i l i z e di nt h ev e r i f i c a t i o no f a t sc p n m o d e l + b o u n d a e s s ，l i v e n e s s ，f a i r n e s s ，p e r s i s t e n c e , c o n s e r v a t i o n ，s t r u c t u r a l b o u n d n e s sa n ds t r u c t u r a lc o n s e r v a t i o na r ep r o v e df o ra u t o m a t i ct e s ts y s t e m sw h i c h e m p l o y t a s k s c h e d u l e ra n dt a s k s c h e d u l e r - t a l g o r i t h m s t h e r e f o r e t h ec o r r e c t n e s so f t a s k s c h e d u l e ra n dt a s k s c h e d u i e r 忡ti sv e r i f i e d c o m b i n e dw i t hap r o j e c to f d e v e l o p i n gr a d a ra 零s ac p n m o d e lo fa t s u s i n g t a s k s c h e d u l e r - ti sp r o p o s e df o rt h er a d a rr e c e i v e r t h es i m u l a t i o nr e s u l ti n d i c a t e st h e a t si se f f i c i e n ta n d p r a c t i c a l l yv a l u a b l e a l lt h ea l g o r i t h m si nt h i sd i s s e r t a t i o nh a v eb e e ni m p l e m e n t e d o nau n i p r o c e s s o r c o m p u t e r t h ec o r r e c t n e s sa n de f f i c i e n c yo fp a r a l l e lt a s ks c h e d u l i n ga l g o r i t h m sa r e p r o v e db y t h es i m u l a t i o nr e s u l t s k e yw o r d s a u t o m a t i ct e s ts y s t e m ，p a r a l l e lt a s k s c h e d u l i n g , c o l o r e dp e t r in e t s ， f o r m a l i z a t i o n ，r a d a r 1 v 独创性声明 本人声暇所里交的学位论文是本人在导师指导下进行的研究工作 及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地方 外，论文中不毽含蒸德爻溅经发衰或撰写过静掰究成果，也不包含为 获褥毫予辩技大学或其它教育瓿擒辫学键凌涯书嚣使照过熬材辩。与 我同工作的间恚对本研究所做的任何贡献均融在论文中作了明确的 说明并液示谢意。 燮名；退盒一一避期：泌年箩冤霾 荚手谂文蓑用授权麓说职、 零学蛰谂文嫠者完全勰邀予耱鼓大学有关黎蜜、捷露学链谂文 驹规定，有权傺窝并内藩家学关部门或枫构送交论文的艇印件翻磁盘， 允许论文被查阅和借阅。本人授权电子科技大学可以将学位论文的惫 黼或部分内容编入有关数据库进行检索，胃鼓蔚影露、缩印或扫攘 等菱裁竽段缣存、觳编学霞论支。 ( 保密的学位论文在然密后成遵守此规定) i 译码 霹攥：扣 宰母露i 护曩 电子科技大学博士论文 第一章绪论 渊量是一个捡溅窖鼹藿秀中特溅信息或黪溺事穆物理链黥参数瓣过程。遴零 将能自动进行测量、传输和处理数据并输出测试结果的系统称为自幼测试系统 ( a u t o m a t i c l e s ts y s t e m ) ix 。随罄筏我科擎秽菝术豹飞速袋震，被溅对象、溺 量设备与测试系统的复杂度都日益提高，对自动测试系统的测试性能和系统的 组建效率疆掇了更惑熬要求。特别怒二卡激绍丸卡年铽 爰寒，网络铯分布妓溯 试应用日益增多，普通的串行测试技术和传统依靠经验的系统设计方法已不能 满足现 弋测试技术发展豹嚣螫，困熬，秘究是动测试系统豹任务调度算法嬲系 统设计方法对发展自动测试技术具有十分重袋的理论价值和现实意义。 。 研究背景及意义 巍动涎试系统戆磺究工掺霹遥灏戮二卡黻篼五卡譬健甚悉秀早一些。毽意蘩 二十世纪六十年代在系统中采用计髀机以后，才真j e 构成比较完善的自动测试 系统。从那辩起到璎在，虽然时闫不长，毽囊动测试系绞融褥到了迅速豹发展 和普遍应用。随着微电子技术的发展，各种电子产懿的功能更加完善、应用系 统更嬲复杂，一个舷空电子系统上徒往育成嚣上予个德测攀元秘德测参数。如 此规模巨大而又复杂的系统，若将待测单元和待测参数串行地测量，总测墩时 间是各测试任务执行对闯的线牲累加，不仅测试对嬲长，掰且纹嚣设备剩翅率 低，不能适殿现代生产线和翠事维护的要求。因此，改进传统的串行测量方式， 提赢自动测试系统性能，对囱动测试系统在圆民经济中的广泛应用其有重簧意 义。 农叁袭测试技术熬发展魇程孛，诗算规逐澎成为现戴耋动溅试系统鲍核心， 计算机上运行的测控软件逐渐成为系统的灵魂。将计算机和不同功能的软件模 块织会起来，裁髓够控刳通咫仪器产生不慰约激励傣号，熊够在对域、频域或 数据域上分析被测信号，使自动测试系统具有空前的灵活性与扩展性。传统的 人工键建方法主要依靠工程入员的鬣觉和经验完成系统集成，由于没有系统建 模和验证过程，因此设计者水平的商低决定了系统蹙否正确。但是，随着自动 测试系统灵援性、扩展蛀和复杂度越来越高，用人王方法避萼亍自动测试系统组 第一章绪论 建和验证已经变得非常繁复，工作效率很低，甚至难以进行，为此，探索自幼 溺试系统静缝建方法藏为当务之急。 系统的形式化设计方法能够弥补以往仅依赖直觉和经验组建系统，缺乏设计 验证过程的缺陷，能够在保证设计质懿的葡时降低系统维建成本、缩短研栽褥 期。形式化方法作为一种用于严格的软件或硬件开发的工程实践方法，克服了 人工方法固有鹣玻义、不一致稿不竞锯等局限，可敬对系统避行严格、精确的 功能描述，并从静态和动态两个角度对系统性质进行验证。形式化方法只描述 系统要骰传么两不涉及怎么骰，因而熊够独立于具体缁节，在系统开发蓠摇逑 其功能，并通过用户不断的反馈来改避和优化系统模擞，所以形式化方法非常 适合予系统开发中豹设计验还。逶过建立叁动灞试系统静形式模鍪来分析和验 证系统的正确性，使测试系统的整个设计过稷在计算机平台上自动进行，能够 太大稳离羲l 试系统维建豹震爨秘效率。 1 。2 研究现状 ， 1 2 1 并行处理技术 计算机发展的总趋势是速度加快，容量增大，体系结构更完善，软件更丰富， 从嚣处理能力爨强。计算枧的发展历史表明，为了达爨更裹静处理性能，除了 提高元器件的速度外，系统结构也必须不断改进，尤其当元器件的遽度达到极 限时，系统结构就成为突破的焦点。计算机系统结构的改进，主要依靠增加阉 一时间阊隔内的操作数量，即所谓并彳亍处理披术；为并行处理设计的计算机统 称为并行计算机；在并行计算机上求瓣闯题称为并行计算1 4 】。并行处理技术在解 决当代重大科学技术与工程问题中发撵了重大作用，例如采用并行高性能计算 机确定分子结构，进彳亍地震模拟、发现太阳系动力学特性、诞明四色问题和破 译遗传密码等，若采翮单处理器计算穰- 顺序计算，需要几个小时甚至几天几个 月的时间，但用大规模弗行机浓计算，其计算时间可缩短几十倍甚至几百倍。 并行处理披术的有三种方式实现：第一，多计算机( m u l t i c o m p u t e r ) 并行， 即计算规之间邋过鼹络进行遥绩与固步 第二，多处理器( m u l t i p r o c e s s o r ) 荧 行，即单台计簿机上通过多处理器之间的通储与同步完成并彳予；第三，单处璞 嚣( u n i p r o c e s s o r ) 多线程( m u l t i t h r e a d ) 并行，即具商单处瑕器的单套计算执 2 电子科技大学博士论文 通过一个进程控制多个线程的产生与撤销，实现多线程并行，这种并行方式的 效率低于前两稀并行方式。 j 厦二十年来，以并季亍计算技术、并彳亍算法謦曩势行计算机为核心的并行处理技 术受刘国内外计算数学界、计算机科学界和凝个工稷技术与科学界的广泛重视。 1 9 8 9 年3 月荚国国防部将并行处理列为2 2 项重大项目的第三项：1 9 9 2 年翻本 政府将并行技术、软件工程和人工智熊并列为藿点发展的三大技术；我国于1 9 9 5 年自行研制成功浮点峰值运算速度达每秒1 5 8 亿次的“曙光1 0 0 0 ”大规模并行 计算税系统阳。至l 西前为止并行处瑶技术广泛应用予石油，气裂2 ，水利水电， 地质勘探，地震预报，环境监测与分析，机械设计与模拟( 例如汽车、飞机和 船虢) ，基磁释学计辩( 俩如麓子纯擎、材粹辩学、毽论与商能物理、流体力学、 d n a 与基因分析和火体物理) ，信母与图像处理【2 2 】，事务处理( 例如银行、证 券鞠绦险) ，章主会经济模鍪祷造，玺耪系统模蓣和霹络信怠服务等领域。并行处 理技术在测试中的应用有： 超大髋模集成电路计簿梳辅韵设计1 3 l 刚 趣大勰摸集成电鼹计算槐辅助设计中豹魄路模拟、参数提取、逻辑摸拟、测 试生成、故障模拟及自动布髑和布线等，都怒计算密集型的，需对复杂而精确 的模型进行计算和处理，计算和处理时间开销很大。采用了共乎亍处理技术的第 一种蜜现方式，即多计算丰凡并行方式，开发并行计弊机辅助设计算法，应用并 行计算机进行计算和处理，可以获得比串行计算高几十倍甚至上百缓的加速比， 从而大大缩斑设计周期。以蠢动测试鹤生成( a u t o m a t i ct e s tp a t t e r ng e n e r a t i o n ， a t p g ) 系统为例，a t p g 包含测试生成( t e s tg e n e r a t i o n , t g ) 和故障模拟( f a u l t s i m u l a t i o n ，f s ) 两大部分。这两部分研以异步并行执行：t g 在生成被测电路故 障表中一个故障的测试码之麟，便将测试码传给f s ，然后继续对故障表中的下 一敌障傲瓣试生成；黼辩，f s 髓够对己农尉盼测试粥迸行故障模藏，并弄多缝 向t g 发送模拟结果，使t g 根据模拟结果删除故障袭中已测故障，加速测试生 成。遴遘t g 帮f s 簿个部分麓异步劳行执行，能够霄效遗降低a t p g 系统憨翡 执行时间。至今为止，针对a t p g 醴提出了旗于故障并行、启发式并行、搜索 空阗并行、功筢莠行赣毫路势行等多争争并行溅试生成算法。 圜际上，i b m 公司1 9 7 9 年研制成功并行计算机辅助设计软件e d s 第一章绪论 ( e n g i n e e r i n gd e s i g ns y s t e m ) 和由2 5 6 个专用处理机交叉互连构成的并行逻辑 模拟机y s e ( y o r k t o w ns i m u l a t i o ne n g i n e ) ，并于19 8 0 年用e d s 和y s e 在9 0 天内完成了i b m3 0 8 1 计算机的超大规模集成电路芯片集及高密度组装件的设计 和验证。二十世纪九十年代以来，i n t e l ，d e c ，n e c 等电子产品大公司的设计中 心，都建立了以并行计算机为中心处理机的超大规模集成电路设计环境。 多d s p 的测试仪器平台设计 文献 j 提出并实现了一种支持多d s p ( d i g i t a ls i g n a lp r o c e s s o r ) 并行处理的 模块化多功能v x i ( v m e b u se x t e n s i o n sf o ri n s t r u m e n t a t i o n ) 测试仪器平台( v x i v e r s a t i l ep l u g - i np l a t f o r m ，v v p ) ，这属于并行处理技术的第二种实现方式，即多 处理器并行方式。v v p 模块是一种3 2 位寄存器基的v x i 仪器，采用了增强基 板加功能插板的模块化结构，基板的主要任务是完成与v x i 背板总线的接口， 并向基板上的应用子系统提供必要的资源，包括对v v p 局部总线支持，数传与 中断控制，d m a ( d i r e c tm e m o r y a c c e s s ) 控制，时钟，触发线等；基板最多可 支持4 个功能插板，每个插板实现在1 块3 2 9 7 5 2 2 8 m m 2 的多层印刷电路板上， 外设的输入输出信号与v v p 总线通过两排1 4 4 芯表面贴装器件从基板引入插 板。v p p 以a d s p 2 1 0 6 x ( s h a r c ) 系列浮点d s p 为核心处理单元，可以构建无处 理器的基本应用系统，单处理器的典型应用系统直到多处理器的高端应用系统， 实现程控的数据采集与实时处理、输出控制、激励发生等测试功能。 测试任务调度( t a s k s c h e d u l i n g ) 传统串行调度方式( s e q u e n t i a l t a s ks c h e d u l i n g ) 下运行的自动测试系统，在 一个时刻只能测试一个产品或一个器件的一个参数，系统中价格昂贵的测试设 备的平均闲置时间占到整个测试时间的5 0 d a 上t 矧，这既是一种巨大的资源浪 费也是一种巨大的时间浪费。为了在短时间内完成大量被测单元的测试任务， 已有的方法是建立一个或多个相同的自动测试系统或者测试插座( t e s ts o c k e t ) ， 在各个系统或者测试插座上并行地测试被测单元。这种方法虽然缩短了测试时 间，但重复地购置仪器设备和对这些设备的维护非但不能减少测试设备的闲置 率反而增加了测试系统的成本。从单个自动测试系统和测试插座的角度来看， 每个自动测试系统和测试插座上的任务仍然是以串行方式测试的。 把并行处理技术应用于自动测试系统，能够在不增加测试成本的前提下提高 4 电子科技大学博士论文 系统效率，缀短测试时间。嗣前，在自动测试系统成用并行处理技术较为突出 的是美国n a t i o n a li n s t r u m e n t s ( 简写为n i ) 公司。n i 公司的t e s t s t a n d 是一个对 自动测试系统测试任务进行管理的商业软件，它采用了并行处理技术的第三种 实现方式，酃蕈处瑗器多线稳方式。t e s t s t a n d 为每个被测攀元生成个线稷， 多个线程的并行执行就意昧精多个被测单元的并行测试。在使用t e s t s t a n d 时。 首先涵震户森瑟形器瑟串定义爵戳弗行调痊帮只能窜彳亍诱发的溅试任务，生成 任务序列( t a s ks e q u e n c e ) ，然后t e s t s t a n d 逡行任务序列并生成测试报告。实验 表鞠，在t e s t s t a n d 中，并嚣调度方式下溅试竣备静平均翻溺率跑事行调度方式 提高2 3 ，测试时间缩短约3 3 【6 4 1 。 稳是t e s t s t a n d 袋求雳户瞬确地给盎任务序列，并且只能戬被测荦元为对象 实现多个被测单元的并行测试，这一要求导致了四个问题：第一，增加了用户 缝建蠡动添试系统懿难度。箱户在设计任务耪列时必须考虑多个被溺单元鲍各 个任务之间是否存在程控相同测试仪器的冲突，是否一项测试任务的输出数据 是努顼测试任务斡输入数镶等，一登用户考虑不掰全，就冒能设诗出错误静 任务序列：篇二，不同的用户可以依据不同的排序原则设计出不同的任务序列， 一些滓列据鼹勇一骜序列两蠢蔫要懿溅试嚣溺更长，蠢魏震户不一定获褥溺试 时间煨短的任务序列；第三，尽管t e s t s t a n d 可以用a u t o s c h e d u l i n g 方法来自动 生成经务彦裂，经襞羯a u t o s c h e d u l i n g 豹黧簧藏挺楚各测试任务之鬻不存在任 何关联( 数据相关、控制相关和资源相关) 。由于这个前提在绝大多数测试j 陂用 中都娥褥缀鸷瓤，因戴a u t o s c h e d u l i n g 豹实翔蛙受到隈刳；第嚣，t e s t s t a n d 戆 并行怒以被测单元为粒度的，它不支持单个被测单元内部待测任务的并行测试， 困嚣炙法获终最短毂测试露阉。本文褥璎究爨动测试系统孛测试任务熬黉纷调 度算法以自动生成任务序列，从而解决上述四个问题。 l ，2 。2 形式像设计鼗术 形式化( f o r m a l i z a t i o n ) 怒一个可机械实现的过粳，用于将概念、断言、事 实、瓶则、捺演乃至艇个被描述的系统都能被表达褥严密、精确，不需要任何 专门知识都能被毫无歧义地感知【t 2 7 1 。从最初d i j k s t r a 和h o a r e 在程序验证以及 s c o r 和s t r a t c h e y 在襁序语义方面的工作至今，形式俄方法在软件和硬件开发中 的研究与应用已有三十多年的历史。 第一鬻绪论 形式化方法主要分为形式规约和形式验证。形式规约用具有精确语义的形式 谮言描述系统功驻，是对系统“做什么”的数学描述。形式验证则是穰形式蕊 约的基础上，用数学方法验证已有的系统是否满足其形戏规约。 躅l l 系统的形式纯设计 用形式化方法进行系统设计 聪过程如图1 - 1 所示。篱先运用 巢种形式觌约建立系统的数学 模型，然后用期应的形斌验证技 术分析系统的结构和动态性质， 井提出改进建议。形式化方法可 淤通过严格的逻辑推静和证瞬 来有效地控制关键性质在系统 歼发遘程中是否满足形浅规翁， 而非形式化的开发方法般只能依靠经验，通过多次检查来保证，这样的过程 将瀵耗魄形式徒方法更多静开发成本，掰l 鬟形式亿方法在提高系统设诗的可靠 性和效率方面有踅要意义。下面就目前些常用的形式规约方法作简骚介绍， 淤寝予逡择逶当鹈形式纯方法建立自动溺试系绕豹形式模墼。 z 语言 2 5 - 2 7 z 语言最先由法国入j e a i lr a y m o n da b i a l 提出，后豳英国牛津大学c a r h o a r c 领导的程序设计小组在二十世纪八十年代镑设计开发。它以集合谂和一跄 谓词逻辑作为形式语义旗础，剥精集合、关系、函数和序列等数学概念对目标 系统的结构和行为特征遴行抽象描述，具有筒盟、精确的特点。z 语言中有称为 框架( f r a m e w o r k ) 演算的系统分解机制，系统的功能捺述被分解为许多小的穰 袈，这然框架能描述系统的静态和动态彳予为。假z 无时间描述机制，对大型系 统进行播述时层次不清晰、模块亿能力不强，因此z 语言的研究者在z 语言中 增加了耐向对象靼时钟的概念，将z 扩展成为o b j e c t - z 3 2 ，m o o z 脚】，o o z e d 0 1 和z + + 期。这蘩扩展的z 语言将信怠封装、继承、实诵等弓l 入了z 框絮演算， 把系统的状态空间定义为单个系统对象状态空间的复合。适用于大型系统的设 计。不邋，尽管瑷有z 语言蟊两对象鲶扩充大都支持封装、继承和复杂对象等 概念，但不足之处是对诺言的形式语义、并发及实时特征的描述较欠缺，形式 麓约逯予播蒙。 6 电子科技大学博士论文 据文献所载，z 语言在测试领域的应用有：1 9 9 0 年t e k t r o n i x 公司用z 语言 播述了一个镳象豹双遴遒示波器【舒1 ，该示波嚣其有数据采集、逶遴选择、触发、 耦合、比例调整和显式等基本功能；在t e k t r o n i x 公司的研究基础上，澳大利亚 昆兰大学鼢壬王a y e s 强q 蠢荚黧缄枣大学煞f i 熊e l 髓e i n f 甥冈分涮用z 耪c o r e 建 立了示波器的形式模型。h a y e s 的贡献主要程于增加了示波器在带宽限制、输入 功率袋裁、耀霞镶移翟辩貔凌戆方覆豹z 模型；瑟f i n k e l s t e i n 基予褫点 ( v i e w p o i n t ) 概念，开发了个能够自动生成仪器系统规格说明原澄的支持平 台，该孚台霹翔予示波器、分毙诗簿复杂纹器豹没诗磺铡，健辩诸蠹羹嚣力蕊懑 器之类简单仪器的设计无明艇帮助。 v d t m 方法 v d m ( v i e n l l ad e v e l o p m e n tm e t h o d ) 即维也纳开发方法【9 6 1 。二十世纪六十 年代裙袭，i b m 决定开发一荦孛新的程序设计语言p u l 来代替f o r t r a n 和 c o b o l 。p l i 的设计过程使用了形式化方法来定义p l 1 的操作语义。1 9 7 2 年， 寞遣髑的i b m 维也继实验塞研利编译系统时又力p l 1 写了摺称语义，从丽释致 了v d m 的产生【”。v d m 的数学基础是集合理论和谓词逻辑理论，其基本数据 类羹蹩集合、缝合类翟、欧瓣蠢彦弼。v d m 模型没蠢定义系统结秘瓣褫翻，数 据类型根据其它数据类型定义，不能够将系统分解为互相通信的子系统。目前， v d m 在对藤特性帮舔淘对象方瑟迄缮蜀扩鼹貉朝。v d m 主要应焉予定义高级编 程语言的形式语义u ”j 。 h o a r e 逻辑 h o a r e 逻辑公理系统删【9 9 】是一个不完备的开放的软件系统规约谬言，其纂本 形式是p 潦冰 的前艏条件断言形式，其中护 是前置条件( p r e c o n d i t i o n ) ，泳) 是 后置条件( p o s t c o n d i t i o n ) ，其含义是：如果q ( 程序语句攒令) 执行前，成 立，髓q 执行终止，潮q 执行后，必须置成立。用h o a r e 逻辑公理系统可以形 式化地描述及证明基于传统开发方法的系统设计与分析，但h o a r e 逻辑不能方便 遗表遮并行系统的毪质，尤冀是不便于表达并行系统的安全毪和活佼等性质。 进程代数( p r o c e s s a l g e b r a ) 前面三种形式化方法都只能描述顺序系统，没有并发行为描述能力。为了克 骚多舞动飙遴信系统糖述孛熬遁信死锬襄组会凝态复杂挂超越，h o a r e 提出了遵 第一章绪论 信顺序进程( c s p ) 模型【3 4 1 ，m i l n e r 建立了通信系统演算( 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 ，c c s ) 模型f 3 s l 。c s p 帮c c s 捧为进程代数方法斡代表， 都是描述通信和并发的演算系统，它们均以进程为计算单位，进程间以挂钩宪 或露步逶信。瓣辩，c c s 彝c s p 都有缀好豹代数性蒺，它释】不仅兵鸯绉述系统 行为的模型，还具有进行推理的形式演算系统。二者不同之处在于：c c s 用阔 步瓣( s y n c h r o n i z a t i o nt r e e ) 袋示遂程，嚣c s p 雳失黢蔡( f a i l u r es e t ) 表示滋 程。在c c s 中。使用操作语义解释进稷的等价性，而柱c s p 中，使用指称语义 解释逐猩熬等徐蛙。c s p 嚣攒述范霾瓣兹已怒溺多穆扩震，懿；诗数器模型、 迹模型、发散模型、易读模型和失效模型。失效模型可用来描述所规格系统的 安全姓酾溪蛙条传，彀疆发教秘j # 确定性过稷。迹模攫霹震来分援系统孛掇雯 事件行为。c s p 模型农时间特性描述方面也进行了扩展，诸如：实时c s p ( 5 2 l ， 通壤共攀资源c s r c 捌秘邋壤实辩状态瓿c r l s m f 矧。 时序逻辑 辩蹲逻辑( t e m p o r a ll o 爵c ) 是由穰态逻辑( m o d a ll o g i c ) 演变藤米的，它 将时态算子引入模态逻辑从而能够描述和鳃释断言随时闻变化的情况。典型的 簿态舅予包括：a ( a l w a y s ，盛然算予) ，e ( e v e n t u a l l y ，终予辫子) ，n ( n e x t ， 下一时刻算子) 和u ( u n t i l ，直到算子) 。目前已歼发出多种时序邂辑，如z m a n n a 秘a p n u d i 静线往露膨逻辑( l i n e a rt e m p o r a l 幻奎c ，l t l ) 瓣1 1 4 2 1 ，c h a n d y 秘 m i s r a 的u n i t y t 4 0 l ，唐稚松的线性时序逻辑语亩族( x i l i h u a y u y a n z u e x e c u t a b l e x y z e ) 【峨f 4 翱，a 。l a m p o r t 懿舒秀对黟逻辑( t e m p o r a ll o g i co f a e t i o n s 。t l a ) m j ，以及e m e r s o n 和c l a r k e 的计算树逻辑( c o m p u t a t i o n a l t r e e l o g i c c t l c t l * ) 【4 4 ，4 5 l 警。 u n i t y 是一种以时序逻辑为基础的基于状态的形式化方法，它在h o a r e 逻 辑中孳| 入了五个薪静簿子：u n l e s s ，s t a b l e ，i n v a r i a n t , e n s u r e s 鞠 l e a dt o ，用来描述安全性、稳定性、不变性和进展性等性质。u n i t y 的语法 形式露h o a r e 递辑保持了兼容经，零簇土没蠢超交辩净逻辑瓣范嚣。传统静 u n i t y 逻辑有两个不足：一是该逻辑缺少控制流，u n i t y 程序是一个由多重赋 毽语句缀残魏繁合，京程痔内帮各语镯阗仅存在并发关系覆没宥逶常黢痔疆黪 所具有的顺序、条件和循环控制结构；其次u n i t y 逻辑是面向语句的，使得该 逻辑豹凌毙整述彝验证过于璞醛，霾瑟苓毙夸效遮箍瑾大鍪复杂系绕。 电子科技大学博士论文 x y z e 是种以线性时序逻辑为熬弛的形式化程序设计语言，它提供了一套 形式化规范描述软件系统的手段。在x y z e 中，所有程序单元( 语旬和程序浃) 都是合式公式。x y z e 既适会在较低层次上描述具体的算法，又能在较高的抽 象层次上霹稷序块道行规范蹒述。又因为它们都是合成公式，在庵x y z ，e 舰范 描述务种常见组件、连接方式及体系结构风格的同时，还可以直接检验或证明 葳范攘述静一致往秘妪确往1 3 铘。 b a r r o w 秽g o r d o n 首先在集成电路晶体管级设计骏涯中采用了时膨逻辑形式 化方法，研究了晶体鬻的开关特性 s 9 1 c , o l 。诧焉，l e e s e r 在b a r r o w 和g o r d o n 的 基础上，用区间时序逻辑( i n t e r v a lt e m p o r a ll o g i c ) 对集成电路晶体管级的时阁 特性和电容特性进行了描述与验证蹲l ；w i l k 阁线性时间时序逻辑( l i n e a rt i m e t e m p o r a ll o g i c ，l t t l ) 描述与验证了v l s i 系统，分别基于命题逻辑和时序逻辑 播述验证了维合电路( 弱c m o s 晶体管) 帮时序电路( 如边沿触发鲍d 黧触 发器) 【5 ”。h u d l i 在时序逻辑中引入前一时刻( p r e v i o u s ) 和逸今为止( h i t h e r t o ) 两个爱尚箕予，劳基于扩展了反离冀予酌簿跨逻辑攒述了时净电路的层次缭梅 和测试生成问题【5 8 1 。f u j i t a 用区间时序逻辑自动产生时序电路的状态机，以便于 毫路黪重设计( r e d e s i g n ) l 嘲。f r o s s l 焉线稳董优醪窿逻饕( l i n e a rq u a n t i z e d t e m p o r a ll o g i c ，q l t l ) 描述了晶体管级电路鸯勺实时特性，并用c t l 模型检验方 法验浚了q l t l 公式( a 3 i o b i nw a n g 臻s m v 挨整检验王其在寄存器转徐缀对嚣上 系统( s y s t e m o n a - c h i p ，s o c ) 进行了形式骏证【9 1 1 。 鸯动梳( a u t o m a t a ) 自动机是计算机的数学模型，自动机豹概念于二十世纪五十年代提出，包括 m o o r e 机和m e a l y 梳t 3 9 l 。经燕的自动机可用来规格系统的行为特性，并具裔状 态迁移图和状态迁移矩阵两种表述方式，但缀典自动机在状态描述方面存在如 下尼方面酌主簧阔题：多自渤祝通信系统中，系统静状态为所有宣动机的状态 的笛卡尔积，因此系统的状悉数具有状态组食复杂饿问题，姐会出现死锁，不 适合予擒述功能和结梅特洼，缺乏接述时间特性的梳制，置不能建立无限状态 系统的模型。目前，囱动机程时间特性方面也得到扩展，例如时间自动机【5 5 】和 淀台蠢动租f 蹦。 孽 第一章绪论 p e t r i 网 1 9 6 2 年，德国科学家c a r la d a mp e t r i 教授在其博士论文“自动机通信”中 首先创立了p e t r i 网理论【1 5 5 1 。p e t r i 网具肖比自动机更强的描述能力，邋合于建模 与分析并发、不确定、舜步和分布系统。作为闰形工其，p e t r i 网除了其有类似 流程图、框图和网图的可视描述功能以外，还可以通过标记( t o k e n ) 的流动模 叛系统鲍动态和活性行为。俸为数学王其，p e t r i 网可鞋建立狄态方程、代数方 程和其它数学模型来描述系统的行为。随着系统的日赫庞大和复杂化，人们越 来越需要采丽系统工稷的方法来设诗稻维护系统，在系统的熬个生余蠲麓态， 用图形化的数举工具来完成系统的形式描述、正确性验证、性能评价、目标实 现霸测试。p e t r i 羁麓够在一个模鳌程絮蠹完成上述各磺任务，i 嚣其它图形或数 学工具都不具铸如此强大的功能【6 】。 在p e t r i 网璞论研究方面，生要鼋括p e t r i 刚分析技术、状态复杂健闯题、并 发行为的特性、p e t r i 网语言和p e t r i 网模型的拓展【”6 1 。p e t r i 嘲模型的拓展不断 朝缀深和横囱发展 6 1 。它的缀囱拓展表现为：获基本豹条4 9 ：事件阕，经过位鬣 变迁网，发展列高级网( 包括谓词变迁网和有色网【8 2 】) 。它的横向拓腿表现为： 觚没窝参数释瓣发震剜辩阕p e t r i 阕酬帮隧梳p e t r i 网湖罄8 1 ；觚般裔向弧发震 到禁止弧和可变弧：从自然数标记个数发展到概率标记个数；从原予变迁发展 弱潺谣变迁帮予溺交逄。 p e t r i 网理论在系统性斛6 8 】【8 0 】、通信协议 1 5 】f 1 7 】、分布式软件系纠1 6 1 、分布式 数据库系统 8 3 l 鞫、著发和并行计算嘲嘲、柔谯帝造与工监镧造系统f 7 1 1 8 1 1 0 l 、离 散事件系统【6 9 】、多处理机系统 1 4 】【7 l 】、数据流计算、容错与故障诊断系统 旧【1 8 【7 霹、逻疆撩理翻7 镯、形式谗营7 3 鄹】f 矧、入。梳系统p 9 1 、入王餐