Skip to main content Skip to main navigation


Quantitative Timing Analysis of UML Activity Diagrams Using Statistical Model Checking

Fan Gu; Xinqian Zhang; Mingsong Chen; Daniel Große; Rolf Drechsler
In: Design, Automation and Test in Europe (DATE). Design, Automation & Test in Europe (DATE-2016), March 14-18, Dresden, Germany, Pages 780-785, 2016.


Unified Modeling Language (UML) activity diagrams arewidely used in modeling the dynamic aspects of system designs. However,due to frequent interactions between systems and external uncertainenvironment, the current version of UML activity diagrams cannot beused to accurately capture and quantify the overall timing behaviorsof complex systems. To address this issue, this paper extends the UMLactivity diagrams to enable the stochastic modeling of user inputs andaction executions, which strongly affect the overall timing behaviors ofsystems. Based on the statistical model checker UPPAAL-SMC, this paperproposes an automated framework that can perform quantitative reason-ing under various functional and non-functional queries. Experimentalresults demonstrate the effectiveness of our proposed approach.