Automatic Verification and Performance Analysis of Time-Constrained SysML Activity Diagrams

We present in this paper a new approach for the automatic verification and performance analysis of SysML activity diagrams. Since timeliness is important in the design and analysis of real-time systems, we annotate activity diagrams with time constraints. In order to apply the model checking technique, we use discrete-time Markov chains (DTMC) as a semantic interpretation of such SysML models wherein communication is restricted to synchronization. Thus, we describe a mapping procedure of SysML activity diagrams to their corresponding DTMC and use PRISM model checker for the assessment and evaluation of performance characteristics. Finally, we apply our methodology on a real-life case study meant to assess a systems engineering behavioral model of a photo-camera device