（交通信息工程及控制专业论文）ATS系统内部通信协议的设计及形式化验证.pdf

中文摘要 摘要：在c b t c ( c o m m u n i c a t i o n s b a s e dt r a i nc o n t r o l ，基于通信的列车控制) 系 统中，a t s ( a u t o m a t i ct r a i ns u p e r v i s i o n ，自动列车监控) 子系统实时监控列车运 行线路及列车运行状况，为调度人员提供实际运行线路上的大量现场信息。a t s 系统设备间的数据交互都是通过通信协议来完成，通信协议将系统内的设备联系 起来形成一个有机的整体，从而使系统中各子单元共同协作完成特定的功能，通 信协议质量的好坏直接关系到系统功能的完成和系统性能的优劣。 传统的通信协议验证大多是通过大量的实践来检验协议设计的正确性，这样 的验证方法无法从理论的角度来证明通信协议设计的正确性，同时也很难发现一 些隐藏很深的设计漏洞。所以应用形式化的验证方法对协议的设计模型进行验证 是非常有意义的。本文对实验室自主研发的a t s 系统的内部通信协议进行了设计 和形式化的验证工作，并给出了验证结果分析。 首先，介绍了形式化的验证方法，形式化验证方法的意义在于它能够证明待 验证系统模型设计的正确性，它会遍历系统内所有的状态迁移路径来验证模式是 否满足指定的性质。接下来阐述了符号模型检验方法的原理及其支持工具s m v ， 具体说明了s m v 的基本工作原理和语法，同时指出了在使用s m v 的过程中发现 的一些问题。 其次，依据需求对内部通信协议进行了设计。先简要介绍了设计工具r a t i o n a l r o s e ，接着阐述了a t s 系统内部通信协议的需求以及相应的设计策略，简单来说 内部通信协议的需求即通信协议要满足a t s 系统对数据传输的需求，接着针对需 求进行了内部通信协议的架构设计和模块划分工作，最后以u m l 类图、序列图和 活动图的方式对内部通信协议的功能进行了概要设计，为形式化验证工作提供了 建模基础。 最后，使用形式化的方法对内部通信协议关键模块进行了验证，通过抽象内 部通信协议的有限状态迁移图，用s m v 语言对待验证的模型进行描述，用c t l 公式对待验证的性质进行表达。其中对于临界区的操作模型进行了改进，使得验 证最终得以通过，对于数据冗余、处理关键数据报文处理的形式化验证均一次通 过。通过形式化验证证明了通信协议关键模型设计的正确性，进而保证了内部通 信协议的开发质量。 关键词：c b t c ；a t s ；符号模型检验；s m v ； 分类号：u 2 8 5 a b s t r a c t a b s t r a c t ：i nc o m m u n i c a t i o n - b a s e dt r a i nc o n t r o ls y s t e m ，a u t o m a t i ct r a i n s u p e r v i s i o ns u b s y s t e mm o n i t o r st r a i nl i n e sa n dp r o v i d e sv a r i o u sa s p e c t so fp r a c t i c a l r u n n i n gi n f o r m a t i o nf o rs c h e d u l i n gs t a f f e x c h a n g i n gd a t aa m o n gd e v i c e so fa t s s y s t e ma r ec o m p l e t e dt h r o u g hi n n e rc o m m u n i c a t i o np r o t o c o l ，c o m m u n i c a t i o np r o t o c o l i sj u s tl i k ec h a n n e l so fs y s t e m ，w h i c hm a k e ss y s t e me q u i p m e n tl i n k e dt oa no r g a n i c w h o l e ，s ot h a te a c hs u b - s y s t e mm o d u l e st o g e t h e rt oc o m p l e t et h es p e c i f i c a lf u n c t i o n ， g o o do rb a dq u a l i t yo fc o m m u n i c a t i o np r o t o c o li sd i r e c t l yr e l a t e dt os y s t e m sf u n c t i o n , p e r f o r m a n c ea d v a n t a g e sa n dd i s a d v a n t a g e t r a d i t i o n a lc o m m u n i c a t i o np r o t o c o lm o s t l yv e r i f i e dt h ec o r r e c t n e s so fp r o t o c o l d e s i g nb yal a r g en u m b e ro fe x p e r i m e n t t h i sm e t h o dc a n tp r o v et h ec o r r e c t n e s so f t h e d e s i g no fc o m m u n i c a t i o np r o t o c o la tat h e o r e t i c a lp o i n to fv i e w , b u ta l s ov e r yd i f f i c u l t t of i n ds o m eh i d d e nd e s i g nb u g s t h e r e f o r e ，t h ev e r i f i c a t i o nt od e s i g nm o d e li sv e r y m e a n i n g f u lb yf o r m a lm e t h o d i nt h i sp a p e r , w ed e s i g n e da n dv e r i f i e d t h ei n n e r c o m m u n i c a t i o np r o c o t o lo fr e s e a r c h i n gi n d e p e n d e n t l ya t ss y s t e mi no u rl a b o r a t o r y , a t t h es a m et i m e ，w ea n a l y s e dt h ev e r i f i c a t i o nr e s u l t f i r s t l y , w ei n t r o d u c e d t h ef o r m a lv e r i f i c a t i o nm e t h o d ，t h em e a n i n go ff o r m a l v e r i f i c a t i o nm e t h o di sw h i c hc a np r o v et h ec o r r e c t n e s so fs y s t e m a t i c ，b e c a u s ei tw i l l t r a v e r s a la l lt h es t a t es p a c ea n dj u d g ee v e r ys i t u a t i o n i s m t h e n ，p a p e ri n t r o d u c et h e p r i n c i p l eo fs y m b o l i cm o d e lc h e c k i n ga n ds m vt o o l ，a tt h es a n l et i m e ，i n t r o d u c i n gt h e b a s i cw o r k i n g p r i n c i p l ea n dt h eb a s i cs e m a n t i c so fg r a m m a ro fs m v , p o i n t i n g o u ts o m e p r o b l e m sw h i c h w e r ef o u n di nt h ec o u r s eo fu s i n gs m v s e c o n d l y , p a p e rd e s i g n e di n n e rc o m m u t a t i o np r o t o c o lb a s e do nd e m a n d p a p e r i n t r o d u c et h ed e s i g nt o o l b a rr a t i o n a lr o s ei nb r i e f , t h e na r t i c l ed e s c r i b e sn e e d so ft h e c o m m u n i c a t i o np r o t o c o la t ss y s t e ma n dc o r r e s p o n d i n gd e s i g ns t r a t e g y s e c o n d l y , w e c a r r i e do u tm o d u l ep a r t i t i o na n dm o d u l ed e s i g no fa t ss y s t e mi n n e rc o m m u n i c a t i o n p r o t o c 0 1 f i n a l l y , p a p e rd e s c r i b eas u m m a r yo fd e s i g np r o c e s so fm o d u l ew h i c hp r o v i d e t h eb a s i sf o rt h el a t t e rf o r m a lv e r i f i c a t i o n f i n a l l y , p a p e rv e r i f i e di n n e rc o m m u n i c a t i o np r o t o c o l w i t hf o r m a lm e t h o d ，b yt h e m e a n so fa b s t r a c t i n gt h ei n f i n i t es t a t et r a n s f e rd i a g r a m ，w eu s es m vl a n g u a g et o d e s c r i b et h em o d e lw h i c hw i l lb ev e r i f i e da n du s ec t lf o r m u l at oe x p r e s st h ep r o p e r t y w h i c hw i l lb ev e r i f i e d w ei m p r o v e dt h em o d e lo fo p e r a t i n gt h ec r i t i c a lr e g i o n a l ，s oa s t ov e r i f ys u c c e s s f u l l yf i n a l l y , t h ev e r i f i c a t i o ns i n g l ep a s sf o rt h em o d e l so fp r o c e s s i n g c r i t i c a ld a t am e s s a g e ，d a t ar e d u n d a n c yp r o c e s s i o n , d a t ao u t o f - o r d e r p r o c e s s i o n t h r o u g ht h ev e r i f i c a t i n go fi n n e rc o m m u c a t i o np r o t o c o l ，w ep r o v et h a tt h ep r o t o c o l w h i c hw e d e s i g n e di sc o r r e c ta n de n s u r et h eq u a l i t yo f i n n e rc o m m u n i c a t i o n s k e y w o r d s ：c b t c ；a t s ；s y m b o l i cm o d e lc h e c k i n g ；s m v c l a s s n 0 ：u 2 8 5 v 图索引 图la t s 系统设备布置简图2 图2a t s 系统应用程序和通信协议关系4 图3k r i p k e 结构和无限可计算树的转换1 2 图4s m v 工作原理1 4 图5 通信协议层次结构1 9 图6 应 l j 程序与通信传输类库交互2 0 图7 通信协议与应刚接口2 4 图8 通信传输类库层次结构。2 4 图9 数据发送类2 6 图l o 数据接收类2 6 图l l 通信传输管理类2 7 图1 2 通信传输类库初始化序列图2 8 图1 3 通信传输类库数据发送序列图2 8 图1 4 数据接收概要流程2 9 图1 5 数据处理概要流程3 0 图l6 数据插入上传列表概要流程3l 图l7 数据上传概要流程3 2 图1 8 关键数据报文发送概要流程3 3 图l9 关键数据报文接收概要流程3 4 图2 0 数据接收状态迁移图3 6 图2 l 数据处理状态迁移图3 6 图2 2s m v 验证结果3 8 图2 3 改进模型后数据处理状态迁移图3 9 图2 4 改进模型后s m v 验证结果一4 0 图2 5s m v 验证结果4 l 图2 6 数据冗余处理状态迁移图4 2 图2 7s m v 验证结果4 4 图2 8 数据发送方状态迁移图4 5 图2 9 数据接收方状态迁移图4 6 图3 0 发送方剑接收方信道状态迁移图4 7 图3 l 接收方到发送方信道状态迁移图4 7 图3 2s m v 验证结果4 9 图3 3s m v 验证结果5 0 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均己在论文中作 了明确的说明并表示了谢意。 学位论文作者躲毫主聿签字魄2 口哆年7 月7 日 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 提供阅览服务，并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。 同意学校向国家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 、 主 导师签名： 弋 磅尚 同 签字日期：加研年6 月仃r 致谢 研究生两年的学习生涯即将结束，在这两年中我有幸参加了实验室的科研项 目基于通信的城轨c b t c 系统的研究，收获颇丰，个人能力也有了较大的提升。 在这里我要向这两年中帮助我、关心我的老师和同学致以最诚挚的谢意。 本论文的工作是在我的导师唐涛教授的悉心指导下完成的，唐涛教授严谨的 治学念度和科学的工作方法给了我极大的帮助和影响。在此衷心感谢两年来唐涛 教授对我的关心和指导。唐老师严谨求实、精益求精的科研态度和真诚待人、朴 实无华的生活作风将是我一生学习的楷模。 轨道交通控制与安全国家重点实验室郜春海副教授、马连川副教授、王海峰 副教授、黄友能副教授、刘波老师、周达天老师、王悉老师悉心指导我们完成了 实验室的科研工作，在学习上和生活上都给予了我很大的关心和帮助，在此向他 们表示衷心的谢意。 实验室的张建明老师在我的科研工作中给予了精心细致的指导，对于所问问 题总是能给予耐心的讲解，他那忘我的工作热情和广博的学识都深深的感染着我、 激励着我，在此向他致以真诚的谢意。 赵林老师、谢雨飞、王义惠、许永成、简锐锋等向我提供了一些论文资料和 相应文档，并对论文的选题和编写提出了许多宝贵建议，必不厌其烦的给我热心 讲解，使得我的论文得以顺利完成，在此向他们致以由衷的谢意。 在实验室工作及撰写论文期间，实验室的夏夕盛、魏永真、王洪涛、李晓艳、 李雁、刘辉、单振宇、魏国栋等同学对我论文中的研究工作给予了热情帮助，在 此向他们表达我的感激之情。 另外也感谢我的家人和女朋友，一直以来他们都默默的关心我、支持我、激 励我，使我能够无所牵挂，一心向前，他们是我最坚强的后盾，也正是由于他们 的理解和支持使我能够在学校专心完成我的学业。 最后，衷心感谢为评阅论文和参与论文答辩而付出辛勤劳动的各位专家学者， 感谢您的宝贵意见! 本论文由国家自然科学基金项目“列车运行控制及组织的基础理论与关键技 术研究”( 项目号：6 0 6 3 4 0 1 0 ) 支持。 1 绪论 目前中国正处在快速城市化的进程中，城市的交通问题( 诸如拥挤、阻塞和噪 声等) 也表现得越来越突出。交通拥挤、资源闲置以及环境污染的问题越来越严重， 不符合可持续发展战略的要求【l 】。发展公共交通是解决城市交通问题的一种非常重 要的途径，而城市轨道交通以其运量大、运营速度快、准点性好等优点而倍受青 睐。列车运行控制系统作为城市轨道交通系统的核心单元，其控制性能的优劣必 然影响到轨道交通事业的发展。 基于通信的列车运行控制( c o m m u n i c a t i o n s - b a s e dt r a i nc o n t r o l ，c b t c ) 系统 独立于轨道电路，采用高精度的列车定位和连续、高速、双向的数据通信，通过 车载和地面安全设备实现对列车的控制，现已成为列车控制系统发展的方向，可 满足铁路运输高速化、信息化、网络化的发展。目前国内对于c b t c 系统的研究 还处于起步阶段，为了早同实现c b t c 系统国产化工作，北京交通大学轨道交通 控制与安全国家重点实验室早在2 0 0 5 年就承担了“基于通信的城轨c b t c 系统研 究与开发 的科研项目。目前，该c b t c 系统已经完成了大连快轨的中试试验， 即将应用在北京亦庄线。 作为c b t c 系统的子系统列车自动监控( a u t o m a t i ct r a i ns u p e r v i s i o n ，a t s ) 系统实时监控并动态显示列车的运行状态和线路设备使用状况，为列车调度人员 和现场工作人员提供清晰真实的动态画面【2 】。同时a t s 负责进路的自动排列，当 列车运行偏离列车时刻表或设备出现故障造成列车延迟时，a t s 系统能为调度中 心调度人员提供实时调度平台及时进行列车运行调整，并能为车站工作人员及时 排除故障提供故障报警提示，供其对整个运行系统进行实时监督控制。可见，a t s 系统可大大提高列车运营的效率，将列车运行、调度推向智能化发展。 a t s 系统设备间的数据交互都是通过通信协议来完成的，通信协议就好比系 统的经脉，将系统内的设备联系起来形成一个有机的整体，从而使系统中各子单 元共同协作能完成特定的功能，由此可见通信协议在系统内部无处不在，通信协 议质量的好坏直接关系到系统功能、性能的优劣，甚至会影响系统所能够完成的 特定功能。 传统的通信协议丌发方法是非形式化的，在设计完成后大都通过大量的实践 来检验协议的正确性，这样的方法无法从理论的角度来证明通信协议设计的丁f 确 性，同时也很难发现一些隐藏很深的设计漏洞。但在实际情况中，如果通信协议 真的在交付后出现了问题，可能会造成重大的损失。鉴于这种情况，对通信协议 的关键设计模型进行形式化验证是必要的，也是非常有意义的。 本章将简述自主研发的a t s 系统的基本原理、系统组成及各部分的功能。首 先，介绍了a t s 系统内部通信协议在a t s 系统中的作用；其次介绍了符号模型 检验的发展和基于符号模型检验工具s m v 的基本原理：最后介绍了论文的结构安 排。 1 1 课题研究背景 1 1 1 列车自动监控系统概述 列车自动监控( a u t o m a t i c t r a i ns u p e r v i s i o n ，a t s ) 系统实时监控线路和列车 运行状况，并动态显示列车的运行状态和线路设备使用状况，为列车调度人员和 现场工作人员提供清晰真实的动态画面。同时a t s 负责进路的自动排列，当列车 运行偏离列车时刻表或设备出现故障造成列车延迟时，a t s 系统能为调度中心调 度人员提供实对调度平台及时进行列车运行调整，并能为车站工作人员及时排除 故障提供故障报警提示，供其对整个运行系统进行实时监督控制。 a t s 系统的设备布置包括：位于控制中心的中央a t s 设各、位于各个设各集 中站的a t s 区域车站设备、位于非设备集中站的a t s 终端设备以及位于车辆段的 a t s 终端设备。殴备布置简图如图1 所示： q 。魍。熏。震，黑霎； 陆一- - 。 父“：a占。、 匹曩圆妇盘嚣疆b 匹蠹蠹譬= 函 臼 1 1 - j * 镕* ” 幽l a t s 系统设备布置简幽 f i g u r e 】a t s s y s t e me q u i p m e n t l a y o u t d i a g r a m 臼 0 一 a t s 系统，主要包括a t s 控制中心、设备集中站a t s 、非设备集中站a t s 和 车辆段a t s 四部分。具体各部分功能简介如下： ( 1 ) 控制中心 a t s 系统控制中心的作用是使中心调度员能监督和控制全线轨道交通列车运 营，了解实时交通运营情况。调度员利用a t s 系统提供的先进运营管理方式，可 以减轻调度人员的工作强度，实现交通运输指挥自动化。主要功能如下： 正线信号设备的远程自动及人工控制功能； 列车信息的追踪和管理； 运行图的编制和在线修改功能； 列车的运营按运行图自动调整： 报警事件及各种统计报表的管理； 系统的时钟同步功能： 历史数据的记录和回放； 图形化的操作员界面； 列车运行和信号设备的模拟以及人员培训。 ( 2 ) 设备集中站 当a t s 系统工作在中心控制模式时，设备集中站的a t s 作为控制中心设备和 微机联锁设备之间的接口，采集现场的实时信息并传输到中心，同时将中心的命 令传到微机联锁设备。一旦中心a t s 故障，则由a t s 车站设备进行控制。其主要 功能概括如下： 在站控模式下实现对集中站管辖范围内各车站信号设备的人工控制功能； 在站控模式下实现对集中站管辖范围内各车站站台相关的人工控制功能； 集中站管辖范围内各车站站台相关的显示功能； 列车识别号显示和追踪； 控制发车表示器显示； 向车站广播系统提供列车接近条件，作为列车到达预报的自动广播触发信号。 ( 3 ) 非设备集中站 非设备集中站的a t s 人机界面显示与设备集中站的人机界面显示相同，但是 其主要支持扣车、取消扣车、催发车等操作，但是不支持进路的排列和取消等操 作。也就是说，其功能是相应设备集中站a t s 人机界面的子集。 ( 4 ) 车辆段a t s 车辆段a t s 设备的功能为车辆段范围内的信息采集，包括停车库线和进、出 车辆段的信号机。系统将采集的信息通过网络传输到控制中心，使控制中心能够 监视到车辆段的信号设备状态和相关列车信息。在车辆段信号设备室和派班室还 设有a t s 终端设备，通过车辆段不同的终端能进行列车车次、司机以及当天列车 运行时刻表的查询，并能进行司机和车辆信息的输入。 1 i 2a t s 系统内部通信协议 通信协议是位于通信网络中的通信实体之间相互交换信息时定义的一组规则 1 3 】。对于网络应用来说，通信协议是系统内设备间沟通的桥梁，所以通信协议在系 统中一直处于核心地位。 a t s 系统设备众多，在控制中心有中心应用服务器、调度员工作站、计划员 工作站、通信前置机、数据库服务器等设备；在每个车站分别有a t s 车站分机和 操作员工作站；在车上有a t s 车载监视终端。a t s 系统正常工作时，这些设备问 都需要交换数据，协同工作才能完成a t s 系统的功能，a t s 系统内部通信协议的 作用就是提供数据传输功能。 应用只负责完成指定的功能而不必考虑怎样进行数据传送，当应用主程序产 生数据后，只需通过协议的接口函数将数据和目的地址告诉协议即可，数据传输 和数据传输的可靠性完全由协议保障。应用程序和通信协议的关系可以概要的描 述如下： u d p 协议1 i p 协议一 庶用程序 f 应用处理模块 l 一一- l 丽矗错嗣f 珥未通酾 隧皿层翱隧：i 义层，霸 应用层 传输层 网络层 嘲络接口层 图2a t s 系统应片j 程序和通信协议关系 f i g u r e2t h er e l a t i o no f a p p l i c a t i o no fa t ss y s t e ma n dc o m m u n i c a t i o np r o t o c o l 如图2 所示，a t s 系统通信协议分为内部通信协议和外部通信协议。内部通 信协议是指负责a t s 系统内部设备问通信的协议，例如a t s 车站分机、操作员工 作站、通信前置机、调度员工作站、应用服务器等内部设备通信是通过内部通信 协议。而对于a t s 车站分机和联锁( c i ) 、区域控制器( z c ) 、车载控制器( v o b c ) 之问的通信则是通过外部通信协议( 即c b t c 系统通信协议) 。本文的研究工作主 4 要是针对a t s 系统内部通信协议。 a t s 系统内部通信协议应该具备以下基本功能： 通信协议设计应该具有清晰的层次结构和合理的功能模块划分； 通信协议应该能提供合适的接口供其他程序使用； 通信协议能够利用合理的机制保障数据报文重复、损坏、乱序和丢失等情况： 所有数据报文的接收和发送都是通过双网传送，协议能够进行双网冗余处 理： 对于完全自主研发的a t s 系统，内部通信协议的作用非常重要，因为内部通 信协议不但会影响系统内的数据交互，还可能产生不合时宜的数据对系统完成的 功能产生影响。所以，要想使a t s 系统运行可靠、稳定，高质量的通信协议是基 础。 a t s 系统内部通信协议运行的环境是有线局域网，实际中采用双网冗余传输。 由于内部通信协议的传输层是基于u d p 协议的，所以对于数据报文在传输过程中 的乱序、损坏、丢失等情况要有充分的考虑和相应的解决方案。 1 2符号模型检验技术及工具 通信协议传统的设计和检验方法有很大的弊端，主要体现在： 由于通信协议用自然语言来描述，所以不可避免的有含糊不清的描述，而这种 描述给开发人员与用户对需求的一致性理解及需求的正确执行制造了障碍； 自然语言的描述不能够提供逻辑的精确论证，带有模糊性和主观性； 通信协议的检验通常要通过大量的实践测试来发现问题，而对于那些只有在特 定条件下才会出现的问题，这种检验方法很难做到完全覆盖； 如果在协议实现后再来纠正协议的设计错误，代价往往是非常可观的。 在本文中，通信协议的设计采用统一建模语言u m l ，而对于通信协议的验证 我们使用形式化的验证方法。本文重点讨论形式化的验证方法。形式化的验证方 法能够从数学理论的角度来证明设计的j 下确性，对于那些越来越复杂的系统，如 果单纯依靠人来检查设计的正确性是不可能的，而形式化验证方法可以实现自动 分析和验证，所以得以迅速发展。本文通过对a t s 系统内部通信协议的设计提取 相关的有限状态迁移模型，接着通过形式化验证工具对该模型进行描述，最后对 该模型进行形式化的验证，进而从理论上验证设计的正确与否。对协议进行形式 化的验证可以判断设计模型是否满足一些关键系统性质，对我们的设计具有非常 重要的现实意义。 形式化的验证方法主要有分为两类：一类以逻辑推理为基础，另一类则以穷 5 尽搜索为基础【4 】。穷尽搜索方法统称为模型检验。模型检验是一种自动分析和验证 有穷状态并发系统的验证技术，适用范围广，速度快，而且充分自动化，是形式 化验证方法中非常重要的一种方法，但状态空间爆炸问题制约了它的实际应用。 在此基础上发展起来的符号模型检验，极大的缓解了模型检验状态空间爆炸的问 题，因此得到了广泛的使用，符号模型检验也是本文形式化验证工作的基础。 s m v ( s y m b o l i cm o d e lv e r i f i e r ) 是一个功能强大的符号化模型检验工具，在复 杂电路设计的验证中得到了广泛的应用。s m v 程序由两部分组成：有限状态迁移 系统和计算树逻辑( c o m p u t a t i o nl o g i ct r e e ) 公式t 5 。将有限状态迁移系统用s m v 语言描述后，输入到s m v 系统并运行s m v 系统后，若有限状态系统满足c t l 所 描述的属性，则输出真，否则输出假，并同时生成不满足属性的反例。 在s m v 系统中，系统状态集合和迁移关系都是用布尔公式隐式地表示，并在 符号状态空间上进行搜索。在大多数情况下，符号化表示一个集合比显示的表示 更紧凑【5 】。在s m v 中，布尔公式用高效率的o b d d ( o r d e r e db i n a r yd e c i s i o n d i a g r a m s ) 来表示和操作，而o b d d 有如下优点：对大多数布尔函数都比较紧凑： 存在唯一的表示形式；由高效算法来直接进行各种布尔运算和不动点运算。因此， s m v 有效地缓解了状态空问爆炸问题。 在协议的验证方面，s m v 也有强大的优势。它具有语法简单、描述全面等特 征，其语法形式与高级语言c 非常接近。综合考虑，本文决定使用s m v 作为a t s 系统内部通信协议的验证工具。 1 3选题目的及意义 为了能够保证a t s 系统内部设备间能够进行稳定、可靠的数据交互，所以必 须要有一个可靠、完备、统一的通信协议来保证。而如今通信协议的复杂性主要 体现在空间分布性、并发性、异步性、不稳定性和多样性，高质量的通信协议再 也不可能通过工程直觉方法设计，协议的完整性、正确性、安全性、可移植性和 标准化都难以得到保证p j 。 正是由于a t s 系统内部通信协议的重要性和复杂性，要想检验协议的设计是 否正确，完全依赖人来检验是不可靠的，形式化的验证方法能够自动、全面的对 系统的重要性质进行验证，同时对于s m v 工具来说当待验证的系统不满足待验证 的性质时，它能够给出反例路径告诉我们设计模型不满足验证性质的原因，开发 人员可以依据其提供的反例路径对模型进行改进，从而大大提高了协议丌发的效 率和质量，所以使用形式化的验证方法对通信协议的关键设汁模型进行验证是保 证通信协议开发质量的一种重要方法。 6 a t s 内部通信协议最终要用c 撑语言实现，c 撑语言是完全面向对象的设计语言， 所以设计工作也是完全面向对象的，在设计中，每一个功能模块都是封装成相应 的类，模块之间的交互通过参数传递实现，本文的验证工作也是分别对各个功能 模块的设计进行验证，主要验证该功能模块是否能够j 下确的执行该模块的功能， 例如对于数据冗余处理模块，我们验证该模块是否能够达到数据冗余处理的目的。 验证的目的是证明内部通信协议关键模型设计的正确性。 1 4本文的结构安排 第一章为绪论，主要介绍了选题背景。首先，介绍了a t s 系统的组织结构、 系统功能和内部通信协议的作用；其次，简要介绍了符号模型检验和其支持工具 s m v ；最后说明了论文选题的目的和意义，阐述了为什么要对协议进行形式化的 验证以及本文要达到的目标。 第二章详细介绍了形式化的验证方法。首先介绍了模型检验方法及其建模步 骤，同时指出了模型检验的缺点；其次，介绍了在模型检验基础上发展起来的符 号模型检验，符号模型检验优势及其被广泛使用的原因；最后，介绍了符号模型 检验工具s m v ，阐述了s m v 工具的基本工作原理，s m v 的语法语义以及本人在 使用s m v 工具时发现的几点问题。 第三章详细介绍了a t s 系统内部通信协议的设计，设计工具使用r a t i o n a l r o s e 。首先，说明了对a t s 内部通信协议的需求分析和设计策略；其次，根据需 求阐述了内部通信协议的设计架构与设计原则及其模块划分的依据和划分结果； 最后，对协议功能模块进行了概要设计，为下一章节的协议形式化验证工作提供 了建模基础和参考。 第四章主要是对a t s 内部通信协议的形式化验证过程及验证结果分析。本文 分别对协议临界区操作、数据冗余处理、关键数据报文的处理进行了形式化的验 证并给出了验证结果，对于不满足性质的模型进行了改进。最终证明了内部通信 协议关键模型设计的j 下确性。 第五章对全文进行了总结，提出了论文的不足之处，接着提出了对研究课题 的展望。 7 2 形式化验证方法 验证方法主要分为非形式化方法和形式化方法两大类。非形式化的方法不能 对待验证系统进行完全的覆盖验证，也无法从理论上证明设计的正确性。而形式 化验证方法由于建立在数学理论的基础上可以十分精确的描述目标系统，并且能 够穷尽系统状态，做到完全覆盖的验证，并且可以自动的对设计模型进行验证， 所以形式化的验证方法得到了快速的发展。 2 1形式化验证方法概述 形式化验证方法以数学理论为基础，用形式推理的方法来证明从某些前提可 以推出某结论，这种方法近似于数学中的证明。形式化验证方法利用形式逻辑和 离散数学技术对系统建立模型，最后用数学手段证明系统设计和实现满足系统功 能和安全性要求。形式化方法能够清晰、抽象、精确的描述目标系统及其性质， 并对描述的系统进行验证，能够大大提高系统的安全性和可靠性，使用形式化方 法能发现非形式化方法不易发现的问题，从而使开发人员更加深入的理解系统 6 - - 8 1 o 形式化验证方法是形式化方法中的一种，就形式化方法而言，其还包含形式 化描述方法。 ( 1 ) 形式化描述方法 形式化描述方法是一个描述系统及其性质的过程，形式化规范描述使用具有 严格数学定义的语义和语法来描述系统。从对系统的描述上讲又可分为两类：一 类是系统或者程序的描述，另一类是系统性质的描述。 被描述的系统特性包括行为特性、时间特性、性能特性和内部结构等。形式 规范语言按照描述系统的特性可以分为三类：描述顺序行为( 典型的语言有z 、b 、 v d m ，这类方法中使用集合、关系和函数等数学结构来表示状态；用前置条件和 后置条件来表示状态转移) 、描述并发系统行为( 典型有c s p 、c c s ，时序逻辑和自 动机模型) 和集成的形式规范方法( 典型的s d l 和r a i s e ，它们把两种不同方法结 合起来，既能表示复杂的状态类型又能描述并发系统的特性) 【9 】。描述系统性质的 语言主要有计算树逻辑、线性时序逻辑等。 ( 2 ) 形式化验证方法 形式化验证方法主要分为两类：定理证明和模型检验。定理证明根据公理和 形式推演规则来验证设计是否能满足要求，由于需要人工干预，能处理的设计规 8 模较小，发展比较缓慢。 逻辑推理有s e q u e n tc a l c d u s 、n a t u r a ld e d u c t i o n 、r e s o l u t i o n 和h o m e 1 0 9 i c 等方 法。穷尽搜索方法统称为模型检验。这类方法与系统以及系统性质的表示有很大 的关系，比如说符号模型检验，其基本原理是用命题逻辑公式表示状态转换关系， 用不动点算法计算状态的可达性以及这些状态是否满足指定的性质【m l 。 形式化验证方法在电路设计和协议设计方面都得到了广泛的应用。逻辑推理 的不足之处在于推理的难度。对于稍微复杂一点的系统，自动化的推理就难以胜 任。人工推理的缺点是费时费力。如果一个定理推不出来，并不能说明这个定理 不成立，很可能是推理方法和策略应用不当【6 】。模型检验的好处在于它有全自动的 检测过程，并且如果待验证的模型不满足指定性质，它能给出一个反例路径告知 不满足这个性质的理由。因此，我们可以根据反例对我们的系统进行改进。模型 检验的不足之处是它所能验证的是有限状态模型，对于协议而言，需要有一个从 任意状态到有限状态的建模过程。并且这样的模型的状态空间可能会面临“状态 空间爆炸 的问题。 ( 3 ) 模型检验 模型检验( m o d e lc h e c k i n g ) 是一种面向有穷状态并发系统的验证技术，是形 式化验证方法中很重要的一种方法。它最早由c l a r k e 和e m e r s o n 等人在1 9 8 1 年提 出，主要通过显示状态搜索或隐式不动点计算算法来验证有穷状态并发系统的命 题性质。模型检验可以从数学上完备的证明设计是否与设计规范一致【1 4 1 ，其主要 原理是用计算逻辑树( c t l ) 描述并发系统的性质，用有限状态迁移系统来表示系 统的设计，通过遍历状态迁移图来检验用c t l 描述的系统性质。模型检验适用范 围比较广，而且速度快且充分自动化，如果计算机处理能力足够大、计算时蒯足 够长，那么模型检验过程总能终止并给出待验证性质的真假，并且在待验证性质 为假的时候，能够提供反例路径供设计人员进行模型的改进，因此，模型检验在 形式化验证领域越来越受到人们的青睐。 目前模型检测已被应用于计算机硬件、通信协议、控制系统、安全认证协议 等方面的分析与验证中，取得了令人瞩目的成功，并从学术界辐射到了产业界。 现在已经有了许多的形式验证工具的提供商，专门设计制作模型检验工具。诸如 微软之类的许多大公司都已开始在其产品开发中逐渐采用模型检验的方法。在学 术界，模型检验技术的研究与争论也比较广泛而活跃，优秀高效的模型检验工具 正不断地涌现。a p n u e l i 指出，验证工程( v e r i f i c a t i o ne n 西n e 硎n g ) 正在形成。 ( 4 ) 模型检验的步骤 对于一个待验证的系统，模型检验一般遵循一下的步骤： 建立模型 9 通过模型检验工具把待验证系统的模型转化为验证工具所能表达的模型，该 模型一定是有穷状态迁移系统。在建立系统模型的过程中，应该忽略一些不必要 细节，以节约时间、空间资源使得验证得以顺利进行。 性质描述 待验证的系统性质用线性时序逻辑或计算树逻辑等描述，给出的性质描述应 该是完整的，因为模型检验只负责判断一个模型是否满足给定的性质，而不考虑 系统其他的性质。 性质验证 对系统建立好模型后，将性质描述输入系统，模型检验能够自动化进行验证。 如果所验证的性质为假，那么模型检验工具会给出导致该性质为假的系统状态迁 移路径作为反例。 ( 5 ) 模型检验的不足 模型检验的优点是明显的，但模型检验也存在着严重的不足，从而导致模型 检验大范围的应用受到很大限制。首先， 搜索的可穷尽性要求系统模型状态有穷， 模型检验的基本的思想是基于状念搜索， 故模型检验不能直接对无穷状态系统进 行验证，所以对于任何待验证的系统都需要一个有限状态建模的过程【堪】。其次， 即使对于有穷状态系统，模型检验也面临着状态空间爆炸问题，因为在把并发系 统表示为状态迁移系统时，系统的状态数量会随着并发分量的增加呈指数增长， 因此当一个系统的并发分量较多时，直接对其状态空间进行搜索实际上是不可行 的。 为了能够解决状态空间爆炸问题使得模型检验可以广泛应用，一些重要的方 法被相继提出，主要包括符号模型检验方法、偏序归约、抽象技术、分解与组合 以及对称、o n t h e n v 、归纳方法等【1 5 1 。 2 2符号模型检验 符号模型检验相比传统的模型检验其采用o b d d s ( o r d e r e db i n a r yd e c i s i o n d i a g r a m s ，有序- - y 判决图) 表示布尔公式，能有效的缓解状态爆炸问题，故获得