A formal verification framework for SysML activity diagrams

作者：

Highlights：

• We propose a formal verification framework for complex systems.

• These systems are modeled as a composition of a set of SysML activity diagrams.

• The composition is formalized and automatically transformed into the probabilistic model checker “PRISM” input language.

• The soundness of the proposed framework is proved.

• The proposed framework verifies two real systems: the shopping online system, and the real time streaming protocol.

摘要

•We propose a formal verification framework for complex systems.•These systems are modeled as a composition of a set of SysML activity diagrams.•The composition is formalized and automatically transformed into the probabilistic model checker “PRISM” input language.•The soundness of the proposed framework is proved.•The proposed framework verifies two real systems: the shopping online system, and the real time streaming protocol.

论文关键词：SysML activity diagram,Probabilistic automata,Probabilistic relation,PCTL

论文评审过程：Available online 14 November 2013.

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