Laborübung zur gleichnamigen Vorlesung. Die Übungen geben Studierenden die Möglichkeit praktische Erfahrung in den in der Vorlesung vermittelten Methoden und Tools zu sammeln.
Übungen mit Verifikationssoftware: Die Studierenden können zwischen zwei Übungsabfolgen wählen die unterschiedliche Ziele verfolgen:
1. Eine Implementierung von standard Modelchecking-Methoden in einer zur JVM kombatiblen Sprache unter Benützung einer zu Verfügung gestellten Bibliothek.
2. Benützung von standard Verifikationstools (Spin, NuSMV, TLC) zur Verifikation von verteilten Protokollen oder Algorithmen.
Anmeldung über TISS Studierende der Kennzahlen 931,938 werden bevorzugt. Bitte LVA 181.145 abonnieren; dort erscheinen die Termine.
ECTS Breakdown:----------------------------------60h Übungen15h Übungspräsentationen----------------------------------75h (3 ECTS)----------------------------------
Evaluation by your written exercises and a short presentation of the results
aktuelle Infos bitte LVA abonnieren Ort: TISS
Basic programming skills, no previous experience with verification tools is required
