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

基于CPS的实时系统的面向方面的形式化验证方法

作　者: 杨汉明
导　师: 张立臣
学　校: 广东工业大学
专　业: 计算机应用技术
关键词: Cyber-physical网络环境下的实时系统 面向方面 形式化验证方法 VDM++
分类号: TP311.52
类　型: 硕士论文
年　份: 2011年
下　载: 73次
引　用: 0次
阅　读: 论文下载
 

内容摘要


Cyber-physical网络环境下的实时系统是一个综合计算、网络和物理环境的多维复杂系统,通过3C (Computation、Communication、Control)技术的有机融合与深度协作,实现大型工程系统的实时感知、动态控制和信息服务。Cyber-physical网络环境下的实时系统实现计算、通信与物理系统的一体化设计,可使系统更加可靠、高效、实时协同,具有重要而广泛的应用前景。近年来,Cyber-physical网络环境下的实时系统不仅已成为国内外学术界和科技界研究开发的重要方向,预计也将成为企业界优先发展的产业领域。开展Cyber-physical网络环境下的实时系统研究与应用对于加快我国培育推进工业化与信息化融合具有重要意义。本文试图建立一种面向方面的实时系统形式化验证方法,这种方法对形式化验证方法的进行了面向方面的扩展。以分布式实时软件非功能特性的面向方面的形式化模型为基础,研究Cyber-physical网络环境下的实时系统非功能特性的面向方面验证理论、方法和关键技术,利用面向方面的技术解决由Cyber-physical网络环境下的实时系统非功能特性的带来的验证问题的复杂性控制,使得Cyber-physical网络环境下的实时系统非功能特性的能在自动化程度和系统规模上适应系统的需要。Cyber-physical网络环境下的实时系统非功能特性的的多种特性使得验证的复杂性呈指数爆炸,在形式验证中可以采用面向方面的技术进行有效的抽象和分解。由于CPS和待检验的性质可分别表示成一个逻辑公式,要想检验系统是否满足该性质,只需在逻辑系统中检验此二公式是否有蕴含关系；同样,要想检验系统和一个方面模块之间是否具有蕴含关系,只需验证方面模块和系统相应的逻辑公式是否具有蕴含关系。在第三章中我们将看到,一种面向方面的VDM++方法对于建立系统模型非常有效。在第四章中我们将看到一个应用的例子——空中交通管制的语音通信系统,并应用基于面向方面的VDM++对系统进行验证。本文的工作重点就是要提出Cyber-physical网络环境下实时系统的形式化验证方法,提出面向方面的非功能需求框架,主要研究将面向方面的形式化验证方法技术用于Cyber-physical网络环境下实时系统非功能性需求中的研究,主要采用面向方面的VDM++方法。并在空中交通管制的语音通信系统中得到了应用。

全文目录


摘要  4-6
ABSTRACT  6-8
目录  8-10
CONTENTS  10-12
第一章 绪论  12-16
  1.1 研究背景  12-13
  1.2 研究现状  13-14
  1.3 研究意义  14
  1.4 主要工作  14
  1.5 组织结构  14-16
第二章 研究基础  16-40
  2.1 CPS概述  16-18
    2.1.1 CPS简介  16-17
    2.1.2 CPS和其他分布式系统  17-18
  2.2 VDM++概述  18-31
    2.2.1 VDM严格的规范  19-20
    2.2.2 VDM严格的证明  20-21
    2.2.3 VDM语言  21-30
    2.2.4 VDM++  30-31
  2.3 AOP概述  31-40
    2.3.1 关注点概述  32-33
    2.3.2 非功能需求与NFR框架  33-34
    2.3.3 关注点分离  34-40
第三章 面向方面的VDM++建模  40-54
  3.1 上下文关注点的分离  40-48
    3.1.1 基于上下文和特征的建模  41-42
    3.1.2 VDM++设计  42-48
  3.2 将方面引入到VDM++中  48-52
    3.2.1 面向方面的开发  48-50
    3.2.2 编织及证明责任  50-52
  3.3 讨论和结论  52-54
第四章 面向方面的VDM++模型的形式化验证  54-70
  4.1 空中交通管制的语音通信系统  55-56
  4.2 VCS 3020S的形式化模型  56-59
    4.2.1 系统的架构  56-57
    4.2.2 该系统的功能的一个实例  57-59
  4.3 验证系统  59-64
    4.3.1 覆盖分析的目标和过程  59-60
    4.3.2 测试用例的方面化和形式化  60-63
    4.3.3 覆盖分析结果  63-64
  4.4 在形式化模型中改变需求  64-70
    4.4.1 将修改的过程方面化和形式化  64-65
    4.4.2 改变需求的一个例子  65-66
    4.4.3 新的功能方面化地集成到形式化建模中  66-68
    4.4.4 测试用例覆盖和时间分析  68
    4.4.5 结果的总结  68-70
总结与展望  70-72
参考文献  72-78
攻读学位期间发表的论文  78-82
致谢  82

相似论文

  1. 基于视点的面向方面需求工程方法研究,TP311.52
  2. 面向方面的实时系统建模及实现方法研究,TP316.2
  3. 基于面向方面机制的模型驱动架构研究,TP311.52
  4. AOP及其在房产管理系统开发中的应用研究,TP311.52
  5. AOP代码中几种特定缺陷的软件测试方法,TP311.52
  6. 基于面向方面的业务流程自动生成技术的研究与实现,TP311.52
  7. 一种面向方面的需求分离建模方法研究,TP311.52
  8. 轻量级JAVA EE框架的研究和实现,TP311.10
  9. 基于AOP的银行综合前置机系统设计与实现,TP311.52
  10. 面向方面编程实现研究及其在银行系统的应用,TP311.1
  11. 面向方面连接件的软件体系结构适应性研究,TP311.52
  12. 面向方面重构的研究,TP311.52
  13. AOP应用程序中的结构冲突问题解决框架研究,TP311.11
  14. 面向幼儿园管理的CMS系统的设计与实现,TP311.52
  15. 面向方面的C~4ISR系统需求分析方法研究,TP311.52
  16. 外籍教师管理信息系统的设计与实现,TP311.52
  17. 基于反射机制的AOP程序演化方法研究,TP311.52
  18. 基于软构件和AOP技术开发自适应ERP系统的研究,TP311.52
  19. Spring框架研究与应用,TP311.52
  20. 钻杆自动排放V型门操作机设计研究,TE928
  21. 基于CPS的实时系统的面向方面的QoS建模,TP393.09

中图分类: > 工业技术 > 自动化技术、计算机技术 > 计算技术、计算机技术 > 计算机软件 > 程序设计、软件工程 > 软件工程 > 软件开发
© 2012 www.xueweilunwen.com