Model checking timed constraint automata within Vereofy

Datum

28.02.2013

Zeit

09:30 - 10:30

Sprecher

David Müller

Sprache

en

Hauptthema

Informatik

Andere Themen

Informatik

Beschreibung

Formal verification becomes more important for software and hardware engineering. Model checking provides an algorithmic technique to examine whether a system fulfills a property which is given in terms of a temporal logic formula. One important application field of model checking is for component-based system models, where complex systems are partitioned into smaller parts called components. Vereofy is a model checker developed at TU Dresden for component-based system models in which the coordination language Reo is used for the communication and orchestration of the components. In this talk we present an extension of Vereofy to cope with real-time behaviour in component-based system models. Based on previous work we extended the input languages of Vereofy, the internal data structures for representing contraint automata with timing information, as well as the model checking algorithms for the verification of real-time properties in component-based system models with exogenous coordination.

Letztmalig verändert: 28.02.2013, 09:51:22