Event-B is a formal method that is used in the development of safety-critical systems; however, these systems may introduce uncertainty and also need to meet real-time requirements, which make the modeling and analysis of such systems a challenging task. While some works exist that try to extend Event-B with probability and over time, they fail to address both in a single framework. Besides, these works mainly addressed extending the language itself, not integrating 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 the probabilistic timed automata (PTA) that are described in the language of the PRISM probabilistic model checker. This transformation approach would allow us to analyze the probabilistic and time-bounded probabilistic reachability properties of probabilistic real-time systems through probabilistic timed CTL (PTCTL) logic.
Ta witryna wykorzystuje pliki cookies do przechowywania informacji na Twoim komputerze. Pliki cookies stosujemy w celu świadczenia usług na najwyższym poziomie, w tym w sposób dostosowany do indywidualnych potrzeb. Korzystanie z witryny bez zmiany ustawień dotyczących cookies oznacza, że będą one zamieszczane w Twoim komputerze. W każdym momencie możesz dokonać zmiany ustawień dotyczących cookies
Informacja
SZANOWNI CZYTELNICY!
UPRZEJMIE INFORMUJEMY, ŻE BIBLIOTEKA FUNKCJONUJE W NASTĘPUJĄCYCH GODZINACH:
Wypożyczalnia i Czytelnia Główna: poniedziałek – piątek od 9.00 do 19.00