Formal verification of internal block diagram of SysML for modeling real-time system

SysML is a graphical modeling language that is mostly used for the graphical representation of real-time systems, complex systems, safely critical systems, and embedded systems. In this paper, we present a methodology based on model checking tool for the correction and verification of SysML internal block diagram with discrete time constraint. We describe the mapping of SysML internal block diagram to PRISM input language and use Probabilistic Computational Tree Logic (PCTL) for the verification of properties. The methodology provides more reliable and quick results for the development of real time systems as PRISM supports parallel composition of components. Finally, we present the effectiveness of our approach with the help of a case study of real-time system. The discrete time factor is included in the case study to evaluate the performance characteristics of system functionality.