近些年来,随着系统设计复杂性的提高,各种系统错误在实际应用中层出不穷,其造成严重后果的事件也逐年增多。系统建模是如今众多系统设计所必不可少的一个环节,同时作为整个系统设计流程的开始,提高其模型的正确性对减少后期生成系统的各类错误至关重要。针对系统设计过程中生成的多种模型进行正确性分析与验证,可以尽早发现设计漏洞,改正设计错误,减少系统问题的出现。所谓模型设计的正确性就是指所设计出的模型是否能正确表达未来真实系统的某种功能或者某些特性,如果能客观的反应出真实系统的一些指标特性,那么这样的模型就是正确的。被设计出的模型的正确与否,与后期生成真实系统的可用性和可靠性密切相关。系统建模语言(Systems Modeling Language,SysML)作为软件工程和系统工程领域的标准建模语言,近些年被设计人员开始大量使用。SysML针对系统工程领域中系统设计与建模的特点,提供了可视化、图形化的系统建模支持,其中Sys ML活动图的应用尤为广泛。但由于其为了保持建模的易于理解和高效简单,在进行语义说明时SysML采用了和UML相似的半形式化描述方法,使用自然语言对相应语义进行描述,这就造成了其自身缺乏进行分析和验证的缺陷。概率模型检测作为一种具有高效、可靠和自动化等优点的形式化验证技术,在模型验证方面具有独特的优势。因此如何依托概率模型检测来验证SysML活动图设计的正确性就成为人们研究的方向。本文针对对该问题进行研究,主要完成工作及创新点如下:1、对SysML活动图的语义描述进行研究,针对SysML活动图缺乏精确语义描述的不足,提出了基于新活动演算来表示SysML活动图形式化语义的方法。首先针对SysML活动图新增加的概率元素,相应的改进活动演算,增加概率因子,在新活动演算中对SysML活动图所有图符一一给出对应的术语,定义语法和操作语义,实现对SysML活动图的形式化描述。2、研究在PRISM模型检测软件中实现SysML活动图形式化验证的方法。以模型检测器PRISM为验证工具,本文研究了一种PRISM模型的语法和语义,将新活动演算所表示的SysML活动图单个图符进行映射,给出详细的映射规则,为SysML活动图到PRISM输入语言的转换奠定基础。3、实现了一种Sys ML活动图到PRISM输入语言的转化算法。在前面定义的单个图符映射规则的基础上,通过该转化算法的应用,可以实现在PRISM检测器中的代码运行,并给出使用PCTL概率时序逻辑进行性质表达的规则,把模型相应代码和所要满足的性质作为PRISM概率模型检测软件的两个输入,实现了对SysML活动图模型设计正确与否的验证。4、在理论研究基础上,对交互式电子技术手册系统中SysML活动图模型进行验证,按照本文提出的验证方法,完成了活动图的转化和PCTL性质的描述,最终通过PRISM检测器的运行结果证明了本文方法的可行性和有效性,对SysML活动图模型验证研究提供了一种新的方法。