Gregorio Díaz Descalzo

Department of Computer Science, University of Castilla - La Mancha.

Time: Wednesday 16.6.2004, 14:30
Place: Room A4-106, Fr. Bajersvej 7

Automatic Verification on Probabilistic Real Time Systems

Nowadays the need for checking whether a system behaves correctly has increased dramatically. There is currently lots of research effort aimed at developing tools for automatic verification. Tools such as UPPAAL have shown that it is possible to deal with time behaviors in large systems like industrial plants, protocols, etc. Other tools like RAPTURE have shown that is possible to deal with probabilistic behaviors. However, no tool has been designed to deal with both, i.e., no tool makes automatic verification over Probabilistic Real Time Systems in a proper manner.

In this talk I shall describe an approach for dealing with systems that have both probabilistic and real-time behaviors. The main goal is to show the possibility of automatic translation between real time models from tools like UPPAAL and probabilistic models used in RAPTURE. Our approach allows us the use of the most effective techniques developed for both tools, such as: abstraction, refinement, state space reduction, etc.