Abstract
Stochastic timed automata are an expressive formal model for hard and soft real-time systems. They support choices and delays that can be deterministic, nondeterministic or stochastic. Stochastic choices and delays can be based on arbitrary discrete and continuous distributions. In this paper, we present an analysis approach for stochastic timed automata based on abstraction and probabilistic model checking. It delivers upper/lower bounds on maximum/minimum reachability probabilities and expected cumulative reward values. Based on theory originally developed for stochastic hybrid systems, it is the first fully automated model checking technique for stochastic timed automata. Using an implementation as part of the MODEST TOOLSET and four varied examples, we show that the approach works in practice and present a detailed evaluation of its applicability, its efficiency, and current limitations.
Original language | English |
---|---|
Number of pages | 15 |
Journal | EASST electronic communications |
Volume | 70 |
DOIs | |
Publication status | Published - 2014 |
Externally published | Yes |
Event | 14th International Workshop on Automated Verification of Critical Systems, AVoCS 2014 - University of Twente, Enschede, Netherlands Duration: 24 Sept 2014 → 26 Sept 2014 Conference number: 14 |
Keywords
- Expected rewards
- Probabilistic reachability
- Stochastic timed automata