Motivation
Stellen Sie sich vor, Sie sind Hollywoodschauspieler – oder wollen einer werden (wer will das nicht?) – und möchten eine der beiden Weltenretterrollen in dem 1995 erschienen Film "Stirb langsam: Jetzt erst recht" übernehmen. In dem Film haben Sie es mit einem Terroristen zutun, der fiese Rätsel stellt, welche in kurzer Zeit gelöst werden müssen, anderenfalls explodiert eine Bombe. Um Ihre Eignung zu überprüfen hat der anspruchsvolle Drehbuchautor die Lösung der Rätsel nicht in das Drehbuch geschrieben, sondern überlässt dies den auf ein Engagement hoffenden Schauspielern. Während im Film nur einige Sekunden Zeit sind, haben Sie als Schauspieler natürlich wesentlich mehr Ressourcen zur Verfügung, jedoch auch weniger Superkräfte. Jedenfalls hat man Sie auf der Schauspielschule nicht ausreichend auf diese Rolle vorbereitet. Aber, Ihnen kann geholfen werden. Nach dem Besuch dieses Kurses haben Sie keinerlei Schwierigkeiten auch ohne größere logische Begabung vertrackte Sachverhalte korrekt zu modellieren. Die Lösung spuckt Ihnen eines der beliebten Tools aus, die wir im Rahmen des Kurses kennenlernen werden.
Zielgruppe
Neben Hollywoodschauspielern richtet sich der Kurs an Studierende in den Bachelor- und Masterstudiengängen Informatik und Elektrotechnik. Denn auch in diesen Fächern haben wir es immer wieder mit komplizierten Zusammenhängen und logischen Vertraktheiten zutun, die vollständig zu Überblicken die Kapazitäten eines oder auch mehrerer Gehirne übersteigt. Digitale System werden immer komplexer. Nicht nur ihr schierer Umfang wächst, sondern auch die Anzahl der nebenläufig oder parallel abzuarbeitenden Aufgaben und deren nicht-triviales Zusammenspiel. Uns kann geholfen werden.
Gegenstand
Wie jeder Ingenieur muss auch der Software- oder Elektroingenieur vor der Umsetzung einen Plan der umzusetzenden Lösung erstellen, einen Bauplan. Dieser kann beispielsweise eine schnell hingeworfene Skizze, ein Pseudocode oder das Skelett einer zu implementierenden Anwendung sein. Genauso wie ein Bauingenieur für die Errichtung einer Gartenlaube keine aufwendigen Pläne erstellen wird, für die Errichtung einer Brücke oder eines Hochhauses dies jedoch für unumgänglich ansehen muss, so ist auch ein Software- oder Elektroingenieur vor der Umsetzung komplexer Lösungen gut beraten einen ausführlichen Plan zu erstellen.
Sinn eines Bauplanes ist zum einen die Anleitung des Baus. Zum anderen soll anhand des Plans noch vor der Umsetzung sichergestellt werden, dass die beabsichtigte Lösung die geforderten Eigenschaften aufweist. Beim Hochbau muss beispielsweise die Statik überprüft werden. Der Brückenbauingenieur, der die Statik seiner Brücke erstmals nach der Fertigstellung "testet", wird nicht ein zweites mal engagiert werden.
Bei digitalen Systemen gibt es vielfältige Eigenschaften, die sichergestellt sein wollen: Beispielsweise, dass inkonsistente Zustände nicht erreicht werden können, dass das System sich nicht in Endlosschleifen verfangen kann (Terminierung), dass bestimmte Zustände immer wieder erreicht werden, oder dass dritte nicht in das System eindringen können.
Inhalte
Wir lernen in der Lehrveranstaltung Techniken der Modellierung kennen, wir formulieren geforderte Eigenschaften formal präzise und verwenden Tools zur Überprüfung dieser Eigenschaften. Denn wie der moderne Igenieur die Statik nicht mehr manuell berechnen muss, so stehen auch uns vielfältige computerunterstütze Verfahren zur Verfügung um digitale Systeme zu prüfen.
Literatur
[1] Jackson, D. (2012). Software Abstractions: logic, language, and analysis. MIT press.
[2] Lamport, L. (2002). Specifying systems: the TLA+ language and tools for hardware and software engineers. Pearson Education.