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.

• Type: Conference
• Year: 2007
• Where: ECBS
• Authors: Yosr Jarraya, Andrei Soeanu, Mourad Debbabi, Fawzi Hassaïne
• Keywords: Activity Diagrams, Discrete-time Markov Chains, ECBS 2007, Hardware, SysML Activity Diagrams