安全关键嵌入式系统的SysML活动图概率验证方法研究

发布时间：2020-10-20 02:37

　　 嵌入式系统已经在航空航天、交通运输、核电能源等安全关键领域得到了广泛运用,系统故障引起的安全事故往往会造成不可挽回的灾难性后果。保证嵌入式系统的可靠性与安全性已经成为学术界和工业界共同关注的重点课题之一。SysML(Systems Modeling Language)是基于UML2.0提出的系统建模语言。SysML活动图扩展了概率属性,是最适合对系统的动态行为建模的方法之一。概率模型检测是基于模型检测技术的概率验证方法,能够对系统模型的随机特征、时间特征及空间特征进行综合描述与验证。本文结合SysML活动图和概率模型检测方法,针对系统的概率事件和外部环境的不确定因素,提出一种面向安全关键嵌入式系统的SysML活动图概率验证方法,在系统开发的早期以较小代价发现并修正嵌入式系统中存在的缺陷。论文主要研究内容包括:(1)提出基于马尔可夫决策过程(Markov Decision Process,MDP)的SysML活动图概率模型构建方法。首先,给出嵌套活动图的分解算法。然后,定义描述活动图状态迁移的MDP表达式,并基于MDP表达式描述活动图的概率模型。最后,给出活动图到MDP表达式的转换算法,实现SysML活动图概率模型的自动构建。(2)提出利用概率模型检测工具PRISM验证并分析SysML活动图概率模型的方法。首先,给出MDP表达式到PRISM代码的转换规则,实现活动图概率模型到PRISM模型的转换。然后,利用概率计算树逻辑(Probabilistic computation tree logic,PCTL)描述待验证的安全性质规约。最后,将活动图概率模型与PCTL表达式导入PRISM验证并分析结果。(3)设计实现模型转换工具SAD2PRISM,并结合本文方法使用SAD2PRISM分析飞机起落架系统的实例。首先,给出模型转换工具SAD2PRISM的设计思想与实现方式。然后,利用SAD2PRISM对飞机起落架系统着陆流程的活动图概率建模。最后,利用PRISM验证起落架系统是否满足性质规约,发现问题并予以改进,保证系统的可靠性与安全性。
【学位单位】：南京航空航天大学
【学位级别】：硕士
【学位年份】：2015
【中图分类】：TP368.1
【文章目录】：
摘要
abstract
缩略词
第一章 绪论
    1.1 课题研究背景
    1.2 国内外研究现状及选题依据
        1.2.1 SYSML建模相关研究现状
        1.2.2 概率模型检测相关研究现状
        1.2.3 选题依据
    1.3 论文组织结构
第二章 面向嵌入式系统的SYSML活动图概率验证方法概述
    2.1 SYSML活动图
        2.1.1 SYSML活动图基本元素
        2.1.2 SYSML活动图的特点
    2.2 形式化建模与验证方法
        2.2.1 形式化方法概述
        2.2.2 概率模型检测方法的特点
    2.3 面向嵌入式系统的SYSML活动图概率验证总体框架
    2.4 本章小结
第三章 基于马尔可夫决策过程的SYSML活动图概率模型构建
    3.1 嵌套活动图的分解
    3.2 基于马尔可夫决策过程的活动图概率建模
        3.2.1 马尔可夫决策过程MDP
        3.2.2 活动图概率模型的定义和约束
        3.2.3 基于MDP表达式的活动图概率模型描述
    3.3 活动图概率模型的自动构建
    3.4 本章小结
第四章 SYSML活动图概率模型的安全性分析与验证
    4.1 SYSML活动图概率模型到PRISM模型的转换
        4.1.1 概率模型检测工具PRISM
        4.1.2 MDP表达式到PRISM代码的转换规则
    4.2 SYSML活动图概率模型的PRISM验证
        4.2.1 基于概率计算树逻辑表示的需求规约
        4.2.2 活动图模型的PRISM概率模型检测
    4.3 本章小结
第五章 飞机起落架系统的安全性分析与验证
    5.1 活动图模型转换工具SAD2PRISM的设计与实现
    5.2 飞机起落架系统活动图概率模型的构建
    5.3 飞机起落架系统概率模型的安全性分析与验证
    5.4 本章小结
第六章 总结与展望
    6.1 论文工作总结
    6.2 未来工作展望
参考文献
致谢
在学期间的研究成果及发表的学术论文
附录 描述飞机起落架系统模型的PRISM代码
    附录A. 初始飞机起落架系统模型的PRSIM代码
    附录B. 排除死锁后飞机起落架系统模型的PRSIM代码

【相似文献】

相关期刊论文 前10条

1 齐建业;李强;余祥;;基于形式活动图的协议一致性测试用例生成方法研究[J];安徽大学学报(自然科学版);2013年03期

2 管昌生，夏红霞，刘定飞，钟珞;一种结构程序设计与分析的工具[J];微电子学与计算机;1994年05期

3 王智群;;一种Concur任务树转化为UML2.0的方法[J];计算机工程;2009年11期

4 张正,刘建华,吴洁明,袁山龙;利用UML活动图进行业务分析[J];北方工业大学学报;2003年03期

5 周新宽;陈平;李青山;;一种UML活动图的逆向恢复方法[J];计算机工程与应用;2006年17期

6 孙自安,周伯生;UML活动图的评价和扩展[J];计算机工程与应用;2001年12期

7 杜薇,刘伟;UML的活动图及其在电子政务项目中的应用[J];计算机工程;2003年05期

8 崔萌 ,李宣东 ,郑国梁;UML实时活动图的形式化分析[J];计算机学报;2004年03期

9 朱雪阳,唐稚松;UML活动图的时序逻辑语义[J];计算机研究与发展;2005年09期

10 许永峰;陈平;;基于UML活动图的进程关系模型恢复方法[J];电子科技;2006年05期

相关硕士学位论文 前10条

1 朱羿全;安全关键嵌入式系统的SysML活动图概率验证方法研究[D];南京航空航天大学;2015年

2 王志超;面向活动图的代码自动生成技术研究[D];哈尔滨工业大学;2010年

3 丁娜;带OCL约束的活动图多态测试方法的研究[D];重庆大学;2012年

4 叶楠;基于活动图的软件回归测试用例自动生成技术研究[D];南京大学;2012年

5 何晓云;基于活动图驱动的软件需求分析方法及应用[D];电子科技大学;2008年

6 崔霞;基于UML活动图的测试场景智能化生成方法研究[D];上海师范大学;2009年

7 方晓春;基于流程挖掘的角色—活动图建模[D];复旦大学;2008年

8 邢冠男;UML活动图到PNML转换的研究与实现[D];内蒙古大学;2009年

9 苏翠翠;一种基于UML活动图生成测试用例的方法[D];南京邮电大学;2011年

10 况振宇;基于UCM的场景可视化建模研究[D];青岛大学;2014年

本文编号：2848083