Master in Information Security
For more information about the Information Security Master Track visit: http://www.infsecmaster.ethz.ch
Fall Semester 2009
T. S. Hoang, M. Schmalz
At this place, we will announce important additions to the course material page.
The participants of this course learn ways of specifying, designing, and implementing computerized systems so that the outcome is correct by construction. We introduce Event-B, a language for modeling (infinite state) discrete transition systems and proving them correct. An important principle is refinement: it allows one to leave out complicated details in the beginning and to introduce them later in a step-by-step manner. Properties that have been proved in the beginning also hold, in a sense, after introducing new details.
The RODIN Platform allows one to write Event-B models, and generates proof obligations, i.e., conditions that are sufficient for correctness of the model. The platform also assists the user in proving these proof obligations.
In the lecture we will mainly discuss examples. In the tutorials we give you an introduction to the Rodin Platform, instructions for solving exercises, and then mainly assist you with the semester project: your own Rodin development.
We assume that you are interested in applying formal modeling and proofs to practical problems. It is an advantage if (but not necessary that) you have participated in the course "Formal Methods and Functional Programming".
The main objective of the course is to make you familiar with the following:
Time : Thursday (starting 17.09.2009), 10h00 - 12h00
Place : IFW B42
Time: Thursday (starting 17.09.2008), 16h00-18h00
Place: IFW A32.1
50% Project (Final Presentation during Exercise Session on 10/12/2009)
50% Exam (17/12/2009 between Lecture, duration at most 2h)
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.