论文部分内容阅读
嵌入式系统已经在航空航天、交通运输、核电能源等安全关键领域得到了广泛运用,系统故障引起的安全事故往往会造成不可挽回的灾难性后果。保证嵌入式系统的可靠性与安全性已经成为学术界和工业界共同关注的重点课题之一。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验证起落架系统是否满足性质规约,发现问题并予以改进,保证系统的可靠性与安全性。