Institute of Computer Languages
Compilers and Languages Group

Talks 2007 - Ernst-Rüdiger Olderog

The Compilers and Languages Group invites you to a talk given by

Prof. Dr. Ernst-Rüdiger Olderog

Carl v. Ossietzky Universität Oldenburg, Deutschland

on

Automatic Verification of Combined Specifications

Date: Thursday, December 13th, 2007
Time: 14:00 (c.t.)
Location: TU Wien, Elektrotechnik, EI 5 Hochenegg-Hörsaal, Gußhausstraße 25-29 (Altbau), 2. Stock

Abstract:

We discuss how properties of high-level specifications of real-time systems combining the dimensions of process behaviour, data, and time can be automatically verified, exploiting recent advances in semantics, constraint-based model checking, and decision procedures for complex data. As specification language we consider CS-OZ-DC, which integrates concepts from Communicating Sequential Processes (CSP), Object-Z (OZ), and Duration Calculus (DC). Our approach to automatic verification rests on a compositional semantics of these languages in terms of Phase-Event-Automata. These are translated into Transition Constraint Systems which serve as an input language of an abstraction refinement model checker which can handle constraints covering both real-time and infinite data. We demonstrate this with a case study concerning emergency messages in the European Train Control System (ETCS). For CSP-OZ-DC we also discuss a UML profile and tool support.

The talk is based on the project "Beyond Timed Automata" carried out in the Collaborative Research Center AVACS (Automatic Verification and Analysis of Complex Systems) of the Universities of Oldenburg, Freiburg, and Saarbrücken, funded by the German Research Council (DFG): see also www.avacs.org.

About Prof. Dr. Ernst-Rüdiger Olderog:

Ernst-Rüdiger Olderog obtained his diploma, doctoral degree, and habilitation in Computer Science from the University of Kiel in the years 1979, 1981 and 1989. During 1981-1983 he was a visiting scientist in the Programming Research Group at Oxford University. He has been visiting professor at the Universities of Saarbrücken and Amsterdam, and at ETH Zürich. Since 1989 he is a professor of Computing Science at the University of Oldenburg. His research interest is in the area of specification, design, and verification of programs, reactive and real-time systems. In 1994 he was awarded the Leibniz Prize of the DFG. During 1995-2005 he was chairman of the IFIP Working Group 2.2 on Formalization of Programming Concepts. Since 2000 he is Editor-in-Chief of the journal Acta Informatica. (http://csd.informatik.uni-oldenburg.de/)

Complang
   About Us
   Research
   Lehre
   Service
      Robotics
      Library
      Talks 2017
      Talks 2016
      Talks 2015
      Talks 2014
      Talks 2013
      Talks 2012
      Talks 2011
      Talks 2010
      Talks 2009
      Talks 2008
      Talks 2007
      Talks 2006
      Talks 2005
      Talks 2004
Sitemap
Contact
Fast Access:
Previous Talk
Next Talk
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2017-02-13 (Webmaster)