Content

In this seminar, we will study different formal modelling techniques, involving specific sorts of automata (like timed or probabilistic automata) as well as logics. Such models can be employed in a formal approach to system correctness, both with respect to safety as well as security properties, and are typically the basis for verification techniques.

The articles to be read will all be of a theoretical nature. Prerequisite for the seminar is knowledge of finite state automata and first order predicate logic.

Organisational Issues

Language: The language of the seminar is English, i.e. you will need to give your presentation in English as well as write your report in English.

Important Dates:

  • Preliminary meeting: October 17, 2016, 5pm, O4.267
  • First version of slides: January 05, 2017
  • Your presentation: January 16-18, 2017, 3-6pm each day
  • First version of your report: February 2, 2017
  • Peer Reviews: February 9, 2017
  • Final version of your report: March 3, 2017

 Your submissions of slides, reports etc. will have to be handed in via the Koala system.

Registration:

In order to participate, you need to register via PAUL. If more than 12 students are registered, then we will roll the dice at the beginning of the preliminary meeting. You must attend the preliminary meeting! If you miss the meeting or if you are too late and have no medical attestation, we will not allow you to participate in the seminar

 

Exam registration:

Please register during the first exam registration phase (10/24/16 - 11/14/16) for an examination. Otherwise, your participation will not count and you will need to participate in another seminar.

 

Questions:

Questions regarding the seminar are answered by Oleg Travkin.

Requirements for passing the seminar

  • give a ca. 30-minute talk and prepare for a follow up discussion
  • written report (ca. 10 pages)
  • active participation in the discussion
  • adhere to the dates and appointments
  • review reports of two other participants

Before the talk, there should have been at least two meetings with your supervisor. More information on this will be given in the preliminary meeting.

Topics and helping materials

Topics:

  1. Security Automata
    • Enforceable Security Policies, Fred B. Schneider,
  2. Attack Trees
    • Attack Trees, B.Schneier, Dr. Dobb's Journal 1999
    • Foundations of Attack Trees, S. Mauw, M. Oostdijk
  3. Attack Graphs
    • Automated Generation and Analysis of Attack Graphs, O. Sheyner, J. Haines, S. Jha, R. Lippmann, and J. M. Wing
    •  Scenario Graphs and Attack Graphs. O. Sheyner, PhD thesis, Pittsburgh,
  4. Fault Trees
    • A Compositional Semantics for Dynamic Fault Trees in Terms of Interactive Markov Chains, H. Boudali, P. Crouzen, M. Stoelinga
    • Dynamic Fault Tree Analysis Using Input/Output Interactive Markov Chains, H. Boudali, P. Crouzen, M. Stoelinga
  5. I/O-Automaten
    • An Introduction to Input/Output Automata, N. A. Lynch, M. R. Tuttle
    • Hierarchical Correctness Proofs for Distributed Algorithms, N. A. Lynch, M. R. Tuttle
  6. Interface Automata
    • Interface Automata, L. de Alfaro, T. A. Henzinger
    • Interface-Based Design, L. de Alfaro, T. A. Henzinger
  7. Büchi-Automaten
    • An Automata-Theoretic Approach to Linear Temporal Logic. M. Y. Vardi
    • Principles of Model Checking (Kapitel 4.3, 4.4), J.-P. Katoen, C. Baier
  8. Markov-Ketten
    • Principles of Model Checking (Kapitel 10.1, 10.5), J.-P. Katoen, C. Baier
    • Model-Checking Algorithms for Continuous-Time Markov Chains,  C. Baier, B. Haverkort, H. Hermanns, J.-P. Katoen
  9. Timed Automata
    • The theory of timed automata, R. Alur, D. Dill
    • Timed Automata, R. Alur
  10. μ-Kalkül
    • Model Checking and the mu-Calculus, E.A.Emerson
    • A linear-time model-checking algorithm for the alternation-free modal mu-calculus, R. Cleaveland, B. Steffen
  11. Software Model Checking for People Who Love Automata
    • Software Model Checking for People Who Love Automata, M.Heizmann, J. Hoenicke, A. Podelski
  12. Monadic Second Order Logic
    • On winning strategies in Ehrenfeucht-Fraissé, S. Arora, R. Fagin

 

Other materials:

  • Slides of the preliminary meeting (can be found in Koala)
  • Latex template for the report (zip)
  • Review guide/form (txt)