Modeling and Analysis of Probabilistic Real-time Systems through Integrating Event-B and Probabilistic Model Checking

Authors

  • Hichem Debbi Department of Computer Science, University of M'sila

DOI:

https://doi.org/10.7494/csci.2022.23.4.4588

Abstract

Event-B is a formal method used in the development of safety critical systems. However, these systems may introduce uncertainty, and need also to meet real-time requirements, which make their modeling and analysis a challenging task. Existing works on extending Event-B with probability and time did not address both probability and time in a single framework. Besides, they did focus the most on extending the language itself, not on integrating the extended Event-B with verification. In this paper, we aim to represent both probability and time in the Event-B language, and we will show how such a representation can be automatically translated into Probabilistic Timed Automata (PTA) described in the language of the probabilistic model checker PRISM. This translation would allow us to analyze probabilistic, as well as time-bounded probabilistic reachability properties of probabilistic real-time systems through the Probabilistic Timed CTL (PTCTL) logic.

Downloads

Download data is not yet available.

Downloads

Published

2022-11-08

How to Cite

Debbi, H. (2022). Modeling and Analysis of Probabilistic Real-time Systems through Integrating Event-B and Probabilistic Model Checking. Computer Science, 23(4). https://doi.org/10.7494/csci.2022.23.4.4588

Issue

Section

Articles