After this course the student is able to autonomously:
• apply process algebra to model simple concurrent systems
• study literature where modeling formalisms for concurrent phenomena are introduced
• solve problems about small examples of concurrent systems, using the studied formalisms
The first part of this course introduces a process calculus for the specification of concurrent systems. It is shown how bisimulation and observational equivalence provide powerful analysis tools for such specifications.|
The second part of this course studies a stochastic extension of process algebra, and timed automata and UPPAAL. These formalisms are introduced by lectures and research papers.
Each part of the course is assessed by a take-home examination, in which the formalisms have to be applied to small examples.
This course is interesting for any student interested in modeling concurrency aspects as encountered in e.g. cyber physical systems, database and information systems, or security protocols.
Prerequisites At the beginning of the course the student is expected to:
• be interested and motivated to work with mathematical formalisms
• accept the challenge to study new formalisms from research papers
• be able to deal with mathematical concepts like sets, relations, automata, and induction proofs.