Protocol Validation

 
Vakcode:
X_400117
Periode:
Periode 1
Credits:
6.0
Voertaal:
Engels
Faculteit:
Faculteit der Exacte Wetenschappen
Coördinator:
dr. A. Ponse
Examinator:
dr. A. Ponse
Lesmethode(n):
Hoorcollege, Practicum, Werkcollege
Niveau:
500

Doel vak

Learning to use formal techniques for specification and validation of
communication protocols.

Inhoud vak

This course is concerned with the specification and validation of
protocols, using formal methods. The course is based on a specification
language based on process algebra combined with abstract data types,
called mCRL. This language and its toolset can be used for the
specification of parallel, communicating processes with data. Model
checking is a method for expressing properties of concurrent finite-
state systems, which can be checked automatically. Interesting
properties of a specification are: "something bad will never happen"
(safety), and "something good will eventually happen" (liveness). In the
lab we will teach the use of a tool for automated verification of the
required properties of a specification.

Onderwijsvorm

4 hours per week HC
4 hours per week WC/PR (mixed)

During the practicum the mCRL tool and the CADP model checker will be
used for the validation of protocols discussed during lectures.

Toetsvorm

Written exam, together with a practical homework assignment. The overall
mark of the course is (H+2W)/3, where H is the mark for the homework
assignment, and W is the mark for the written exam.

Literatuur

Wan Fokkink, Modelling Distributed Systems, Springer 2007. An online
version of this book (2nd edition) will be available.

Aanbevolen voorkennis

Logica en Modelleren

Doelgroep

mAI, mCS, mPDCS, master of Logic

© Copyright Vrije Universiteit Amsterdam
asnDCcreatorasvVUAmsterdam asnDCdateasv2017 asnstudyguideasvmodule asnDCidentifierasv50049473 asnDCtitleasvProtocolValidation asnperiodasv110 asnperiodasv asncreditsasv6p0 asnvoertaalasvE asnfacultyasv50000044