Formal Modeling of Communicating Systems

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 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. J.A. Perez Parra
Verplichte literatuur	Titel Auteur ISBN Prijs Reactive Systems: Modelling, Specification and Verification (recommended) Luca Aceto, Anna Ingólfsdóttir, Kim Guldstrand Larsen and Jiri Srba
Entreevoorwaarden	Discrete Structures, Languages and Machines, Program Correctness
Opmerkingen	This course was registered last year with course code WMCS14001
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