Quantitative Timing Analysis for Cyber-Physical Systems using Uncertainty-Aware Scenario-Based Specifications

Due to the merits of intuitive and visual modeling of design requirements, unified modeling language (UML) sequence diagrams are widely used as scenario-based specifications in the design of cyber-physical systems (CPSs). However, when more and more CPS products are deployed within an uncertain environment, existing sequence diagram analysis approaches cannot be used to accurately capture and quantify their timing behaviors at an early design stage. To address this problem, this article extends UML sequence diagrams to allow the modeling of stochastic system inputs, message processing time, and network delays, which strongly affect the system timing behaviors. We develop a statistical model checking-based framework that can automatically convert stochastic sequence diagrams into networks of priced timed automata to enable the quantitative analysis under various performance queries. The experimental results of two industrial designs in the railway field demonstrate the effectiveness of our approach.