Deductive probabilistic verification methods for embedded and ubiquitous computing

Abstract

Many people have studied formal specification and verification methods of embedded and ubiquitous computing systems all over the world. We can specify real-time systems using timed automata, and verify them using model-checking. Especially, recently, probabilistic timed automata and their model-checking have been developed in order to express the relative likelihood of the distributed real-time systems exhibiting certain behavior. Moreover, model-checking and probabilistic timed simulation verification methods of probabilistic timed automata have been developed. In this paper, we propose probabilistic timed transition systems by generalizing probabilistic timed automata, and propose deductive verification rules of probabilistic real-time linear temporal logic over probabilistic timed transition systems. As our proposed probabilistic timed transition system is a general computational model, we have developed general verification methods. © Springer-Verlag Berlin Heidelberg 2004.