On the probabilistic verification of time constrained sysML state machines

3Citations
Citations of this article
6Readers
Mendeley users who have this article in their library.
Get full text

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.

Cite

CITATION STYLE

APA

Baouya, A., Bennouar, D., Mohamed, O. A., & Ouchani, S. (2015). On the probabilistic verification of time constrained sysML state machines. In Communications in Computer and Information Science (Vol. 532, pp. 425–441). Springer Verlag. https://doi.org/10.1007/978-3-319-22689-7_33

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free