文档介绍：北京交通大学
硕士学位论文
基于模型工程的安全计算机平台设计与验证
姓名:王艺燕
申请学位级别:硕士
专业:交通信息工程及控制
指导教师:马连川
20090601
件、平台软件、处理器和专门的冗余管理硬件单元组成的。论文详细描述了中文摘要元嵛Sτ帽尘埃ü圆捎糜布⑷砑哂嘟岷戏绞降目衫┱拱踩ḿ扑慊摘要:随着安全苛求系统在铁路、航空航天、工业控制等领域应用得越来越广泛,安全计算机技术的发展越来越受到人们的重视,已经形成了一个专门的学术分支。为了扩大适用范围、减少开发成本和维护成本,安全计算机的开发正朝着通用化、可升级、可扩展等方向发展。本文以基于通信的列车运行控制系统中区域控制器和数据存储单台的设计,研究了基于模型工程的系统开发方法在安全计算机平台设计中的应用。论文引入了基于形式化方法的模型工程概念,在系统开发早期和整个开发生命周期内对系统进行建模和验证,以尽早发现设计中存在的问题。架构分析和设计语言是一种支持模型工程的形式化建模语言。本文从基于的系统开发生命周期模型出发,完成了对系统中的安全计算机平台的系统需求分析、系统高层建模、平台软件建模和验证。根据对系统安全计算机平台的需求分析,设计了安全计算机平台的高层模型,并描述了该三模冗余安全计算机平台实际结构。该结构由应用软安全计算机平台的工作原理和布ピ5穆呒δ堋论文详细介绍了平台软件流程,并根据该流程设计了基于的平台软件详细模型,包括系统表决、系统模式转化和系统重构等模块。根据列车运行控制系统的安全计算机平台的需求,利用工具软件橹ち嘶贏的实时响应时间、系统安全等级和可调度性等特性,验证结果表明了系统的完备性和设计的合理性。可扩展安全计算机平台原理样机的制作和调试成功进一步证明了系统设计的正确性和可行性,也表明了以建模、验证为基础的模型工程开发方法适用于安全计算机平台的设计。本文用图幅,表个,参考文献篇。关键词:安全计算机平台;三模冗余;模型工程;;分类号:.
.甌甌,,.,【,.:甌瑆.,.
;:;狟;..籄‘】.篒..甧譴
图系统体系结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯可靠性模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯通用结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图传统安全苛求系统工程关注焦点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图安全苛求系统工程关注的新焦点⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图系统设计失配模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.在嵌入式系统中的应用⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图单一源基于模型的断言⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图基于的系统生命周期模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.组件图形记法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.元素概况⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图系统建模整体环境⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.体系结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图衫┱拱踩ḿ扑慊植憬峁埂图可扩展安全计算机平台对应模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图安全计算机平台高层模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图可扩展安全计算机实际结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图系统状态转移图⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯单元结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯实时时钟模块结构⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯实时时钟控制模块⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图骰教ㄈ砑鞒獭图单机状态转移⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图平台上电阶段容错处理方式⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图セ鞒坦收戏治觥图肭笫淙胧莸拇矸绞健图输入数据交互和表决⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图砭龃矸绞健图两机表决处理方式⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯怨收现骰拇矸绞健图晗窤P汀图谛潘惴ǎ名将军,其中淹降牧街智榭觥图签名口信算法解决三模拜占庭失效⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..图数据输入拜占庭失效模型⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图H哂嘞低持毓鼓P假设主机收⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图低呈凳毕煊κ奔浞治觥教ㄈ砑质贝砘啤图分析数据流响应时间⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图数据流响应时间结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.图安全性等级验证错误⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图图舢
图错误的代码行⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯浚簉橹ぁ图可调度性分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图可调度性分析线程信息⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图可调度性验证结果⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯。加寐省图修正后的可调度模型线程⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯图