A quantitative verification framework of SysML activity diagrams under time constraints

作者：

Highlights：

• Formal verification framework for probabilistic systems is proposed.

• SysML activity diagrams is used for system modeling.

• Automatic transformation of activity diagram into PRISM language.

• The soundness of the proposed framework is proved.

摘要

•Formal verification framework for probabilistic systems is proposed.•SysML activity diagrams is used for system modeling.•Automatic transformation of activity diagram into PRISM language.•The soundness of the proposed framework is proved.

论文关键词：SysML activity diagram,Probabilistic Timed Automata,Model checking,PCTL

论文评审过程：Available online 29 May 2015, Version of Record 18 June 2015.

论文官网地址：https://doi.org/10.1016/j.eswa.2015.05.049