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

网络嵌入式系统形式化描述与验证的研究

专 业: 计算机应用技术
关键词: 网络嵌入式系统 进程代数 描述语言
分类号: TP393
形 态: 共 127 页 约 83,185 个字 约 3.979 M内容
阅 读: 全文阅读说明

内容摘要


随着信息技术的突飞猛进,嵌入式系统尤其是网络嵌入式系统得到了广泛的应用,并且随着功能的增强,其复杂度也在呈指数增长。

形式化方法具有严密的数学基础,能够准确的对系统进行建模和描述,并能够在设计初期发现潜在的错误和问题,进而在较早的时期得到及时解决,降低了重复开发的成本,因此这种方法得了广泛的应用并变得越来越需要。

但形式化方法应用面临的一个最大障碍是状态空间的爆炸问题,而且每种具体的方法都同时存在这样或那样的问题,比如没有充分考虑到网络环境下的建模问题、表达能力不强、不能定量的分析系统模型、缺乏实用的验证工具等等。

本文提出了一种适合网络嵌入式系统的进程代数方法EACSR-VP,设计了一种易于使用、表达能力强的嵌入式系统描述语言CPSL,深入研究了嵌入式系统模型的建立、描述、执行以及验证,开发了一种用于网络嵌入式系统测试与仿真的工具—PVkit。

其中,EACSR-VP是本文形式化方法的数学基础,CPSL是形式化的描述工具,同时也是PVkit的输入,PVkit则是形式化分析和验证的工具..……

全文目录


文摘
英文文摘
论文说明:图表目录、缩略语说明
第一章 绪论
1.1嵌入式系统设计的问题
1.2嵌入式系统的形式化方法
1.3形式化方法的研究现状
1.3.1形式化描述方法
1.3.2形式化验证技术
1.4形式化方法的困难和趋势
1.5本文结构
第二章 进程代数方法EACSR-VP
2.1基本概念
2.1.1资源
2.1.2优先级
2.1.3操作符
2.1.4隐藏与限制
2.1.5标记转移系统
2.1.6语义框架
2.2语法结构
2.2.1术语
2.2.2动作
2.2.3进程
2.3语义解释
2.3.1语义模型
2.3.2无优先级的操作语义
2.3.3优先级条件下的语义
2.3.4通信
2.4小结
第三章 形式化描述语言CPSL
3.1引言
3.1.1嵌入式系统描述的特征和要求
3.1.2面向对象技术
3.1.3CPSL语言的框架
3.2语法
3.2.1数据类与数据对象
3.2.2进程类
3.2.3系统的进程代数描述
3.3语义
3.3.1树的节点
3.3.2基于树的语义
3.4小结
第四章 模型的建立与描述
4.1概述
4.2并发
4.2.1并发执行与顺序执行
4.2.2异步并发与同步并发
4.2.3交叉语义
4.2.4CPSL中的并发
4.3同步
4.3.1时间同步与进程行为同步
4.3.2不确定性问题
4.3.3竞争与互斥
4.3.4空闲动作
4.4通信
4.4.1消息的组成
4.4.2消息与封装
4.4.3信道名字的设计
4.4.4消息流程图
4.4.5基本通信原语
4.4.6通信的表现形式
4.4.7实际通信信道建模
4.4.8通信信道的竞争与选择
4.4.9链路
4.4.10小结
4.5分布
4.5.1物理分面与逻辑分布
4.5.2资源的分布性
4.5.3对象的分布性
4.5.4资源与对象的关系
4.5.5分布与并发
4.5.6CPSL与分布性设计
4.6实时性
4.6.1时间属性
4.6.2时间属性的描述
4.6.3时间粒度的选择
4.7抽象层次与系统描述框架
4.8小结
第五章 模型的执行与验证
5.1动态行为模型
5.1.1相关研究
5.1.2控制的动态行为
5.1.3数据的动态行为
5.2动态树
5.2.1树和森林
5.2.2树的操作
5.2.3动态树的构造与执行
5.2.4动态树执行算法
5.2.5案例分析——动态树的执行
5.3验证
5.3.1测试
5.3.2仿真
5.4小结
第六章 验证工具与案例分析
6.1工具PVKit
6.2案例分析之一:路由器系统的测试
6.2.1路由器模型描述
6.2.2测试类的描述
6.2.3测试与分析
6.3案例分析之二:报文交换系统的仿真
6.3.1仿真模型的建立与描述
6.3.2仿真结果及分析
6.4小结
第七章 总结与展望
参考文献
附录

相似论文

  1. 基于领域知识的Deep Web接口发现研究,45页,TP393.09
  2. Deep Web数据集成系统中数据标注研究,43页,TP393.09
  3. 基于改进RBF神经网络的入侵检测研究,41页,TP393.08
  4. 一种基于网络流量特征分析的DDOS攻击检测技术,41页,TP393.08
  5. 数据网格环境中副本一致性问题的研究,56 页,TP393.02
  6. 基于蚁群算法的网格多QoS任务调度研究,61 页,TP393.09
  7. 深层网信息挖掘技术的研究在化工领域的应用,73 页,TP393.4 TP311.131
  8. 基于VRML的自然景物动画模拟研究与应用,64 页,TP393.4 TP391.41
  9. 面向蠕虫的检测技术的研究,67 页,TP393.08
  10. 中职考务管理系统的设计与实现,75页,TP391.78
  11. 基于45°旋转扫描反射镜的图像畸变校正研究,72页,TP391.44
  12. 基于图像的重光照技术,44页,TP391.9 TP317.4
  13. 药品采购决策支持系统的研究,55页,TP39 R197.32
  14. 校园网网络监测管理系统的研究,54 页,TP393.18 TP393.07
  15. 双彩色图像水印和MPEG4视频水印算法研究,48页,TP391.41
  16. 基于图像处理技术的仪表非接触测量研究,52页,TP391.41
  17. 自相似业务流下自适应RED算法研究,82 页,TP393.07
  18. 基于贝叶斯分类的垃圾邮件过滤系统研究与实现,71 页,TP393.08 TP393.098
  19. 基于逆向工程的测试脚本转换框架的研究与实现,65 页,TP391.72 TP311.52
  20. 基于Web挖掘的个性化网站制定服务的研究和应用,60页,TP393.09
中图分类: > TP393 > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机的应用 > 计算机网络

© 2012 book.hzu.edu.cn