On the probabilistic verification of time constrained sysML state machines

Abstract

Software and hardware design of complex systems is becoming difficult to maintain and more time and effort are spent on verification than on construction. One of the reason is the number of constraints that must be hold by the system. Recently, Formal methods such as probabilistic approaches gain a great importance in real-time systems verification including avionic systems and industrial process controllers. In this paper, we propose a probabilistic verification framework of SysML state machine diagrams extended with time and probability features. The approach consists of mapping a SysML state machine diagrams to PRISM input language. To ensure the correctness of proposed approach, we capture the semantics of both SysML state machine diagrams and their generated PRISM code. We demonstrate the approach efficiency by analyzing PCTL temporal logic on ATM case study.