文档介绍：实时信息物理系统的实时性分析与验证广东工业大学硕士学位论文刘辉盐笠扭廛旦垫查盐笠扭堂瞳三沟分类号:学校代号:堂皇垦錾撞论文答辩日期:ぱ妒指导教师姓名、职称:学科ㄒ或领域名称:学生所属学院:
螈蟠á驣:ā璵篖:. 珿,甊.●
摘要信息物理融合系统珻且恢中滦思际酰代表了下一代的核心信息技术,甚至被称为“第三次信息革命”,足见其受重视程度。⒅氐氖窍质凳澜绾托槟饧扑阒涓叨燃械耐ㄑ都际跹芯浚局适对时间和空認的控制研究,所以又有“人一机一物”融合系统之称。魑R恢质蔽使丶低常奔涫侵匾5目剂恳蛩兀淮问淙氡匦朐谟邢的时间内产生有效的输出。一个完整的枰5幕〖际跤腥啵杭扑憷砺酆技术,主要解决的是虚拟世界和现实空间的融合技术,减少或避免物理世界的不确定性因素在系统中产生的弊端;通信理论和技术,解决的是实现物理对象在网络中存在的表示规约,以及对测试网络通信协议的广域网测试平台;传感网技术,主要用束感知物理对象信息,并以无线传输方式传送到网络中。谑奔浜涂占渖嫌胛锢硎澜缃裘苋诤希偌由舷低车母吒丛有裕庑┒给姆⒄勾戳司薮筇粽剑蟛糠痔粽蕉技性谑奔涞奶匦苑矫妗@缂扑系统和物理世界交互时,如何将时间分离出来,如何让物理世界中的连续时间离散化;还有当处理器芯片为了性能更好,技术变得更复杂时,会导致实时性行为不准确,同时最坏执行时间的估计也会愈发困难;还有如何保证虚拟和现实世界间依赖工作同步进行等等。利用自动机理论对系统的建模和分析可以在某种程度上分析和解决一些问题,而衡量时间特性建模方法的重要标准是其通用性和规范性,影响准确性和简单行的因素是模型表达能力的大小,为使系统能被正确的建模,并确保其可靠性,形式化方法的使用和描述足必不可少。本文在信息物理融合系统基础上进行的,介绍了概念,分析了时间语义特性,研究了在卸允奔涮匦缘募虻ソ#芙崃耸奔渎呒幕±砺奂捌浞类,利用混合自动机理论对低辰薪!⒎治龊脱橹ぃ婧筇教至嗽诩扑系统和物理系统交互时的时钟同步,利用模型检测理论,运用工具对最坏执行时间的分析。然后利用自动机的新变种验证了系统是具有可判定性的。最后,利用连续世界和离散世界的联系理论,通过把离散变量转化为连续变量表示,定义局部变量和全局变量的关系,运用微分方程表示连续变量和离散变量的连接机制,而且当改变初始值的时候,描述了微分方程的变化。实例部分给出了一个
铁道路募虻ダ樱擞昧淞坷肷⒒睦砺郏允道低车男枨蠼辛诵式化描述,并且给出了说明和验证。关键词:信息物理融合系统;时间逻辑;最坏执行时间;;形式化方法广东工业大学硕士学位论丈
;,甅,,瓹’甀””,.:;,.琧.,—..,
.—琣瑃:,,琺,.瑆,.籺
精密计时的时钟实例⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.经典时钟逻辑⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.区间时序逻辑⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯一第三章基于氖奔浣!械氖奔淠P汀械姆峙淠P汀第四章时间逻辑⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯时钟逻辑基础实体⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯小结⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯中的语法⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯...
中的语义和证明规则⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯第五章混合自动机⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.建模混合系统⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.旌瞎旒!.⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.道橹ぁ第六章时钟同步⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯时钟内音同步⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯时钟夕⒁鬴健第七章最坏执行时间分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.任务交互⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..旎òò逵畔刃閘最坏情况执行时间⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯.蔡椒ā静态分析⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯...刂屏魍糃⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯...橄蠼馐汀模型检测⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯..⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯中的模型检验⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯时序异常⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯⋯....