Theoretical Computer Science

Imperfect and Timed Systems

Verification often relies on idealized assumptions about systems, like 100% uptime of a network, that do not hold in practice and therefore invalidate verification results. We developed a model that captures the imperfection of systems but yet allows for hard verification results. The idea is to work with safe thresholds on the system availability.

Team:

Roland Meyer

Publications:

• What's Decidable about Availability Languages?, by Parosh Abdulla, Mohamed Faouzi Atig, Roland Meyer, and Mehdi Seyed Salehi.
  In Proceedings of FSTTCS 2015.
  PDF | DOI | BibTeX

• Kleene, Rabin, and Scott are available, by Jochen Hoenicke, Roland Meyer, and Ernst-Rüdiger Olderog.
  In Proceedings of CONCUR 2010.
  PDF | DOI | BibTeX

• Automata-theoretic verification based on counterexample specifications, by Ernst-Rüdiger Olderog and Roland Meyer.
  In Informatik als Dialog zwischen Theorie und Anwendung, 2009.
  DOI | BibTeX

• Model checking data-dependent real-time properties of the European Train Control System, by Johannes Faber and Roland Meyer.
  In Proceedings of FMCAD 2006.
  DOI | BibTeX | Slides

• Model checking duration calculus: A practical approach, by Roland Meyer, Johannes Faber, and Andrey Rybalchenko.
  In Proceedings of ICTAC 2006.
  PDF | DOI | BibTeX

• Model Checking Duration Calculus: A Practical Approach., by Roland Meyer, Johannes Faber, Jochen Hoenicke, and Andrey Rybalchenko.
  Formal Aspects of Computing, 2008.
  PDF | DOI | BibTeX

• Model-Checking von Phasen-Event-Automaten bezüglich Duration Calculus Formeln mittels Testautomaten, Master's thesis by Roland Meyer.
  Department of Computing Science, University of Oldenburg, 2005.
  PDF, in German | BibTeX

Funding:

DFG: Automatic Verification and Analysis of Complex Systems (SFB AVACS)