Formal Modeling of Communicating Systems

Faculteit Science and Engineering
Jaar 2021/22
Vakcode WMCS016-05
Vaknaam Formal Modeling of Communicating Systems
Niveau(s) master
Voertaal Engels
Periode semester II a

Uitgebreide vaknaam Formal Modeling of Communicating Systems
Leerdoelen At the end of the course, the student is able to:
1. Identify the distinguishing elements of a formal model of communication based on process calculi.
2. Explain how communication is formalized in the Calculus of Communicating Systems (CCS).
3. Develop abstract specifications of message-passing systems in terms of CCS processes.
4. Demonstrate the use of behavioral equivalences for the analysis of process specifications.
Omschrijving Society heavily depends on distributed, message-passing software systems; everyday examples include the Internet and cloud computing platforms. It is then crucial to develop techniques to ensure that these software systems behave reliably.

In this course, we explore the rigorous specification of message-passing concurrent systems, as well as techniques for establishing their correctness.

The course focuses on process calculi, small specification languages centered around the notions of interaction and communication. In particular, we will introduce the Calculus of Communicating Systems (CCS), which is a simple but expressive process calculus.

To reason about CCS specifications, we will use behavioral equivalences: they allows us to guarantee that an abstract implementation meets an intended formal specification. The course also introduces the pi-calculus as a specification language for mobile communicating systems. Tool support for reasoning over process specifications will also be discussed.
Uren per week
Onderwijsvorm Hoorcollege (LC), Opdracht (ASM)
(Up to four hours (two sessions) per week (to be discussed with students, depending on the lecturer's availability))
Toetsvorm Opdracht (AST), Presentatie (P), Verslag (R)
(Homeworks (60%) and a final project (40%).)
Vaksoort master
Coördinator prof. dr. J.A. Perez Parra
Docent(en) prof. dr. H.H. Hansen ,prof. dr. J.A. Perez Parra
Verplichte literatuur
Titel Auteur ISBN Prijs
Reactive Systems: Modelling, Specification and Verification Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba
Entreevoorwaarden From the BSc Computing Science: Introduction to Logic, Discrete Structures, Program Correctness, and Languages and Machines.
Opgenomen in
Opleiding Jaar Periode Type
MSc Computing Science: Intelligent Systems and Visual Computing  (Guided choice course units) - semester II a keuze
MSc Computing Science: Science Business and Policy  (Elective course units) 1 semester II a keuze
MSc Computing Science: Software Engineering and Distributed Systems  (Compulsory course units) 1 semester II a verplicht
MSc Courses for Exchange Students: AI - Computing Science - Mathematics - semester II a