Time: Wednesday 16.6.2004, 14:30
Place: Room A4-106, Fr. Bajersvej 7
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.