Zeit: Montag 04.10.04, 15.00 Uhr Ort: Mühlenpfordtstr. 23, IZ Hörsaal M 160, 1. OG Vortragender: Prof. Wojciech Penczek, (über Frau Prof. Goltz) Polish Academy of Science und Institute for Computer Science, Univ. of Warsaw

Thema: VerICS 2004: A Model Checker for Real Time and Multi-agent Systems

Zusammenfassung:

Verics is a model checking tool for verification of timed and multi-agent systems. These systems can be represented by Timed Automta, Time Petri Nets, or given as Estelle and Intermediate Language specifications. Verics offers three verification methods: Bounded Model Checking, Unbounded Model Checking, and Splitting for properties to be specified in subsets of TCTL and CTLpK. The current version of Verics uses also a new graphical user interface to design Time Petri Nets and Timed Automata. The lecture presents the verification methods of VerICS as well as a demo of its functionality.

M.Kielhorn,Ch.Schweda Inst. für Betriebssysteme und Rechnerverbund TU Braunschweig Mühlenpfordtstr. 23 38106 Braunschweig

Tel: 0531 391 3283 Fax: 0531 391 5936