（交通信息工程及控制专业论文）基于UPPAAL的RBC系统控车流程建模分析.pdf

中文摘要 摘要：r b c 系统是中国铁路c t c s 一3 级列控系统中的重要组成部分，u p p a a l 是 基于时间自动机理论的实时系统建模分析验证工具，使用u p p a a l 分析r b c 系统 控车流程，可以验证流程的特性，对于保证r b c 系统控车流程的安全性有着重要 的实际意义。 论文完成的主要工作如下： 1 介绍了时间自动机理论及其模型检验工具u p p a a l 的使用方法。 2 通过分析列车在r b c 系统控制下的运行过程，把r b c 系统控车流程分为 五部分：列车登录流程，正常控车流程，r b c 交接流程，列车注销流程和消息重 发流程。 3 基于时间自动机理论对r b c 系统控车的五个流程以及其他外部设备分别 进行了建模：根据研究对象的特点，在合理的抽象和假设之后，确定了各个模型 的状态，状态跳转路径和状态跳转的约束条件，得到了r b c 系统控车流程的时间 自动机模型。 4 使用u p p a a l 对r b c 系统控车流程的时间自动机模型进行了分析验证： 通过设置通道和全局变量，构造了时间自动机的积；使用模拟器，模拟了r b c 控 制列车运行过程，分析r b c 控制列车运行过程中的状态变化；使用验证器，通过 快速搜索整个系统的状态空间，验证r b c 系统控车流程的活性和j 下确性等各项特 性。 关键词：c t c s 3 列控系统；r b c ；时间自动机；u p p a a l ；建模分析 分类号：u 2 8 4 4 4 a bs t r a c t a b s t r a c t ：r b cs y s t e mi sa ni m p o r t a n tc o m p o n e n to fc h i n e s et r a i nc o n t r o ls y s t e m l e c e l3 ( c t c s - 3 ) u p p a a li sam o d e l i n g , a n a l y z i n ga n dv e r i f y i n gt o o lf o rr e a l t i m e s y s t e mb a s e do nt i m e da u t o m a t at h e o r y i ti sp o s s i b l et ov e r i f ys o m ep r o p e r t i e so f r b c s y s t e mt r a i n - c o n t r o lp r o c e s so fr b cb yu s i n gu p p a a l ，a n di ti ss i g n i f i c a n tf o r g u a r a n t e e i n gt h es a f e t yo ft r a i n - c o n t r o lp r o c e s s t h em a j o rw o r k so ft h i st h e s i sa r es u m m a r i z e da sf o l l o w i n g ： 1 t h i st h e s i si n t r o d u c e st i m e da u t o m a t at h e o r ya n dt h em e t h o do fu s i n gt h i s m o d e l t e s tt o o lu p p a a l 2 b ya n a l y z i n gt r a i ne o n t r o lp r o c e s s ，t h e r ea le5p a r t so ft r a i n c o n t r o lp r o c e s s ： t r a i nl o g i np r o c e s s ，n o r m a lc o n t r o lp r o c e s s ，r b ch a n d o v e rp r o c e s s ，t r a i nl o g o u tp r o c e s s a n dm e s s a g er e s e r l dp r o c e s s b a s e do nt h e s e5p r o c e s s e s ，r b cc a nc o n t r o lat r a i n 3 t h em o d e l so ft h e s e5p r o c e s s e sa n do t h e re x t e r n a le q u i p m e n tb a s e do nt i m e d a u t o m a t at h e o r ya r ee s t a b l i s h e d a f t e rr e a s o n a b l ea b s t r a c ta n da s s u m p t i o n ，t h es t a t e s o fe a c hp r o c e s s ，s t a t e st r a n s i t i o np a t ha n dc o n s t r a i n t sa r ed e t e r m i n e db a s e do nt i m e d a u t o m a t at h e o r y , s oa st oo b t a i nt h et i m e da u t o m a t am o d e lo ft h e5p r o c e s s 4 u p p a a li su s e dt oa n a l y s ea n dv e r i f yt h e s e5t i m e da u t o m a t am o d e l s b y s e t t i n gc h a n n e la n dg l o b a lv a r i a b l e s ，t h ep r o d u c to ft i m e da u t o m a t ai so b t a i n e d b y u s i n gs i m u l a t o r , t h ep r o c e s so fr b c c o n t r o lt r a i ni ss i m u l a t e d ，a n da n a l y z i n gt h es t a t e t r a n s i t i o no fr b ct r a i nc o n t r o lp r o c e s si sa n a l y z e d b yu s i n gv e r i f i e r ，v i aq u i c k l y s e a r c h i n gt h ew h o l es t a t es p a c eo fr b cs y s t e m ，a c t i v i t y , v a l i d i t ya n do h t e rp r o p e r t i e so f r b ct r a i nc o n t r o lp r o c e s sa r ev e r i f i e d k e y w o r d s ：c t c s - 3t r a i nc o n t r o ls y s t e m ；r b c ；t i m e da u t o m a t a ；u p p a a l ； m o d e l i n ga n da n a l y s i s c l a s s n 0 ：u 2 8 4 4 4 学位论文版权使用授权书 本学位论文作者完全了解北京交通大学有关保留、使用学位论文的规定。特 授权北京交通大学可以将学位论文的全部或部分内容编入有关数据库进行检索， 并采用影印、缩印或扫描等复制手段保存、汇编以供查阅和借阅。同意学校向国 家有关部门或机构送交论文的复印件和磁盘。 ( 保密的学位论文在解密后适用本授权说明) 学位论文作者签名： 译球 签字日期：少鸸年占月1 3 日 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工作和取得的研 究成果，除了文中特别加以标注和致谢之处外，论文中不包含其他人已经发表或 撰写过的研究成果，也不包含为获得北京交通大学或其他教育机构的学位或证书 而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作 了明确的说明并表示了谢意。 学位论文作者签名：签字日期：年月日 致谢 本论文的工作是在我的导师邱宽民教授的悉心指导下完成的，邱宽民教授严 谨的治学态度和科学的工作方法给了我极大的帮助和影响，并在学习上和生活上 都给予了我很大的关心和帮助。在此衷心感谢两年来邱宽民老师对我的关心和指 导。 在实验室的科研工作中，我得到了刘中田老师的悉心指导，顺利完成了实验 室的科研工作。刘中田老师对于我的科研工作和论文写作都提出了许多宝贵意见， 在此表示衷心的感谢。 在实验室工作期间，王海峰老师和燕飞老师都给予了我关心和帮助，在此向 他们表达我的感激之情。 在实验室工作及撰写论文期间，吕继东、刘超、陈磊、余学虎、杨旭文、刘 朔、秦岭、于涛、赵剑华、赵显琼、耿鹏等同学对我论文中的研究工作给予了帮 助，在此向他们表示感谢。 另外也感谢我的家人，他们的理解和支持使我能够在学校专心完成我的学业。 最后，衷心地感谢所有关心和帮助过我的其他老师和朋友们! 谢谢你们! 1 引言 铁路具有运力大、成本低、能耗小、全天候等优势，是国家重要的基础设施， 是国民经济的大动脉，是综合交通运输体系的骨干，为经济和社会的全面、协调、 可持续发展，发挥着巨大的促进作用。但是随着科学技术水平的日益提高、社会 的不断发展，我国铁路技术装备水平较低、不适应国民经济和社会发展要求的问 题日益突出。中国铁路需要一个跨越式的发展。 2 0 0 4 年1 月，国家原则通过中长期铁路网规划。规划到2 0 2 0 年，中国铁 路网总里程达到l o 万公里。而建设客运专线，是中长期铁路网规划最主要的 内容。为此，铁道部于2 0 0 7 年9 月发布了中共铁道部党组关于增强铁路自主创 新能力，推进和谐铁路建设的决定。决定设定了“十一五”期间，中国铁 路科技发展的十大目标。为实现“十一五 铁路科技发展目标，铁道部还提出了 对促进铁路技术装备水平快速提高具有全局性、战略性、带动性作用的1 0 项重大 专项，其中包括针对客运专线这种高速、高效运营环境下列车安全运行控制系统 的研究，即c t c s 3 级列控系统。 1 1 列控系统发展现状 列车运行控制系统是保证列车安全、高速和高效地运行的信号安全防护系统。 传统的列车控制系统以车站联锁设备为核心，控制命令从行车调度中心发出，经 车站联锁设备检查其正确性，然后排列所需进路，进行安全防护。为实现这种防 护，要对道岔进行锁闭，防止侧面行车冲突，排除进路的故障。随后，行车调度 员的行车指令以及进路的允许速度由车站联锁设备通过地面信号显示传达给列 车。列车司机通过了望，得到从车站联锁设备发出的行车命令。所以，列车运行 的安全由车站联锁设备和列车司机共同承担。如果司机不注意地面信号，或当列 车高速运行时误认地面信号，就会造成车毁人亡的事故【l 】。显然，这样的系统已经 不适应现代铁路向高速、重载方向发展的要求。因此，世界各国铁路纷纷研制和 开发出多种不同性能的列车运行自动控制系统。 列车运行自动控制系统a t c ( a u t o m a t i ct r a i nc o n t r 0 1 ) 就是对列车运行全过 程或一部分作业实现自动控制的系统。其特征为列车通过获取的地面信息和命令， 控制列车运行，并调整与前行列车之间必须保持的距离。列车运行自动控制系统 ( 简称列控系统) 是保证列车按照空间间隔运行的技术方法，它是靠控制列车运 行速度的方式来实现的1 2 j 。 1 1 1 国外列控系统现状 针对传统的列车控制系统存在的弊端，西方各国从不同方面改进系统，其中主 要以改变地面与车载之间的信息传输通道为突破口。如使用轨道传输地面信号和 控制命令，或者使用无线传输方式进行车地通信等，再辅以先进的车载计算机设 备来实现不同的速度控制方式，从而完成对列车运行的自动控制。这样，车载与 地面的信息交互更直接，减少人员参与，使列车运行安全可靠。 在上世纪8 0 - 9 0 年代，欧洲各国铁路纷纷开发出多种不同性能的速度监督系统 或列车自动控制系统，如法国的u 厂r 系统，德国的l z b 系统等。欧洲各国铁路采用 不同的信号制式，存在多种列车控制系统，过境运输列车必须装备多套设备，在 过境运行时切换。这种不兼容的状态，使列车运行速度受到限制，也给司机增加 了操作困难，极大地影响了欧洲铁路网的统一。 到了2 0 世纪9 0 年代，随着“欧洲大一统”进程的不断推进，为解决欧洲铁路的 互连互通问题，国际铁路联盟( u i c ) 提出以铁路专用全球移动通信网( g l o b a ls y s t e m m o b i l ed e v o t e dt or a i l w a y ，g s m r ) 为平台，欧洲点式应答器( b a l i s e ) 为列车定 位手段的欧洲列车控制系统( e u r o p e a nt r a i nc o n t r o ls y s t e m ，e t c s ) 。e t c s 是欧 洲铁路运输管理系统( e u r o p e a nr a i l w a yt r a f f i cm a n a g e m e n ts y s t e m ，e r t m s ) 的 核心，它涉及一系列技术文件、标准、规范和概念，范围从地面设备到车载设备， 从通信协议到信息码的格式，包括了信号安全和列车控制的各个方面。该系统采 用模块化结构，能根据功能需要和运营条件灵活配置系统。e t c s 根据运输功能需 求和系统运用条件，以分级的方式配置基本结构，通过标准化的系统，在提高系 统安全性的同时，解决了欧洲铁路互联互通的运营问题。 e t c s 分5 级【3 】： e r t m s e t c s 0 ：装备了e r t m s e t c s 的列车可在没有e r t m s e t c s 或没 有国家信号系统的线路上运行，或者e r t m s e t c s 系统在试运行。在列控等级转 换处设置欧洲应答器e u r o b a l i s e ，车载装设具有e u r o b a l i s e 传输功能的b t m 模块( 应 答器传输模块) 。 e r t m s e t c s s t m ：装备了e r t m s e t c s 的列车，在已经装备了某个a t p 系统制式的线路上运行。通过s t m 模块实现车载设备与原来信号系统的兼容。 e r t m s e t c s 1 ( w i t h o u ti n f i l1 ) ：现有信号系统+ 查询应答器+ 轨道电路。即利 用查询应答器构成的点式超速防护系统，列车行车控制命令变化不能及时送至运 行中的列车，保留地面信号机。 e r t m s e t c s 1 ( w i t hi n f i l1 ) ：现有信号系统+ 查询应答器+ 轨道电路+ 欧洲环 线或欧洲无线( g s m r ) 。即利用欧洲无线或欧洲环线构成的接近连续式列超速防护 2 系统，保留地面信号机，该方式可提高通过能力。 e r l r m s e t c s 2 ：轨道电路+ 查询应答器+ g s m r 。即通过g s m r 连续传送运 行控制命令，并可进行车一地双向通信，用固定查询应答器实现列车定位和传递部 分列车运行控制命令，轨道电路检查列车完整性和轨道占用，采用固定闭塞，可 取消地面信号行车。 e r t m s e t c s 3 ：查询应答器+ g s m r 。通过g s m r 传输运行指令，查询应答 器实现列车定位，车载设备进行列车完整性检查，实现移动闭塞。 目前，e r t m s e t c s 的1 、2 级技术标准明确，在欧洲铁路建设中已有实施的 先例；但应用级别3 级，由于还未找到一个简单、易行的列车完整性检查方式， 目前还没有明确的标准以及应用计划。 采用e t c s 技术规范，同一列车能在不同装备水平的干线铁路上跨国运行，从 而大大提高了运输效率。e t c s 在欧洲的成功得到世界各国铁路的高度重视，亚洲、 北美、澳洲和非洲的一些铁路纷纷对采用e t c s 系统表示了极大的兴趣，它非常 可能成为一个全球性的列车控制标准【i 】。 1 1 2 国内列控系统现状 在2 0 0 2 年，中国铁路根据2 0 2 0 年国家经济远景发展规划和铁路跨越式发展 的要求，在分析世界铁路发展趋势的同时，结合中国铁路现状，提出研究中国列 车运行控制系统( c h i n e s et r a i nc o n t r o ls y s t e m ，简称c t c s ) 。中国列车运行控制 系统是参照e t c s 欧洲标准并结合中国国情由我国自主创新的系统。 c t c s 系统的主要功能是有效地保证行车安全，不干扰机车乘务员的正常驾 驶。c t c s 系统包括地面子系统和车载子系统，按功能和基本配置划分为5 级【4 j ： c t c s 一0 级为既有线的现状，由通用机车信号和运行监控装置构成。 c t c s 1 级由主体机车信号和安全型运行监控装置组成。1 级面向列车最高 运行速度为1 6 0 k m h 的区段。要求：地面设备在既有设备基础上强化改造，并增 加点式设备；车载设备对既有装置强化改造，实现安全升级。 c t c s 2 级基于轨道传输信息的列车运行控制系统。2 级面向提速干线和高 速新线，采用车地一体化系统设计，适用于各种限速区段。2 级地面可不设通过 信号机，机车乘务员凭车载信号行车。 c t c s 3 级基于g s m r 传输控制信息并采用轨道电路等方式检查列车占用 的列车运行控制系统。3 级面向提速干线、高速新线或特殊线路，基于g s m r 的 固定闭塞或虚拟自动闭塞，地面通过无线闭塞中，c , ( r b c ) 控制列车运行，适用于各 种限速区段。3 级地面可不设通过信号机，机车乘务员凭车载信号行车。 3 c t c s - 4 级完全基于g s m r 传输控制信息的列车运行控制系统。4 级面向高 速新线或特殊线路，基于g s m r 传输平台，可实现虚拟闭塞或移动闭塞。4 级可 取消轨道电路，由无线闭塞中心和车载验证系统结合或与其他系统共同完成列车 定位和列车完整性检查。地面可不设通过信号机，机车乘务员凭车载信号行车。 其中，c t c s 1 级和c t c s 一2 级系统是基于轨道传输信息的列车运行控制系统。 由于轨道传输的局限性，如传输单向、易受干扰、维护成本高、运行速度低等限 制，当列车速度越来越快的时候，依靠轨道进行信号传递已经变得不安全。为此， 需要使用新的通信平台来保证高速列车的安全运行。 g s m r 是由国际铁路联盟( u i c ) 支持开发的欧洲铁路专用无线通信系统， 具有适应铁路运输特点的应用优势，其标准、技术和产品在铁路上的应用已在欧 洲许多国家得到验证，达到了商业运用的程度。采用g s m r 系统，可满足铁路运 输移动话音通信和数据传输的需要，可在列控系统中连续传送列车控制命令信息， 实现车一地双向通信，充分体现通信信号一体化的鲜明特点。因此，专家和决策部 门经过充分论证和比较，决定在使用无线传输信息的c t c s 3 级系统中，选择 g s m r 作为中国铁路综合移动通信的技术体制。 c t c s 系统的目标是进一步提高列车运行的安全性，进一步强化系统设计的规 范性，与国际标准接轨，满足运输发展需求。研究符合c t c s 规范的列车运行控 制系统，特别是以无线通信技术作为列车控制信息的传输平台，基于g s m r 的 c t c s 3 级列车运行控制系统的研究，是列车运行控制系统向更高层次发展的必然 和急需。c t c s 3 级列控系统将是中国铁路各类客运专线列车控制系统理想的解决 方案。 1 2 论文研究的目的和意义 本课题是在作者参与实验室c t c s 3 级列控系统r b c 子系统设计项目后提出 的。在c t c s 3 级列控系统中，r b c 是一个基于安全计算机的系统，它依靠g s m r 及以太网等通讯平台与其他子系统联系，根据外部地面系统的基本信息和车载子 系统的信息，产生并传输给车载子系统控制命令。r b c 在实现内部功能的同时， 还需要与其他子系统协同工作，因而其控制机理相当复杂，属于对实时性、可靠 性要求高的一种控制系统。 安全和效率是铁路运输生产永恒的主题。对r b c 系统进行设计，在硬件方面， 可以使用设备冗余、故障屏蔽、故障隔离等技术，使得系统的可靠性和安全性大 大提升；但在软件设计方面，则只能靠对系统进行仔细的需求确定以及程序员的 编程能力去保证软件的安全性和可靠性，由于编程人员水平的不同，以及他们对 4 于系统理解的不同，所设计出来的软件必然存在安全隐患。所以，使用合适的理 论和工具对这一大型而又重要的系统建模，对其工作流程及性能进行分析，得到 所设计系统功能上及性能上的安全验证，从而保证软件设计的安全性和可靠性， 这一过程是十分必要的。 实时系统是一种带有时间约束的计算系统。这类系统的部分或全部事件的完 成与时间紧密相关，即需要满足一定的时间约束。对于这类软件系统而言，系统 流程的正确性和安全性显得尤为重要。使用形式化方法对实时系统进行描述和分 析是检验实时系统基本特性非常有效的手段，是保障实时系统流程正确性和安全 性的重要途径。 模型检验是形式化分析验证被测系统的一种方法。模型检验的实质是利用计 算机的快速计算能力，通过穷举被检验系统的状态空间中的每一个状态来验证该 系统满足特定的形式规约。相对于传统的形式化证明方法而言，模型检验方法具 有快速，全自动，以及对使用人员的数学背景要求不高的特剧引。 实时系统模型检验的研究以及工具的开发是当今形式化方法研究的热点之 一。世界各地的研究人员己经开发出了多个不同的实时系统模型检验工具，其中 比较著名的有u p p a a l 。 u p p a a l 是由丹麦的a a l b o r g 大学和瑞典的u p p s a l a 大学于1 9 9 5 年联合开发 的对实时系统建模、确认和验证的工具，其理论基础是基于扩展的时间自动机理 论，适用于可以被描述为非确定的并行过程的积的系统。它具有高效、快速、使 用方便的特点，己成功地用于实时控制器和通信协议等实时系统的建模和正确性 的自动验证。 使用u p p a a l 对r b c 系统进行建模，主要对r b c 与车载之间的信息交互流 程进行描述，分析r b c 系统流程的一些特性，如活性、可达性等，为r b c 系统 的设计提供一种规范的，正确的软件设计方法，进而保证r b c 系统控车的安全性 和可靠性。这就是本课题的研究目的和意义。 1 3 论文章节安排 本文的篇章结构安排如下： 第一章引言。介绍国内外列控系统发展现状，结合r b c 系统的特点，提出使用 u p p a a l - i - 具分析r b c 系统的目的和意义。 第二章u p p a a l 介绍。介绍形式化方法，介绍使用形式化方法分析软件系统的优 点，给出时间自动机的形式化定义，并对基于时间自动机理论的建模工具 u p p a a l 进行详细介绍。 5 第三章r b c 系统控车流程设计分析。介绍c t c s 3 级列控系统及其r b c 子系统， 介绍r b c 子系统与其他子系统之间的逻辑接口，详细分析r b c 系统为实 现对列车的安全控制而设计的几个主要流程，提出系统需求。 第四章基于时间自动机的r b c 控车流程建模。基于时间自动机理论，对r b c 系 统的主要控车流程进行建模，对列车和相关的地面系统进行建模，得到整 个系统的时间自动机模型。 第五章基于u p p a a l 的r b c 控车流程验证分析。使用u p p a a l 对r b c 控车流 程的时间自动机模型进行仿真，模拟控制列车运行过程，分析r b c 控制 列车运行过程中的状态变化，使用u p p a a l 的验证器验证系统的各项约 束条件，得到系统需求验证。 第六章结论与展望。对本文进行总结，展望未来工作。 6 2 分析工具u p p a a l 介绍 2 1 形式化方法 2 1 1 形式化方法概述 e n c y c l o p e d i ao f s o t h a r ee n g i n e e r i n g ) ) 对形式化方法的定义【6 j 为：“用于开 发计算机系统的形式化方法是基于数学的用于描述系统性质的技术。这样的形式 化方法提供了一个框架，人们可以在该框架中以系统的方式刻画、开发和验证系 统 。也就是说，在软件开发的全过程中，凡是采用严格的数学语言，具有精确 的数学语义的方法，都称为形式化方法。从广义上来说，形式化方法是软件开发 过程中分析、设计及实现的一种系统工程方法。狭义地，形式化方法是软件规范 描述和验证的方法【j 7 1 。所以，形式化方法以数学为基础，是一种定义了硬件系统或 软件系统的规约并对系统进行验证的语言、技术和工具。其核心在于通过具有明 确数学定义的文法和语义的方法或语言对软件的期望特性或者行为进行精确、简 洁描述，得到系统数学模型，然后通过计算的方式对模型性质进行分析和验证。 形式化描述精确地描述了用户的需求、软件系统的功能以及各种性质，其描 述的是“做什么”，而不考虑“怎么做 。它是基于严格的数学，具有严格的语 法和语义定义，从而可以准确地描述系统模型。在对系统进行严格地描述地过程 中，将会帮助用户明确其原本模糊地需求，并发现用户所陈述的需求中存在的矛 盾，从而相对完整、正确地理解用户需求。 形式化验证与形式化描述之间具有紧密的联系，形式化验证就是验证已有的 程序( 系统) p ，是否满足其形式化描述( 9 ，、l ，) 的要求( 即p ( 9 ，v ”，它也是形式化方法所 要解决的核心问题。形式化验证的主要技术包括模型检验和定理证明。模型检验 是一种基于有限状态模型并检验该模型的期望特性的技术。定理证明则采用逻辑 公式来推导系统及其性质，其中的逻辑由一个具有公理和推理规则的形式化系统 给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性 质。相对于传统的定理证明方法而言，现代模型检验方法使用计算机作为模型检 验的平台，具有快速，全自动，以及对使用人员的数学背景要求不高的特点，是 现代形式化验证的趋势。 形式化方法为计算机系统的规约、实现和验证提供了合理的数学基础。它首 先基于一定的形式语义对系统进行独立于实现的抽象描述，然后经过逐步求精、 7 变换或是逐次验证，利用规约的数学特性检验实现的一致性，直至生成最终的实 现。形式化方法中的“形式化 通常是指用来对系统进行规约说明的语言是形式 化的，即是形式语言。形式语言不是通常的自然语言，而是具有严格数学定义语 法、语义的语言。采用形式语言可以准确地刻画系统的功能、时间特性、性能等 性质，而同时形成的规约是严格的、一致的、非歧义的、完备的。对系统进行形 式规约的描述，可以对系统有一个深入的理解，同时也是对系统进行形式化分析 的过程【8 】。再辅以模型验证，就可以得到系统实现与系统需求之间的差异，从而验 证系统的需求与设计之间的一致性。 2 1 2 形式化方法分类 目前，已建立了多种适用于软件系统描述的形式化方法【7 】。从形式化描述到目 标软件系统的可实现和可执行角度，已建立的形式化方法可分为三类：操作类、 描述类和双重类。 操作类方法是基于状态和转移，通过可执行模型来描述系统，模型本身能够 采用静态分析和模型执行而得到验证，这类方法包括有限状态机、p e t r i 网、时间 自动机等； 描述类方法基于数学公理和概念，通过逻辑或代数给出系统的状态空间，具 有高度抽象的特点，便于通过自动工具进行验证。基于不同的数学基础，描述类 方法进一步分为：基于代数的描述类方法，如z 、v d m 、l a r c h 等；以命题线性时 态逻辑、一阶线性时态逻辑、计算树逻辑等时态逻辑为代表的基于逻辑的描述类 方法； 双重类方法则兼有前面二者的特点，既能够通过数学公理和概念来高度抽象 地描述系统，又具有状态和转移地可执行特征，这类方法包括扩展状态机实时时 态逻辑、t r i o + 、t r o l 等。 形式化验证分为定理证明和模型检验。定理证明系统又可以粗略地分为自动 和交互式两种类型。自动定理证明系统是通用搜索过程，在解决各种组合问题中 比较成功；交互式定理证明系统需要与用户进行交互，要求用户能提供验证中创 造性最强部分地工作，因而效率低，较难用于大系统地验证。定理证明地实施同 样需要定理证明器地支持。定理证明器包括：用户导引自动推演工具、证明检验器 和复合证明器。 模型检验离不开模型检验工具地支持。根据模型所使用的描述方法的不同， 可分为：时态逻辑模型检验工具、行为一致检验工具和复合检验工具。时态逻辑模 型检验工具有e m c 、c e s a r 、s m v 、m u r p h i 、s p i n 、u v 、s v e 、h y t e e h 、k r o n o s 、 u p p a a l 等；行为一致检验工具有f d r 、c o s p a n f o r m a l c h e e k 等；复合检验工具 有h s i s 、v i s 、s t e p 、m e t a f r a m e 等。 在形式化方法的分类中，各种方法之间的区别有时并不是那么明确。有些方 法是在原有理论基础上综合了别的方法的优点而形成的，有些模型检验工具则是 基于某几种形式化描述方法的特点而形成的。 2 1 3 形式化方法优点 在软件开发过程中，由于软件设计人员对于系统规约说明中的需求描述存在 不同理解，致使软件功能实现与需求之间可能存在不一致、不完整的方面。使用 形式化方法对系统进行分析可以发现和纠正这些问题。具体来说，使用形式化开 发软件系统的主要优点【s 】有： ( 1 ) 形式化描述以逻辑精确性为特色，除去了在非形式化说明中不可避免的大 部分含糊不清的描述，这种精确性为开发人员与用户对需求的一致性理解，及需 求的正确执行提供了更大的可能性。 ( 2 ) 形式化验证通过对需求分析中所描述的系统行为提供逻辑的精确论证，除 去了需求分析中的模糊性和主观性。 ( 3 ) 通过形式化描述和验证实现了系统的重复分析、一致性分析以及一个较 少依赖特定分析者技术和毅力的分析过程。 ( 4 ) 形式化描述和验证可以通过“裁剪”以适合于给定的项目及技术要求，也 就是说能被调整以满足具体项目的需要。 ( 5 ) 形式化描述和验证能够应用于任何开发阶段，包括目前最需要分析方法的 开发早期，越早发现和确定错误比晚一些发现付出的代价要小的多。 ( 6 ) 形式化描述和验证是基于计算机的工具所支持，这使得一致性检查和证明 等实现了自动化，提高了系统的可靠性，减少了在分析方面的费用。同时，这些工 具容许证明能够被重复执行而大大增强了分析的重复性。 ( 7 ) 形式化描述和验证弥补了现有的测试方法，通过提供一个精确的形式化描 述而得以获取一个好的测试计划。 2 2 时间自动机 2 2 1自动机概述 自动机理论( a u t o m a t at h e o r y ) 创立于1 9 3 6 年【9 】是在开关网络理论和数理 9 逻辑中图灵机理论的基础上形成和发展起来的。自动机理论主要研究离散数字系 统的功能、结构及其关系。由于自动机可以描述现实世界中各种离散数字系统的 共同特征，因此自动机的研究在经济、神经、生物、通讯、智能和检测等各个领 域都得到了广泛的应用。同时，由于自动机自然地包含状态和事件等描述离散事 件动态系统( d i s c r e t ee v e n td y n a m i cs y s t e m ，d e d s ) 的基本要素，所以理所当然 地成为d e d s 中的被控对象、监控器和整个闭环系统的重要逻辑层模型之一。自 动机理论的研究领域主要包括：有限状态自动机理论、无限状态自动机理论、概 率自动机理论、复自动机理论( 如细胞自动机和图自动机等) 以及抽象自动机理 论【1 0 】等。 现实世界中存在着这样一些系统，这些系统的许多状态的保持或是动作的完 成是与时间相关的，即要满足一定的时间限制，如某个动作要在一秒钟内完成等， 我们称这种系统为实时( r e a l t i m e ) 系统。实时系统是一种带有时间约束的计算系 统，它不仅要求所产生的结果在逻辑上是正确的，而且要求在时间上也是正确的， 核反应堆、飞行控制以及铁路控制等方面的许多计算机控制系统都属于实时系统。 为了描述和验证实时系统，传统的自动机理论显然是不够的，时间自动机作为模 拟实时系统行为的模型被引入。 2 2 2 时间自动机 r a l u r 和d i l l 在1 9 9 4 年首次提出了时间自动机理论f l 。时间自动机是在传统 有限状态自动机基础上为迁移添加时钟约束，为状态添加不变式约束而得到的。 系统包含若干个时钟，它们以相同的速率推进，每个时钟都可以被任意一个迁移 复位。它们测量的是从该时钟被启动( 复位) 以来的时间，因此时钟更像用来计 时的“秒表 。添加到迁移上的时钟约束表示只有在此约束被满足时迁移才被激 活。而添加到状态上的不变式约束表示只有在此不变式被满足时系统才能停留在 此状态1 1 2 1 。 自从有限状态自动机引入时间概念后，时间自动机就一直是一种用于描述时 间系统的标准模型，因为这种模型具有表达时间的能力。时间自动机有有限多个 控制位置、有限多个实型值时钟。两个控制位置之间可能存在转换，仅当与之相 联系的时钟约束都满足转换才有可能发生。转换发生改变了自动机的停留的控制 位置，并重置了相应的时钟【l 引。 下面给出时间自动机理论的相关定义。 1 状态转移系统f 1 4 1 【1 5 】【3 4 】 定义2 一l ：一个状态转移系统a 是一个四元组 ，其中： 1 0 s 是位置的集合； s o ( s o s ) 是初始位置的集合； a 是事件的集合或是指定信息的集合； e c _ s y x s ，是状态转移的集合。 e 中的一个状态转移s _ s 或 ，表示系统在事件a 的激励下，可以从 位置s 转移到位置s 。这样，一个状态转移系统a 从初始位置s o ( s o s o ) 开始，在 有限个状态转移s 与s 的激励下，能从位置”转移到位置s ( j s ) 。 通常，对于定义在事件集上的一个无限事件6 = 霸o ：，我们称r ： s o 山s l g q s 2 g q 是状态转换系统a 定义在事件。上的一个执行序列， 其中s 0 s o ，s 1 ，s 2 s ，v i l 。 2 时钟约束和时钟解释【1 6 】【1 7 】 定义2 2 ：时间约束 时钟约束集m ( x ) 中的一个时间约束万的定义如下： 万：- - - - - x c i x y c j6 l 6 2j t r u e ( 2 - 1 ) 其中x ，y e x ，c e z ， ，) ，x 是一个时钟变量集，z 为整数集。形 式为x y c 的约束条件称为对角线约束，为了保证时间自动机的可判定性，通常不 允许对角线约束出现。 定义2 3 ：时间解释 在一个时间变量集合x 上的时钟解释是一个映射： v ：x 寸t ( 2 2 ) 其中，t r + 。 时钟变量集x 上的一个时钟解释v 就是给每个时钟分配一个实数值。x 上所有时 钟解释的集合记为t x 。如果在时钟解释v 所提供的时钟赋值下，时钟约束万的布尔 值为真，我们就称时钟解释v 满足x 上的一个时钟约束万。 对于a r ，v + 表示一个时钟解释，它将每一个时钟x 赋值为v ( x ) + a 。对于 y c _ x ，v 【y ：= o 】表示x 的一个时钟解释，它给每个y y 的时钟重置为0 ，而其余的 时钟x 保持不变。 3 时间自动机定义f 1 8 】【1 9 1 定义2 4 ：时间自动机t a 是一个六元组 ，其中： s 为位置的集合； s o 为初始位置的集合； a 是事件的集合； x 为时钟变量的集合； i 是一个映射，用于给s 中的每个s 指定( x ) 中的一个时钟约束万； e s x a x ( 曲xt xx s ，为状态转移的集合。 其中，( 曲为时钟约束集，t ) 【为时钟解释集。e 中的一个状态转移 或s 屿s ，表示t a 在时间a 激励和时钟约束万下，从位置s 转移到位置s ，同时 相应的时钟x 将被“x ) 重置为0 。 时间自动机a 的语义由一个与它相关的转换系统s a 定义。s a 的一个状态是一 个二元组( s ，v ) ，s 是a 的一个状态，v 是x 的一个时钟解释，且v 满足s 上的时钟约束 i ( s ) 。s a 的所有状态的集合记为q a ，如果s o 是a 的一个初始位置，并且v o ( x ) ：o ， 那么状态( s o ，v o ) 是一个初始状态。在s a 中有两类转换： ( 1 ) 时间流逝：对于一个状态( s ，v ) 和一个实数值的时间增量o ，如果对于所 有的0 a a ，v + 都满足不变式i ( s ) ，那么： ( s ，v ) 兰一( s ，v + ) ( 2 3 ) ( 2 ) 位置转换：对于一个状态( s ，v ) 和一个转换 ，v 是满足时间约束万 的一个时间解释，那么： ( s ，v ) 曼哼( s ，v 【五：= 0 】) ( 2 - 4 ) 其中，名为需要重置时钟x 的集合。这样，s a 就是具有事件集a ur + 的一个转 换系统。 4 时间自动机的积【2 0 】 一个系统往往可以看成多个成员时间自动机的协调工作，为了描述多个时间 自动机间的相互作用，需要构造时间自动机的积。下面给出一个时间自动机的积 的构造方法。 定义2 5 ：设两个时间自动机为：t a l = 和 t a 2 s 2 ，s 2 0 ，a 2 ，x 2 ，1 2 ，e 2 。假设时钟集合x l 和x 2 不相交，那么t a l 和t a 2 的积 记为t a l l i t a 2 ，且： t a li i t a 2 s lxs 2 ，s i oxs 2 0 ，a lxa 2 ，x lux 2 ，i ，e ( 2 5 ) 其中i ( s 1 ，s 2 ) = i ( s 1 ) 人i ( s 2 ) 。转换e 定义如下： ( 1 ) 对于a ea lna 2 ，e l 中每个转换 和e 2 中的每个转换 ，e 有转换 。 ( 2 ) 对于a ea l a 2 ，e l 中每个转换 和e 2 中的每个位置s 2 ，e 有 转换 。 ( 3 ) 对于a ea 2 a l ，e 2 中的每个转换 和e l 中的每个位置s l ，e 有转换 。 这样，积的状态是成员状态组成的二元组，一个复合状态的不变式是成员状态 不变式的联合，转换由同一个事件进行同步转换得到。 1 2 2 2 3 可达性分析 在利用时间自动机模型对系统进行验证时，主要是安全可靠性验证，而安全 可靠性验证可归约为时间自动机的可达性分析，因此可达性的问题是时间自动机 的主要研究内容之一。 下面给出可达性的定义【1 8 】【2 0 】。 定义2 6 ：( 点的可达性) 假设s o ，s ，属于位置集合s 并且v o ，v f 是时钟的赋 值，如果状态( s ，v f ) 对于状态( s o ，v o ) 是可达的，那么一定存在一个自然数n 和 一个执行序列，从状态( s o ，w o ) 出发到达( s f ，v fo 且p ( s o ，v o ) 山( s l ，v 1 ) ( s n l ，v 。一1 ) j 且一( s n ，v n ) ，毛a ur + 。 定义2 7 ：( 时间区域) 一个时间区域为满足( x ) 中某个约束的时间值集合， 给定万( x ) ，将满足时间约束万的所有时钟值集合记为d ，称万为时间区域d 的特征约束。 定义2 8 ：( 时间区域的可达性) 假设s o ，s f 属于位置集合s 并且d o ，d f 是时 间区域，也就是点的集合。如果状态( s ，d ，) 对于状态( s o ，d 。) 是可达的，那么一定 存在自然数n 和一个执行序列从状态( s o ，d 。) 出发到达状态( 8 ，d ，) ，如下描述 ( s o ，d o ) 山( s l ，d 1 ) ( 8 n 小d 。一。) 山( s f ，d ，) ，并且在该式子中对于所有 霸a a ur + 。 时间自动机的可达性问题可以描述为是否存在一个执行序列，使系统能从一个 状态转移到另一个状态。因此，要对时间自动机进行可达性分析，就需要遍历系 统的状态空间，找到一个或某个特定的执行序列，使需要验证的特性在这个执行 序列中得到体现。 2 2 4 时间自动机优点 在参考文献【8 】中，作者对自动机与u m l 及p e t r i 网进行了比较。重要的，自动 机的优势有： 1 与半形式化建模语言u m l 相比，自动机理论弥补了u m l 在进行软件开发中 表现出来的不足。自动机理论可以消除u m l 里由于自然语言的引入而造成的语义 理解的二义性。因为自动机理论以严格的、规范化的数学理论为依据，能用严格 的数学符号和数学方法对目标软件系统的结构与行为进行有效的综合、分析和推 理，可以为系统的说明、开发和验证提供一个整体框架，更能够较早的发现目标 软件系统需求中的不一致性和不完整性。 2 与p e t r i 网这种形式化描述方法相比，自动机理论更适合描述像r b c 软件这样 1 3 的离散数字系统，因为自动机理论就是研究离散数字系统的功能、结构和两者之 间的关系的数学理论。 在自动机里引入时间的概念，使得系统状态保持或是转移都严格的遵守时间 条件的限制，这就很好的描述了实时系统行为的各种特征，如：活性、周期性、 公平性、有界响应、时间延迟和非确定性等。