并发系统的建模与验证一体化方法的研究

发布时间：2017-05-13 07:12

  本文关键词：并发系统的建模与验证一体化方法的研究，由笔耕文化传播整理发布。

【摘要】：现代软硬件系统变得越来越复杂和智能化,并具有并发的特征。随着并发系统的广泛应用,尤其在关系人们生命财产安全的领域,其可靠性受到高度重视。传统的安全性保障方法主要基于测试技术,难以保证测试用例覆盖系统的所有可能执行路径。模型检测通过数学方法验证系统模型是否满足需求属性,具有完备性和自动化等优点,因而受到青睐。但是模型检测的建模过程通常由手工完成,因此对于并发系统,需要一种能够描述其行为和功能的建模语言。设计和应用针对并发系统的建模语言,其主要面临的问题有:(1)如何描述系统的控制流和数据流以及并发等特征;(2)如何减少建模的成本,提高建模的效率;(3)如何保证系统、模型、验证之间的一致性;(4)如何解决系统的白箱验证与保密性之间的冲突。针对这些问题,本文做出以下研究工作:?提出针对并发系统的形式化建模语言MCD,并给出了其语法、语义和形式化定义。MCD使用模块作为基本组件,定义层次事件自动机和功能块过程分别用于描述系统的控制流和数据流。层次事件自动机通过状态和变迁与功能块过程统一起来。各个层次事件自动机并发运行,通过共享变量和信道进行交互。基于形式化语法和语义可以对系统模型进行形式化验证和分析。?提出由MCD系统模型生成模型检测代码的算法。将层次事件自动机翻译生成线程,将功能块过程翻译生成内联函数。利用阻塞和随机选择机制实现模型的同步异步和不确定性。通过定义功能块优先级和端口变量解决数据流中带环的部分。此外还可以根据用户的需求和配置使用不同的优化策略以减小系统的状态空间和检测时间。?基于MCD建模语言设计实现了模块化建模与模型检测一体化平台M3C,该平台没有使用任何开源代码和第三方库,完全自主知识产权。M3C采用模块和图形化方式建模,自动生成模型的检测代码并进行模型检测,最后将检测结果以可视化的方式显示。还实现了语法检查,模块的自定义和复用等功能。M3C降低了形式化验证的使用门槛,同时提高了建模的正确性和效率。?使用M3C对列车通信网络中的实际系统进行了建模验证。经过验证发现系统存在缺陷,可能导致功能异常。通过和系统设计人员沟通合作,找到并修复了错误。证明了本文所提出的方法和工具的实用性。
【关键词】：并发系统 模块化建模 控制流 数据流 模型检测
【学位授予单位】：清华大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP311.52
【目录】：

• 摘要3-4
• Abstract4-7
• 第1章 绪论7-16
• 1.1 研究背景7-10
• 1.2 研究现状10-13
• 1.3 论文贡献13-15
• 1.4 论文结构15-16
• 第2章 模块化控制流与数据流建模语言16-43
• 2.1 引言16-17
• 2.2 MCD建模语言17-18
• 2.3 MCD建模语言的语法18-28
• 2.3.1 数据类型18-20
• 2.3.2 表达式20-21
• 2.3.3 层次事件自动机21-24
• 2.3.4 功能块过程24-28
• 2.3.5 MCD系统模型28
• 2.4 MCD建模语言的语义28-34
• 2.4.1 MCD系统模型28-29
• 2.4.2 层次事件自动机29-31
• 2.4.3 功能块过程31-34
• 2.5 MCD建模语言的形式化定义34-42
• 2.5.1 层次事件自动机34-38
• 2.5.2 功能块过程38-40
• 2.5.3 MCD系统模型40-41
• 2.5.4 形式化语义41-42
• 2.6 本章小结42-43
• 第3章 模型检测代码生成及优化43-63
• 3.1 引言43-44
• 3.2 PROMELA44
• 3.3 数据类型与变量44-46
• 3.4 层次事件自动机46-52
• 3.5 功能块过程52-60
• 3.5.1 功能块52-54
• 3.5.2 功能块网络54-60
• 3.6 MCD系统模型60-62
• 3.7 本章小结62-63
• 第4章 模块化建模与模型检测一体化平台63-83
• 4.1 引言63
• 4.2 整体设计63-68
• 4.3 建模工具68-75
• 4.3.1 数据类型和变量69-70
• 4.3.2 控制流和数据流70-73
• 4.3.3 布线73-75
• 4.3.4 需求属性75
• 4.4 翻译优化工具75-77
• 4.5 验证分析工具77-80
• 4.6 辅助工具80-82
• 4.7 本章小结82-83
• 第5章 应用案例83-100
• 5.1 引言83
• 5.2 MVB83-89
• 5.3 WTB89-99
• 5.4 本章小结99-100
• 第6章 结束语100-103
• 6.1 工作总结100-101
• 6.2 研究展望101-103
• 参考文献103-108
• 致谢108-110
• 个人简历、在学期间发表的学术论文与研究成果110-111

【相似文献】

中国期刊全文数据库 前10条

1 王咏刚;;并发系统的测试[J];程序员;2004年03期

2 齐微;李青山;陈平;赵芸;杜宽利;;多机并发系统动态信息的逆向抽取和过滤策略[J];系统工程与电子技术;2006年09期

3 王金双;张兴元;杨华兵;张毓森;;并发系统概率空间的形式化构造方法[J];计算机工程与科学;2008年11期

4 付立军;;医院实时多并发系统的研究[J];价值工程;2011年09期

5 冯玉琳,赵旭东,郭端阳;并发系统的模型和自动验证[J];计算机学报;1990年02期

6 刘建福,徐德启;并发系统的模型与验证[J];兰州大学学报;1992年01期

7 张广泉,戎玫,沈一栋;并发系统基本模型及其分析[J];重庆大学学报(自然科学版);1998年03期

8 刘剑,李彤;一种并发系统的规约方法[J];计算机应用研究;2000年05期

9 李杨;程建华;房鼎益;陈晓江;冯健;;并发系统的安全性与活性的验证方法[J];计算机工程与应用;2008年04期

10 鱼先锋;王辉;;并发系统互斥约束的形式化验证[J];商洛学院学报;2011年06期

中国重要会议论文全文数据库 前4条

1 燕飞;唐涛;;实时并发系统的形式化建模方法研究[A];2009系统仿真技术及其应用学术会议论文集[C];2009年

2 陈晓江;杨琛;冯健;房鼎益;;并发系统模型检测中的状态约减算法[A];2007年全国开放式分布与并行计算机学术会议论文集(下册)[C];2007年

3 蒋昌俊;疏松桂;郑应平;;随机Petri网同步并发行为的量化分析[A];1994中国控制与决策学术年会论文集[C];1994年

4 朱连章;魏晓慧;;基于着色Petri网避免并发系统死锁的方法[A];2008通信理论与技术新进展——第十三届全国青年通信学术会议论文集（上）[C];2008年

中国博士学位论文全文数据库 前4条

1 夏默;并发系统的建模与验证一体化方法的研究[D];清华大学;2015年

2 蒋昌俊;并发系统综合的PN行为理论及其应用[D];中国科学院研究生院（计算技术研究所）;1998年

3 吴鹏;并发系统的模型检测与测试[D];中国科学院研究生院（软件研究所）;2005年

4 郑光;并发系统的动作细化理论[D];兰州大学;2008年

中国硕士学位论文全文数据库 前6条

1 王婷;基于偏序简化的并发系统模型检测技术的研究[D];西北大学;2007年

2 贺彦琨;并发系统的事件结构模型初步研究[D];兰州大学;2008年

3 杨琛;基于进程代数并发系统的建模与验证研究[D];西北大学;2006年

4 宋琳;概率进程演算的互模拟分析[D];上海交通大学;2007年

5 申慧;并发系统的并行计算及性能分析[D];浙江理工大学;2011年

6 宋磊;概率符号Pi演算的有限公理化[D];上海交通大学;2009年

  本文关键词：并发系统的建模与验证一体化方法的研究，，由笔耕文化传播整理发布。

本文编号：361878