Quantitative timing analysis of UML activity diagrams using statistical model checking
Quantitative timing analysis of UML activity diagrams using statistical model checking
复制标题
DOI:
10.3850/9783981537079_0339
复制
发表时间:
2016-03
期刊:
影响因子:
--
通讯作者:
F. Gu;Xinqian Zhang;Mingsong Chen;Daniel Große;R. Drechsler
中科院分区:
文献类型:
--
作者:
F. Gu;Xinqian Zhang;Mingsong Chen;Daniel Große;R. Drechsler
Unified Modeling Language (UML) activity diagrams are widely used in modeling the dynamic aspects of system designs. However, due to frequent interactions between systems and external uncertain environment, the current version of UML activity diagrams cannot be used to accurately capture and quantify the overall timing behaviors of complex systems. To address this issue, this paper extends the UML activity diagrams to enable the stochastic modeling of user inputs and action executions, which strongly affect the overall timing behaviors of systems. Based on the statistical model checker UPPAAL-SMC, this paper proposes an automated framework that can perform quantitative reasoning under various functional and non-functional queries. Experimental results demonstrate the effectiveness of our proposed approach.