基于概率模型检测的SysML活动图验证方法

摘要

针对系统建模语言(systems modeling language,SysML)活动图模型无法进行精确的形式化分析与验证的问题,在研究现有模型检测的基础上,提出使用概率模型检测器(PRISM)对SysML活动图模型进行检测的分析验证框架,并提出一种把SysML活动图转化为相应的PRISM可执行模型的转化规则.利用该转化规则可以把SysML活动图模型转化为概率模型检测器支持的格式,实现对模型的精确分析和定量验证.实验结果表明,该规则能够有效对SysML活动图模型进行转化,为模型检测提供支持.