基于概率模型检测的SysML活动图验证方法研究
发布时间：2021-02-18 00:37
近些年来,随着系统设计复杂性的提高,各种系统错误在实际应用中层出不穷,其造成严重后果的事件也逐年增多。系统建模是如今众多系统设计所必不可少的一个环节,同时作为整个系统设计流程的开始,提高其模型的正确性对减少后期生成系统的各类错误至关重要。针对系统设计过程中生成的多种模型进行正确性分析与验证,可以尽早发现设计漏洞,改正设计错误,减少系统问题的出现。所谓模型设计的正确性就是指所设计出的模型是否能正确表达未来真实系统的某种功能或者某些特性,如果能客观的反应出真实系统的一些指标特性,那么这样的模型就是正确的。被设计出的模型的正确与否,与后期生成真实系统的可用性和可靠性密切相关。系统建模语言（Systems Modeling Language,SysML）作为软件工程和系统工程领域的标准建模语言,近些年被设计人员开始大量使用。SysML针对系统工程领域中系统设计与建模的特点,提供了可视化、图形化的系统建模支持,其中Sys ML活动图的应用尤为广泛。但由于其为了保持建模的易于理解和高效简单,在进行语义说明时SysML采用了和UML相似的半形式化描述方法,使用自然语言对相应语义进行描述,这就造成了其...
【文章来源】：战略支援部队信息工程大学河南省
【文章页数】：73 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
第一章 绪论
1.1 研究背景和意义
1.2 国内外研究现状
1.3 本文研究内容
1.4 论文组织结构
第二章 相关知识介绍
2.1 SysML概述
2.1.1 SysML的产生和发展
2.1.2 SysML的图形表示
2.2 模型检测技术
2.2.1 模型检测定义
2.2.2 模型检测特点
2.3 概率模型检测技术
2.3.1 离散马尔科夫链模型
2.3.2 连续马尔科夫链模型
2.3.3 概率自动机模型
2.3.4 三种模型的比较分析
2.4 本章小结
第三章 基于新活动演算的SysML活动图形式化描述
3.1 SysML活动图
3.2 SysML活动图在新活动演算中语法表示
3.3 SysML活动图的语义表示
3.3.1 动作节点
3.3.2 行为调用
3.3.3 并发节点
3.3.4 决策节点
3.3.5 合并节点
3.3.6 同步节点
3.3.7 发送和接收
3.3.8 流程结束和活动结束
3.4 应用实例
3.5 本章小结
第四章 基于概率模型检测器的SysML活动图形式化验证
4.1 PRISM定义
4.1.1 PRISM程序定义
4.1.2 PRISM语法定义
4.1.3 PRISM语义定义
4.2 SysML活动图到PRISM输入的转换
4.2.1 SysML活动图相应术语在PRISM中的表示
4.2.2 SysML活动图到PRISM代码的转化算法
4.2.3 PCTL性质规格说明
4.3 验证方法
4.5 本章小结
第五章 交互式电子技术手册的SysML活动图建模与验证
5.1 系统介绍
5.2 实验平台简介
5.3 系统SysML活动图建模
5.4 系统SysML活动图验证
5.5 本章小结
第六章 总结与展望
6.1 本文工作总结
6.2 下一步工作
致谢
参考文献
作者简历
【参考文献】：
期刊论文
[1]基于Spin的SysML活动图验证框架[J]. 胡良文,马金晶,孙博. 计算机科学与探索. 2014(07)
[2]Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. 周宇,Luciano Baresi,Matteo Rossi. Journal of Computer Science & Technology. 2013(01)
[3]基于UML的地空导弹武器系统IETM建模[J]. 王学智,邵孟国,胡邓华. 计算机测量与控制. 2011(11)
[4]基于CPN的UML2.0形式化建模[J]. 孔莹莹,蒲海涛,隋瑞升. 青岛大学学报(工程技术版). 2011(01)
[5]IETM技术发展综述及其特点分析[J]. 陆洪武,陈建国,王荣颖. 舰船电子工程. 2009(07)
[6]装备交互式电子技术手册发展综述[J]. 梁伟杰,于永利,张磊,杜晓明. 国防技术基础. 2009(05)
[7]SysML:一种新的系统建模语言[J]. 蒋彩云,王维平,李群. 系统仿真学报. 2006(06)
[8]UML活动图的时序逻辑语义[J]. 朱雪阳,唐稚松. 计算机研究与发展. 2005(09)
[9]UML顺序图的自动验证[J]. 王璐珍,董威,陈火旺. 计算机工程与应用. 2003(29)
[10]基于Z规范的统一建模语言序列图语义分析方法[J]. 李景峰,陈平. 西安电子科技大学学报. 2003(04)
硕士论文
[1]SysML行为图到Petri网的转换研究[D]. 王松锋.解放军信息工程大学 2012
本文编号：3038784
【文章来源】：战略支援部队信息工程大学河南省
【文章页数】：73 页
【学位级别】：硕士
【文章目录】：
摘要
Abstract
第一章 绪论
1.1 研究背景和意义
1.2 国内外研究现状
1.3 本文研究内容
1.4 论文组织结构
第二章 相关知识介绍
2.1 SysML概述
2.1.1 SysML的产生和发展
2.1.2 SysML的图形表示
2.2 模型检测技术
2.2.1 模型检测定义
2.2.2 模型检测特点
2.3 概率模型检测技术
2.3.1 离散马尔科夫链模型
2.3.2 连续马尔科夫链模型
2.3.3 概率自动机模型
2.3.4 三种模型的比较分析
2.4 本章小结
第三章 基于新活动演算的SysML活动图形式化描述
3.1 SysML活动图
3.2 SysML活动图在新活动演算中语法表示
3.3 SysML活动图的语义表示
3.3.1 动作节点
3.3.2 行为调用
3.3.3 并发节点
3.3.4 决策节点
3.3.5 合并节点
3.3.6 同步节点
3.3.7 发送和接收
3.3.8 流程结束和活动结束
3.4 应用实例
3.5 本章小结
第四章 基于概率模型检测器的SysML活动图形式化验证
4.1 PRISM定义
4.1.1 PRISM程序定义
4.1.2 PRISM语法定义
4.1.3 PRISM语义定义
4.2 SysML活动图到PRISM输入的转换
4.2.1 SysML活动图相应术语在PRISM中的表示
4.2.2 SysML活动图到PRISM代码的转化算法
4.2.3 PCTL性质规格说明
4.3 验证方法
4.5 本章小结
第五章 交互式电子技术手册的SysML活动图建模与验证
5.1 系统介绍
5.2 实验平台简介
5.3 系统SysML活动图建模
5.4 系统SysML活动图验证
5.5 本章小结
第六章 总结与展望
6.1 本文工作总结
6.2 下一步工作
致谢
参考文献
作者简历
【参考文献】：
期刊论文
[1]基于Spin的SysML活动图验证框架[J]. 胡良文,马金晶,孙博. 计算机科学与探索. 2014(07)
[2]Towards a Formal Semantics for UML/MARTE State Machines Based on Hierarchical Timed Automata[J]. 周宇,Luciano Baresi,Matteo Rossi. Journal of Computer Science & Technology. 2013(01)
[3]基于UML的地空导弹武器系统IETM建模[J]. 王学智,邵孟国,胡邓华. 计算机测量与控制. 2011(11)
[4]基于CPN的UML2.0形式化建模[J]. 孔莹莹,蒲海涛,隋瑞升. 青岛大学学报(工程技术版). 2011(01)
[5]IETM技术发展综述及其特点分析[J]. 陆洪武,陈建国,王荣颖. 舰船电子工程. 2009(07)
[6]装备交互式电子技术手册发展综述[J]. 梁伟杰,于永利,张磊,杜晓明. 国防技术基础. 2009(05)
[7]SysML:一种新的系统建模语言[J]. 蒋彩云,王维平,李群. 系统仿真学报. 2006(06)
[8]UML活动图的时序逻辑语义[J]. 朱雪阳,唐稚松. 计算机研究与发展. 2005(09)
[9]UML顺序图的自动验证[J]. 王璐珍,董威,陈火旺. 计算机工程与应用. 2003(29)
[10]基于Z规范的统一建模语言序列图语义分析方法[J]. 李景峰,陈平. 西安电子科技大学学报. 2003(04)
硕士论文
[1]SysML行为图到Petri网的转换研究[D]. 王松锋.解放军信息工程大学 2012
本文编号：3038784
本文链接：https://www.wllwen.com/shoufeilunwen/xixikjs/3038784.html
