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:

Security Automata

Enforceable Security Policies, Fred B. Schneider,

Attack Trees

Attack Trees, B.Schneier, Dr. Dobb's Journal 1999
Foundations of Attack Trees, S. Mauw, M. Oostdijk

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,

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

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

Interface Automata

Interface Automata, L. de Alfaro, T. A. Henzinger
Interface-Based Design, L. de Alfaro, T. A. Henzinger

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

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

Timed Automata

The theory of timed automata, R. Alur, D. Dill
Timed Automata, R. Alur

μ-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