（控制理论与控制工程专业论文）混合系统形式验证中的问题研究.pdf

混合系统形式验证中的问题研究 摘要 混合系统理论是控制工程理论与计算机科学验证交叉的学科领域。混合系统 理论主要涉及到有限自动机表示的离散状态与微分方程表示的连续动态相互作 用的建模、分析、控制和验证。为了了解混合系统的行为和验证混合系统是否在 某种条件下能安全运行，需要先进的理论知识和分析工具。混合系统的形式验证 是混合系统研究的一个重要领域，至今仍未出现比较成熟的方法体系，验证工具 大部分都停留在实验室研究阶段，难以广泛适用于工业目标。 在这种背景下，本文围绕混合系统的形式验证问题，以解决验证中连续动态 计算所存在的困难为研究重点，其中又以可达集的计算为主要内容。针对流管道 近似方法在非线性系统中存在的计算复杂性，给出了两种简化方法：变时间间隔 的流管道近似方法和逼近法。逼近法指用流管道近似逼近切换面或者用多丽体逼 近切换面寻找某一时刻，在此时刻开始计算流管道近似凸多面体与切换面的交 集。 在对流管道近似方法进行分析的基础上，提出一种新的计算切换面上可达集 的方法。用凸多面体包裹切换面上的实际可达集，利用优化算法求出包裹的最小 凸多面体，而实际可达集的求取是通过对初始区域上某点，计算其对应于切换面 上的点的数值解，将数值解嵌入优化算法中得到。这里给出的凸多面体是指在切 换面子空间上的闭区域。 论述了一种基于反例的状态划分方法，即仅针对与验证规范有关的状态进行 划分，在一定程度上避免由于再划分整个状态空间导致的状态爆炸问题。在对反 例状态的划分上，由于暂时无法精确划分状态使之与该状态的后续子状态相对 应，给出了多次“对半”剖分的划分方法。经过多次地划分，这种“对半”剖 分方法能够确定划分后的反例状态集合与后续子状态相对应。 在实验部分，结合验证工具c h e c k m a t e 对倒立摆模型进行了验证；利用线 性切换系统的验证过程给出了反例划分的实验结果；在非线性跳跃小球系统的验 证中，列出了文中提出的可达集计算与简化方法的实验结果，并与简化前的计算 方法得到的实验结果进行了对比分析，阐述了改进方法的可行性。 最后，对研究内容进行了总结，分析了工作成果的不足之处，并对今后的研 究方向作了展望。 关键词：混合系统；形式验证；流管道近似；凸多面体包裹 t h er e s e a r c ho i lf o r m a lv e r i f i c a t i o n o fh y b r i ds y s t e m s a b s t r a c t h y b r i ds y s t e mt h e o r yl i e sa tt h ei n t e r s e c t i o no ft h ef i e l d so fe n g i n e e r i n gc o n t r o l t h e o r ya n dc o m p u t e rs c i e n c ev e r i f i c a t i o n i ti 3d e f i n e da st h em o d e l i n g ，a n a l y s i s 。 c o n 缸- o la n dv e r i f i c a t i o no fs y s t e m st h a ti n v o l v et h ei n t e r a c t i o no fb o t hd i s c r e t es c a 姆 s y s t e m , r e p r e s e n t e db yf i n i t ea u t o m a t a , a n dc o n t i n u o u ss t a t ed y n a m i c s ，r e p r e s e n t e db y d i f f e r e n t i a le q u a t i o n s t ou n d e r s t a n dt h eb e h a v i o ro fh y b r i ds y s t e m sa n dt ov e r i f y w h e t h e rt h eh y b r i ds y s t e m so p e r a t es a f e l yi ns o m ec o n d i t i o n s , t h e o r e t i c a la d v a n c e s a n da n a l y s e st o o l sa r en e e d e d f o r m a lv e r i f i c a t i o ni sah o t p o ta sw e l la sd i f f i c u l t yi n h y b r i ds y s t e m ss t u d y 1 1 搪m a t u r ef r a m ea n ds y s t e ma r en o ty e tb u i l t ，a n dv e r i f i c a t i o n t o o l sa r cs t i l lo nr e s e a r c hs t a t ei nl a b s w i t c ha 坞d i f f i c u l tt oe x t e n s i v et h ea p p l i c a t i o n t oi n d u s t r i a lo b j e c t s i nt h i st h e s i s ，t h em a i nc o n t e n to ft h i sd i s s e r t a t i o nf o c u s e so nf o r m a lv e r i f i c a t i o n o fh y b r i ds y s t e m s mr e s e a r c hp i v o ti st os o l v et h ed i 伍c u l t i e so fd i s c r e t em o d e l a p p r o x i m a t i o no fc o n t i n u o u sd y n a m i c s w h e r er e a c hs e tc o m p u t a t i o ni sam a i nt a s k a i ma tc o m p u t i n gd i f f i c u l t yo ff l o wp i p ea p p r o x i m a t i o ni nn o n - l i n e a rs y s t e m s ，t h i s 恤e s i sp r e s e n t sav a r i a b l et i m ei n t e r v a lm e t h o do ff l o wp i p ea p p r o x i m a t i o n ；a n d a c c o r d i n gt op r o p e r t yo ff l o wp i p ea p p r o x i m a t i o n , t h ea p p r o a c h i n gm e t h o do ff l o w p i p ea n do fp o l y h e & o na r eg i v e nw i t c hc a l lb ed e f m e da sc o m p u t i n gf l o wp i p e a p p r o x i m a t i o nn e a rt h es w i t c hs u r f a c e ad e wm e t h o do fc o m p u t i n gr e a c h a b l es e to ns w i t c hf a c ei sp r e s c n t e db a s e do n a n a l y s i s i n gt h ep r i n c i p l ea b o u tt h em e t h o do ff l o wp i p ea p p r o x i m a t i o n 1 1 】em e t h o d w o r k so u tt h el e a s tc o n v e xp o l y h e d r o nt h a te n w r a p st h er e a lr e a c h a b l es e to ns w i t c h f a c e a n dt h er e a lr e a c h a b l es e ti so b t a i n e db yb e l o wa p p r o a c h f a s to fa 1 1 w o r k i n g o u tt h en u m e r i c a lv a l u e0 i is w i t c hf a c ef o rad o ti ni n i t i _ a la r e a , t h e ni n b e dt h e n u m e r i c a lv a l u ei no p t i m i z i n gp r o g r a mt oo b t a i nt h er e a lr e a c h a b l es e t ， a p a r t i t i o nm e t h o db a s e do nc o u n t e r e x a m p l ei sd i s c u s s e d ，w i t c hp a r t i t i o nt h es t a t e i nr e s p e c to fv e r i f c a t i o nc r i t e r i o n ，s ot h ep r o b l e mo fs t a t ee x p l o d i n gc a u s e db y p a r t i t i o n i n g s t a t e s p a c eo n c em o r ei s a v o i d e di naw a y w h e np a r t i t i o n i n g e o u n t e r c x a m p l es t a t e ，t h e r ei sn oe f f e c t i v em e t h o dp a r t i t i o n i n gt h ec o u n t e r e x a m p l e s t a t ei n t ol i r e rs t a t ec o r r e s p o n d i n gt ot h el a t t e rs t a t eo fc o u n t e r e x a m p l cs t a t e ，d u et o t h ea b o v er e a s o n , ap a r t i t i o nm e t h o do f h a l f c u t t i n gi sp r e s e n t e d 砌sm e _ t h o dc a nf i n d o u tt h er e l a t i o nb e t w e e nt h el a t t e rs t a t eo fe o u n t e r e x a m p l es t a t ea n dt h el i t t e rs t a t e a f t e rp a r t i t i o n e dt h ee o u n t e r e x a m p l e i ne x p e r i m e n tp a r to ft h e s i s w ev e r i f yt h em o d e lo fi n v e r tp e n d u l u mw i t h v e r i f i c a t i o nt o o lo fc h e c k m a t e a n dw ep r e s e n ta ne x p e r i m e n tr e s u l tt h o u g h t e o u n t e r e x a m p l ep a r t i t i o n f o rt h em o r e w eg a i as o m ee x p e r i m e n tr e s u l t sa b o u t c o m p u t i n gr e a c h a b l e s e tt h o u g h ts o m em e t h o dp r o v i d e di nt h i st h e s i sa n da n a l y s i st h e r e s l l l ti nc o n t r a s tt oo r i g i n a lm e t h o d t h o u g h tw i t c hw ee x p a t i a t et h ef e a s i b i l i t ya b o u t t h o s em e t h o d s f i n a l l y ，s 1 1 n lu pt h ec o n t e n to f t h i st h e s i sa n da n a l y s i sd e f i c i e n c yi nr e s e a r c h a n d r e s e a r c hw o r ki nt h ef t l r t h e ts t u d yi sp r e s e n t e d k e y w o r d s ：h y b r i ds y s t e m s ；f o r m a lv e r i f i c a t i o n ；a p p r o x i m a t i o no ff l o wp i p e , c o n v e x p o l y h e d r o ne n w r a p p i n g 插图清单 图2 1 温度控制系统1 2 图2 2 台球游戏1 2 图2 3 灰色球运动轨迹1 2 图3 1 混合系统形式验证过程1 7 图3 2 仿真对方法2 0 图3 3 对原系统仿真方法2 0 图3 4 流管道近似2 1 图3 5 ( a ) 优化前凸多面体( b ) 优化后凸多面体2 2 图3 6v a nd e rp o l 方程的流管道近似2 2 图3 7 仿射系统流管道近似2 4 图3 8 多面体剖切2 5 图4 1 误差分析2 7 图4 2 ( a ) 固定时间间隔( b ) 变时间间隔2 8 图4 3 流管道逼近近似2 9 图4 4 切换面上的多面体包裹3 2 图4 5 切换面上多面体包裹应用与v a nd e rp o l 方程3 2 图5 1 1 图形界面3 6 图5 1 2 验证过程3 6 图5 2 1 倒立摆模型和切换律3 7 图5 2 2 倒立摆建模3 9 图5 2 3 线性切换系统4 0 图5 2 4 初始划分p o 4 l 图5 2 5 改进划分p l 4 2 图5 2 6 改进划分p ，4 3 图5 2 7 改进划分e 4 4 图5 3 1 跳跃小球模型4 6 图5 3 2 初始划分4 7 图5 3 3 小球的仿真轨迹4 7 图5 3 4 流管道近似仿真结果4 7 图5 3 53 t 间隔流管道近似逼近仿真结果4 8 图5 。3 。6 变时阅间隔仿真结果4 8 图5 3 7 逼近近似与变时间间隔结合仿真结果4 8 图5 3 8 多面体逼近仿真结果4 9 图5 3 9 切换面上凸多面体近似三维图4 9 图5 3 1 0 切换面上凸多面体近似二维图5 9 表格清单 表5 1 参数选取3 8 表5 2 1 初始划分p o 的迁移关系4 1 表5 2 2 改进划分p i 的迁移关系4 2 表5 2 3 改进划分p 2 的迁移关系4 3 表5 2 4 改进划分r 的迁移关系4 4 表5 3 1 流管道近似数据统计5 0 表5 3 23 t 间隔数据统计5 0 表5 3 3 变时间间隔数据统计5 0 表5 3 4 逼近近似与变时间间隔结合数据统计5 0 表5 3 5 多面体逼近近似数据统计5 0 表5 3 6 切换面上多面体近似5 0 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究i 作及取得的研究成果。据 我所知，除了文中特别加以标志和致谢的地方外，论文中不包含其他人已经发表或撰写过的 研究成果，也不包含为获得金b 王些盔堂 或其他教育机构的学位或证书而使用过的材 料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢 意。 学位论文作者签字：芗必岁蕴签字日期：研6 月，7 日 学位论文版权使用授权书 本学位论文作者完全了解金胆王些太堂有关保留、使用学位论文的规定，有权保留 并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅或借阅。本人授权盒 a b 王些太堂可以将学位论文的全部或部分论文内容编入有关数据库进行检索，可以采用影 印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者躲歹红主盏 导师躲 诹 签字日期：沙7 占7 签字日期：沙p 7 6 、7 学位论文作者毕业后去向： 工作单位： 通讯地址： 电话： 邮编： 致谢 在论文完成之际，首先向我的导师方敏教授致以衷心的感谢1 在三年的学习 和生活中，方老师从各个方面对我进行了精心的指导，为我提供了一个良好的科 研环境，培养了我独立思考和开展科研的能力。方老师认真负责的工作态度、严 于律己、宽以待人的为人处世作风和诲人不倦的师者风范让我受益匪浅。她严谨 求实的治学态度和敏锐创新的科学思维对我影响至深。这也是我研究生阶段获得 的最宝贵的财富，对我将来的工作和生活一定会有帮助。 感谢实验室叶海军、张雅顺、汪洪波、李兵、吕江波等师兄，他们为我树立 了榜样，为我现在的研究做了良好的铺垫。感谢李辉、张荣成、张明和方凯等同 学，感谢他们在学习和生活上对我大力支持和热情帮助。感谢张俊、陈志超、秦 明辉、孙斌、李寅和陈琼几位师弟师妹。祝他们前程什锦、学业有成! 感谢我的父母及家人多年来一如既往对我的支持和鼓励! 感谢所有关心和爱护我的老师、同学和朋友们! 作者：张斌 2 0 0 7 年5 月 第一章绪论 1 1 混合系统简介 混合动态系统h d s ( h y b r i dd y n a m i cs y s t e m s ) 又称混合系统。它是由事件驱 动子系统和时间演化子系统交互作用而组成的一类复杂动态系统。“混合”意味 着连续与离散的组合，混合动态系统意味着系统动态行为由相互影响的连续动态 和离散动态来决定。在文献【l - 5 1 对混合系统的概念都给出了定义，混合系统比较 被接受的定义为：包含离散事件动态系统d e d s ( d i s c r e t ee v e n td y n a m i c s y s t e m s ) 和连续变量动态系统c v d s ( c o n t i n u o u sv a r i a b l ed y n a m i cs y s t e m s ) ， 两者又相互作用的系统称为混合动态系统。 混合系统的研究对象相当广泛。例如，在制造工业中，按照加工流程，零部 件会被传输到一台指定的加工机器，机器完成这一部件加工的过程是一个时间驱 动的动态过程，但是只有在部件到达时，机器才开始加工操作，这又属于事件驱 动，所以整个制造过程既包含时间驱动动态又包含事件驱动动态，因此在制造过 程进行整体优化考虑时，就需要采用混合系统来更完整细致地刻画整个制造系统 的动态行为。离散的规划算法与连续过程交互时也用到混合系统，这为自主的智 能系统提供了分析综合的基本框架与方法。事实上，对于设计具有高度自主能力 的智能控制系统，混合系统研究的重点是为连续系统设计监督控制器。另外，混 合系统在描述复杂系统的分层结构时也很有用，例如化工过程控制系统、空中交 通管理系统及计算机通讯网络等。某些情况下，被控对象本身就是一种混合系统， 或是采用了混合式的控制器，从而使整个系统等价为混合系统。有时为了使问题 简化，将一些系统视为混合系统，例如为了避免直接处理复杂的非线性方程，往 往将其替换为一组简单的方程( 例如线性方程) ，然后在这些简单的方程间进行切 换，这是物理建模时常用的方法，典型的例子是切换系统。切换系统应用较为广 泛，例如变结构系统v s s ( v a r i a b l es t r u c t u r es y s t e m ) 就属于切换系统，变 结构滑模控制仍是控制界研究的一大问题，还有工程上广泛应用的分区p i d ，以 及模糊控制，都可以归入切换系统。 混合系统近十年来受到控制和计算机理论界的广泛关注，是因为无论从应用 角度还是理论研究上都具有重要价值。首先，混合系统广泛存在于生产实际中， 如变结构控制系统、模式切换系统、计算机控制系统、化工批处理过程、机器人 系统、智能高速公路系统( i n t e l l i g e n tv e h i c l e h i g h w a ys y s t e m s ) 、现代飞 行控制系统( m o d e r nf l i g h tc o n t r o ls y s t e m s ) 及一切同时涉及逻辑决策和连 续控制的系统。在理论研究方面，对连续时间动态系统通常采用微分和差分方程 进行建模和分析，旨在捕获系统的“物理”行为；而对离散事件动态系统，通常 采用有限自动机表示，旨在捕获系统的逻辑或顺序行为。由于对两类动态特性的 描述建立在截然不同的数学基础之上，欲对包含相互作用、相互影响的这样两类 动态特性的混合系统建立理想的模型，进行期望性能的分析，以及实施恰当的控 制，在理论上尚面临极大的挑战。基于以上原因，国际学术界对混合动态系统的 研究日益重视。 混合系统的特点可以概括为： 1 ) 系统内存在着性质不同的连续和离散两类变量； 2 ) 时间和事件共同驱动系统的状态演化； 3 ) 连续变量穿越阈值使状态使能或失能； 4 ) 离散状态的变化改变连续变量遵循的变化速率； 5 ) 离散事件发生在离散时刻，具有顺序、选择、并发等特色； 6 ) 状态呈阶段性、间歇性跳跃变化，动态特征显著； 7 ) 对系统的控制表现为对连续状态和离散状态的集成控制； 8 ) 对系统的优化表现为在定性定量双重指标下的集成优化。 总之，现有的大部分控制系统都可以被看作是混合系统，混合系统理论已在 机器人、汽车发动机、液罐液面控制、硬盘驱动、嵌入式系统、网络控制系统、 工业制造、化学过程、航空交通控制等场所得到应用，并越来越得到重视，成为 计算机科学、自动控制、应用数学等领域共同研究的热点睁”l 。 1 2 混合系统理论的发展概况 第一篇研究混合系统的文献出现于1 9 6 6 年( w i t s e n h a u s e n ) f l i 】。1 9 7 9 年瑞 典人c e l l i e r 第一个引入混合系统结构的概念，把系统分为离散、连续和接口三 个部分 1 1 。但是直到8 0 年代末“混合系统”才引起学者们的广泛注意。1 9 8 9 年g o l l i 针对计算机磁盘驱动器模型引入混合系统的概念，把连续部分和接口结 合起来进行研究n 2 1 。自第2 8 届c d c 会议以来，几乎每年世界上都有关于混合系 统的国际会议召开，如1 9 9 1 年在法国召开的关于h d s 的国际会议，1 9 9 2 年在丹 麦召开的计算机科学问题中的混合系统理论专题研讨会，1 9 9 4 年c o r n e l l u n i v e r s i t y 的w o h y a c ，1 9 9 5 年的d i m a c s ，1 9 9 6 年的h s 9 6 ( c o r n e l lu n i v ) 。 s o c i e t y 于1 9 9 6 年2 月成立了以m d l e m o n 为主席的混合动态系统研讨小组 ( w o r k i n gg r o u po fh y b r i dd y n a m i cs y s t e m s ) 。德国s p r i n g e r - v e r l a g 出版 社在其著名的计算机科学领域系列出版物l e c t u r en o t e si n c o m p u t e r s c i e n c e ( l n c s ) 中开辟h y b r i ds y s t e m s 专题，自1 9 9 3 年起至1 9 9 9 年已出版了五 本专辑，汇集了混合动态系统领域有代表性的研究成果；自1 9 9 8 年起，每年还 2 召开有关h y b r i ds y s t e m s ：c o m p u t a t i o na n dc o n t r o l ( h s c c ) 主题的国际讨论 会。从1 9 8 9 年起至今，每年召开的i e e e c d c 大会论文集都有多篇有关h d s 的研 究文献，如c d c 9 2 f 纠3 1 和c d c 9 3 1 1 9 - 2 1 。此外，世界上许多大学和研究机构都 成立了关于混合系统理论与应用研究小组，并形成了自己的研究特色，如以区段 演算( d u r a t i o nc a l c u l u s ) 及其扩展为工具的u n u i i s t 周巢尘小组；以a h s 系统研究致力于混合控制系统的应用研究的u b c 的p y a y a r i a 小组；c o r n e l l u n i v 的a n e r o d e 小组、m i t 的n l y n c h 以及以色列的p n u e l i 小组等则致力 于混合系统的理论探索。 总的说来，混合系统的研究尚处于开拓阶段，其理论基础和应用研究都是研 究的热点。近几年来，国外有关混合系统的文献不断增加，研究成果不断涌现； 国内也有一些学者专家开始着手这方面的研究，人们对混合系统的研究兴趣越来 越浓，其各方面的研究工作将会不断地深入下去。 1 3 混合系统形式验证的意义与现状 混合系统研究的内容主要是系统的描述和建模2 一、分析【、综合【邡，婀和 验证。混合系统的验证就是在已有模型的基础上，通过各种验证工具在实验 室对控制设计是否满足工艺条件进行仿真验证。混合系统的验证方法有两种【篮】： 模型检验( m o d e lc h e c k i n g ) 和演绎推理( d e d u c t i v em e t h o d ) 模型检验又称 形式化验证以计算机为主对整个状态空间进行搜索以确定混合系统是否满足预 定的规范，其优点是全部过程可以实现自动化，从而得到实用的计算机辅助工具， 但可决策问题是其需要迫切解决的问题。演绎推理又称定理证明，是以人为主在 规则集合的基础上用形式化的推理方法证明系统的性质，尽管演绎推理方法不受 可决策性的限制，但应用时需要人工多次干预，因此在大系统中应用遇到了很大 的困难。最近又出现了两者结合的方法f 剀：既先对混合图用演绎法将验证问题 变换为另一个验证问题，然后对这一新问题再利用算法进行验证。 形式化验证的过程为：构建系统的模型，并使用形式化的手段对系统某些 特性进行描述，然后通过一定的计算过程来判断系统是否满足该性质。由于混合 系统包括连续特性，在验证过程中，通常需要对系统的模型进行抽象，将问题转 化到离散空间上来，然后再使用离散系统的方法对其进行验证。在抽象过程中， 首先将连续变量的取值范围划分为若干个区域，然后在判断区域之间的可达性。 抽象不可避免的会造成信息的丢失，抽象过程必须保证不影响验证的正确性。从 严格的意义上来说，要保证抽象系统的可达性和原有系统保持一致，这样要求用 有限的方式精确地表示无限的状态空间，这在实践中通常是不可能做到的。通常 采用的方法是保守近似。 随着计算机应用的日益普及，今天我们已经很难承受计算机控制系统发生 3 故障所带来的损失。连续运行已成为现在许多计算机控制系统的关键需求，一旦 发生故障，终止系统运行进行维护是不现实的。以往的测试或仿真无法回答系统 一定没有错误这样一类问题。而形式验证可以从某一个角度回答系统一定没有错 误这类问题，从而进一步提高我们对系统可靠性的可信度 混合系统中离散事件和连续动态行为间相互作用的特性使得系统开发的复 杂性增加，开发结果的正确性也难以保证。尤其对于安全攸关的系统如航天系统、 电力系统和化工系统等，对系统安全性的要求很高，系统的错误运行将造成重大 损失。形式验证技术的目的在于检验混合系统是否在任何环境下都能安全运行。 因此，混合系统的形式验证问题的研究有着重要的科学价值和工程意义。 由于数字控制器的大量采用，控制程序的正确性和安全性往往难以保证。 目前对于复杂控制系统，需要依靠编程者的实际经验和大量的在线仿真来进行， 而且仍旧难以保证整个系统的安全性。所以研究混合系统的形式验证技术，期望 可以证明系统的所有可达状态是否满足预定的安全规范，从而为控制程序的可靠 性提供了科学分析。 混合系统的形式验证技术是对仿真技术的拓展：仿真技术从某一个初始状 态出发，一次只能检验系统的一条轨迹，即使进行了数千次仿真仍然可能错过一 些重要的非安全因素。而形式验证技术是在系统仿真的基础上，通过对系统可达 集的计算，一次性检查系统从某一个初始状态集合出发的所有轨迹，验证系统设 计的安全性。 近十年来，国际上有多个研究组从事混合系统形式验证的研究。欧洲在1 9 9 8 年正式启动混合系统验证计划( s ) ，其中包括法国v e r i - i a g 工作组、德国 d o r t m u n d 大学和欧洲其它各国科学家。美国的s t a n f o r d 大学、c a r n e g i em e l l o n 大学和c o r n e l l 大学也从事此类研究。现在己有的一些成果，从不同角度研究验 证问题，提供不同的验证工具，给出了多个工业验证实例。如h y t e c h 【”、 h y p e r t e c h 、d d t 【3 ”、c h e c k m a t e 、u p p a l 【3 6 】、k r o n o s 【3 ”、v e r i s h i f t 【3 8 l 和 v e r d i c t ! 跏。其中u p p a l 、k r o n o s 、v e r d i c t 和h y p e r t e c h 用超矩形表示可达集； v e r i s h i f t 用椭圆表示可达集；h y t e c h 、c h e c k m a t e 和d d t 用多面体表示可达 集。 由于可达集计算的复杂性，导致时间和内存的大量消耗，现有的验证技术与 工具仅适用于小规模的系统。目前混合系统验证方法所存在问题主要集中于算法 应用范围的局限性。 1 4 本文的内容和结构 本文主要讲述了混合系统形式验证原理，对可达集的流管道近似方法进行了 重点研究，针对流管道近似方法在非线性系统中存在的计算困难，提出了变时间 4 间隔的流管道近似方法，同时，根据流管道近似方法特性，给出在切换面附近开 始计算流管道近似的流管道逼近法和多面体逼近法。 通过对流管道近似方法的分析，提出一种新的计算切换面上可达集的方法。 用凸多面体来包裹切换面上的实际可达集，利用优化算法求出包裹的最小凸多面 体，而实际可达集的求取是通过对初始区域上某点，计算其对应于切换面上的点 的数值解，将数值解嵌入优化算法中得到。 对状态划分的解决方案，论述一种基于反例的状态划分方案，只针对与验证 规范有关的状态进行划分，在某种程度上有效地避免由于再划分整个状态空间导 致的状态空间爆炸问题；在对反例状态的划分上，由于暂时无法精确划分状态使 之与该状态的后续子状态相对应，给出了多次“对半”剖分的划分方案，经过多 次地划分，这种“对半”剖分方法能够确定划分后的反例状态集合与后续子状态 相对应。基于状态反例的划分思路和对状态反例进行对半剖分的划分方法， 有效地避免了划分过多的情况，在某种程度上抑制了状态的膨胀。 论文的结构大致如下： 第一章介绍了混合系统的背景与意思，讲述了混合系统理论的发展概况与混 合系统的形式验证。 第二章论述了混合系统的建模与分析，列举了几种混合系统的混合自动机模 型，对基于模型检验的混合系统形式验证原理作了简要概括，给出形式验证方法 和过程。 第三章详细介绍了混合系统的形式验证原理。对混合系统进行离散化，在阙 值面上对状态空间划分构建迁移系统，通过流管道近似方法计算可达集确定迁移 关系，利用仿真原理使迁移系统为原系统近似的商迁移系统。 第四章针对流管道近似方法在非线性系统中存在的计算复杂性，提出了变时 间间隔的流管道近似方法；根据流管道近似方法特性，给出在切换面附近开始计 算流管道近似的逼近法；同时提出了一种的计算流管道与切换面的交集的新方 法，即直接用多面体包裹在切换面上实际可达集；最后论述一种基于反例的状态 划分方案，和对半剖分的划分方法，在一定程度上避免了由于划分导致的状 态空间爆炸问题。 第五章结合具体实例的验证过程，分析了第四章提出方法的验证结果，通过 验证结果的对比分析，得出上述方法的合理性。 第六章对研究内容进行了总结，对工作的成果与不足进行了分析，介绍了当 前混合系统研究的热点和难点，指出了下一步所要进行的工作。 第二章混合系统建模与分析 本章介绍了与混合系统模型有关的一些数学基础，并给出了混合系统的序列 性质分析，列举了几种混合系统的混合自动机模型。 2 1 混合系统的性质分析 混合系统研究涉及多门学科的知识，大致可分为两类，连续方面和离散方面 的知识。具体地讲，有微分方程理论、微分几何、拓扑学、连续系统控制论、数 理逻辑、p e t r i 网和自动机，以及模型论等。 2 1 1 微分方程和微分包 混合系统无论是连续方面还是离散方面，都是用微分方程表示的，包括线形 和非线形微分方程。保证混合系统的极值点的存在性和唯一性是混合系统划分的 条件。 对于x ：且j x = r ”和常微分方程： 兰o ) = ，( x ( f ) ，f ) ，x ( o ) = 而 “l 其中f ：兄r + - - r 是向量场。其解的存在性有以下定理； 定理2 1 ( 局部存在性和唯一性) 假定f ( x ，f ) 在t 上是逐段连续的，并且存在厶，t 0 ，对于所有的 x , y b = 缸r ：睁一x 。6 r 和所有的r 【o ，川，使得，r ) 满足上枷曲汜条件： 忱x ，t ) - f ( y ，t ) l i z l l x - 川i 那么存在艿 0 ，使得系统f ( x ，t ) 在 o ，棚上有唯一解： 并( f ) = x o + 【，( x ( 力，r ) d r 定理2 2 ( 全局存在性和唯一性) 假定f ( x ，力在f 上是逐段连续的，并且存在l ，h 0 ，对于所有的x , y r 。和 所有的r 【o , t 】，使得， ，t ) 满足条件： i 矿( 工，t ) - f ( y ，) 忙l l l x - y l i i f ( x o ，f ) 忙而 那么系统f ( x ，f ) 在【o ，刀上有唯一解。 微分包是微分方程的一般化，它是微分方程的抽象和控制系统的抽象。是人 们表征子系统迁移的形式 令f ：r 。斗2 2 ，则微分包 j o ) f o f ) ，x ( o ) = r 4 在 o ，t 】五+ 的一次运行是指可微函数z ：【o , t 】一r ”且x ( o ) = x 0 时，使得对于所 有的te 【o , t 】有： j ( f ) ，( x p ” 注意：微分包是非确定性的( n o n - d e t e r m i n i s t i c ) ，即对于同一初始条件可能 有多个运行结果。 2 1 2 混合系统的性质分析 应用前述，混合动态系统用混合自动机表示为日= ( q ，x ，i n i t ，f ，i n v ，e ，g ，r ) 令h y b ( w ) 表示变量的混合系统序列集合，则有： h y b ( w ) = p ，m ) ：f t ，国：f _ 形 时间r 为混合系统的连续子系统的时间集合，矽为包括所有连续予系统在内的状 态变量集合。如果混合自动机具有离散输入矿和连续输入y ，那么混合自动机写 作日= ( q ，z ，v ，y ，1 n i t ，f ，i n v , e ，g ，震) ，并用v a r ( h ) 表示q u x u 矿u y ，而混合 系统的可能运行记作i - i 互h y b ( q u x u v u n 。 定义混合时间轨迹 混合时间轨迹f 是在实数集合上的有限或无限的间隔序列，f = ) ，i n ， 满足以下条件： 1 ) 与是混合时间轨迹f 闭集合，除非f 是有限序列并且正是最后一个间隔， 它可以是左闭右开。 2 )