 |
|
||||||||||
Model Checking of Reactive Systems
Master in Information Security
For more information about the Information Security Master Track visit: http://www.infsecmaster.ethz.ch
251-0295-00L(2V2U)
Fall Semester 2008
Stefan Leue
Course Description
Reactive Systems are software systems that undergo a continuous stimuli-response interaction with their environment. In practice, they often occur as embedded systems, such as in telecommunications or in automotive systems. The course will introduce into explicit state model checking for reactive systems, an algorithmic, automated technique for the correctness analysis of such systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics. The accompanying project will address the modeling and analysis of a VoIP protocol.
Participants are expected to possess a basic knowledge in programming, concurrent systems, automata theory and logic.
Lectures
Time: Thursday, 14h00-16h00
Place: IFW C44
Tutorials
Time: Thursday, 12h00-14h00
Place: IFW C42
Course Materials Login with your nethz account data.
Wichtiger Hinweis:
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
folgender
Seite.
Important Note:
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.
More
information
!!! Dieses Dokument stammt aus dem ETH Web-Archiv und wird nicht mehr gepflegt !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!
!!! This document is stored in the ETH Web archive and is no longer maintained !!!
