学位论文 > 优秀研究生学位论文题录展示

基于带连续变量的Statecharts的信息物理融合系统的建模与验证

作　者: 黄骏虎
导　师: 虞慧群
学　校: 华东理工大学
专　业: 计算机应用技术
关键词: 带连续变量的Statecharts 计算树时态逻辑建模验证信息物理融合系统
分类号: TP202
类　型: 硕士论文
年　份: 2013年
下　载: 24次
引　用: 0次
阅　读: 论文下载

内容摘要

随着系统复杂度的不断提高、系统对硬件的依赖程度的增加以及客户对程序的安全性、可靠性等要求的提升,传统的离散建模工具已经越来越难以满足软件工程师对于系统建模的需求。特别是对于同时拥有离散事件驱动和连续事件驱动的混合系统而言,这种矛盾更为严重。而近年来发展越来越得到广泛关注的信息物理融合系统则是混合系统的一个典型代表。它是由开放的嵌入式系统、计算机网络和控制模块组成。因此,信息物理融合系统牵涉到计算机、通讯、控制等方面,对其进行建模与验证将是一个非常困难的任务。本文提出一种能够对同时拥有离散事件驱动和连续事件驱动的系统进行建模和验证的方法,从而达到验证系统是否安全、合理的目的。本文主要工作如下：1.以原始Statecharts为基础,提出带连续变量的Statecharts,并给出其相应的Statechart项,从而解决了Statecharts无法有效地对混合系统建模的问题；2.给出将使用带连续变量的Statecharts建模的系统转换成Kripke Structure的方法,并结合计算树时态逻辑来验证此系统的相关属性；3.使用带连续变量的Statecharts对安全信息联动工程系统进行建模与验证,从而解决了此系统中存在的一些相关问题。

全文目录

摘要  5-6
Abstract  6-10
第1章引言  10-14
  1.1 研究背景  10-11
  1.2 发展现状  11
  1.3 应用项目背景  11-12
  1.4 研究工作  12
  1.5 论文结构  12-14
第2章 Statecharts介绍以及模型验证  14-26
  2.1 Statecharts定义  14-15
  2.2 Statechart项定义  15-16
  2.3 Statecharts的限制条件  16-18
    2.3.1 同步假说  16
    2.3.2 保持因果关系假说  16-17
    2.3.3 表达优先假说  17
    2.3.4 其它限制条件  17-18
  2.4 一些Statecharts的变型介绍  18-19
    2.4.1 Basic Statecharts介绍  18
    2.4.2 时间Statecharts介绍  18-19
  2.5 Kripke Structure  19-20
  2.6 时态逻辑  20-25
    2.6.1 迁移系统  20-21
    2.6.2 线性时态逻辑及其验证方法  21-22
    2.6.3 计算树时态逻辑及其验证方法  22-25
  2.7 本章小结  25-26
第3章带连续变量的Statecharts  26-38
  3.1 带连续变量的Statecharts的定义  26-27
  3.2 Statechart项定义  27-28
  3.3 带连续变量的Statecharts的操作语义与说明语义  28-32
    3.3.1 En(Conf,I, Xconf,T)函数定义  28-29
    3.3.2 操作语义  29-30
    3.3.3 说明语义  30-32
  3.4 跨边界的Statecharts的离散状态激活集的变迁  32-33
  3.5 带连续变量的Statecharts的状态变化  33-35
    3.5.1 时延变迁  34
    3.5.2 离散变迁  34-35
  3.6 建模与分析  35-36
    3.6.1 建模方法  35-36
    3.6.2 可达状态集分析  36
  3.7 本章小结  36-38
第4章带连续变量的Statecharts的验证  38-46
  4.1 现有Statecharts验证方法介绍  38-40
    4.1.1 Statemate  38
    4.1.2 Promela和SPIN  38
    4.1.3 NuSMV  38-40
  4.2 CTL验证方法  40-45
    4.2.1 将带连续变量的Statecharts转换成Kripke Structure  40-42
    4.2.2 将需要验证的性质转换成CTL公式  42
    4.2.3 使用CTL带连续变量的Statecharts进行验证  42-45
  4.3 本章小结  45-46
第5章信息物理融合系统的建模与验证  46-58
  5.1 信息物理融合系统介绍  46-49
    5.1.1 概念介绍  46-47
    5.1.2 研究现状  47-48
    5.1.3 与物联网的异同  48-49
    5.1.4 信息物理融合系统中的QoS  49
  5.2 信息物理融合系统的模型  49-51
    5.2.1 时空模型  49-50
    5.2.2 Physicalnet模型  50-51
  5.3 带连续变量的Statecharts对信息物理融合系统建模  51-52
  5.4 带连续变量的Statecharts对信息物理融合系统验证  52-56
    5.4.1 上文验证方法的不足  52
    5.4.2 Online验证  52-55
    5.4.3 Online验证与Offline验证比较  55-56
  5.5 验证结果的使用  56-57
  5.6 本章小结  57-58
第6章安全信息联动工程系统  58-65
  6.1 安全信息联动工程系统介绍  58
  6.2 安全信息联动工程系统分析  58-59
  6.3 安全信息联动工程系统建模  59-62
  6.4 安全信息联动工程系统验证  62-64
    6.4.1 Offline验证  62-64
    6.4.2 Online验证  64
  6.5 本章小结  64-65
第7章总结与展望  65-67
  7.1 工作总结  65-66
  7.2 工作展望  66-67
参考文献  67-72
致谢  72-73
攻读硕士学位期间参加的科研项目  73-74
攻读硕士学位期间发表的学术论文  74

相似论文

基于SVM的常压塔石脑油干点软测量建模研究,TE622.1
非正交面齿轮齿面建模及加工误差分析,TH132.41
混凝土高拱坝三维非线性有限元坝肩稳定分析研究,TV642.4
HID灯整流效应的研究,TM923.32
面向SMDA的服务建模方法及工具实现,TP311.52
导弹虚拟试验可视化技术研究,TP391.9
仿真系统模型验证方法和工具研究,TP391.9
复杂仿真系统VV&A工作流技术研究,TP391.9
飞行模拟中飞行管理计算机系统CDU组件设计与仿真,TP391.9
基于测量的Internet链路延迟建模,TP393.4
基于测量的Internet延迟分析与建模,TP393.4
空中目标抗干扰识别跟踪系统,TN215
多功能车辆总线控制器MVBC综合验证研究,TP273
内衣人台的雏形设计,TS941.2
蛋内注射leptin对肉鸡肝脏胆固醇代谢相关基因及microRNA表达的影响,S831
面向RIA开发模型的研究,TP311.5
虚拟手术中建模与仿真关键技术研究,TP391.41
基于模型的小麦根系可视化研究,S512.1
近红外光谱分析技术在尖椒叶片生长信息获取中的应用,S641.3
高丛蓝莓组培体系及种子萌发率的建模研究,S663.9
基于运动目标轨迹分析的智能交通监控系统,TP277