informal • semi-formal • formal •
informal • semi-formal • formal • • simple
• complex (a) (b)
Abbildung 1: Einführung Formaler Methoden.
den (Semi-)Entscheidungsprozeduren. Das Ziel der
Ergänzung um Formale Methoden ist motiviert durch
unsere Erfahrung in zahlreichen Projekten mit
Partnern aus der Industrie von kleinen Anbietern
sicherheitskritischer Systeme (z.B.
Mit diesem Ziel ergibt sich neben der üblichen
Herausforderung, aus dem umfangreichen Angebot
der Lehrbücher eine ausgewogene Vorlesung
zusammenzustellen, die Herausforderung, Lehrmaterialien
für den Bereich Formale Methoden auszuwählen bzw.
herzustellen. Interessanterweise ist die zweite
Herausforderung keine Teilmenge der ersteren. In den
etablierten Lehrbüchern (s.o.) und dem vorhandenen
Material wird ganz überwiegend ein Ansatz verfolgt,
den wir in Abbildung 1(a) visualisieren. Wir sehen
die für z.B. die Beschreibung von Anforderungen
verfügbaren Mittel auf einer Achse, die von informal
(rein natürlichsprachlich), über semi-formal (mit
formaler konkreter Syntax, aber ohne formale abstrakte
Syntax oder Semantik) hin zu formal (mathematisch
präzise definierte Syntax und Semantik) reichen. Die
vorgenannten Lehrbücher und Materialien bewegen
sich auf dieser Achse zwischen informal und
semiformal und geben kurze Ausblicke auf Formale
Methoden, indem Beispiele auf einer intuitiven Ebene
diskutiert werden. Bei diesem Ansatz sehen wir ein
inhärentes Problem, das bereits Lehman & Buth
Für den Bereich der Formalen Methoden in der Softwaretechnik steht mit (Bjørner, 2006a,b,c) ein dreibändiges Lehrbuch zur Verfügung, das versucht, die Softwareentwicklung vollständig aus formaler Sicht zu vermitteln. Wir haben uns aus zwei Gründen dagegen entschieden, diesem Lehrbuch zu folgen. Zunächst scheint uns das Ziel des Materials von Bjørner zu sein, formale Beschreibungssprachen möglichst in vollem Umfang darzustellen, was schlicht den Rahmen unserer Veranstaltung sprengen würde und für unsere Lernziele nicht notwendig ist. Weiterhin ist das Material u.E. so weit von der (heutigen und mutmaßlich morgigen) Lebenswirklichkeit und den etablierten Lehrbüchern entfernt, daß wir annehmen müssen, daß es Studierenden unnötig schwer fallen würde, andere Lehrbücher oder Fortbildungen in der Arbeitssituation zu unserer Veranstaltung in Bezug zu setzen. Unser (zugegeben: hoher) Anspruch an unsere Veranstaltung ist, daß nach der Teilnahme an unserer Veranstaltung keines der etablierten Lehrbücher große konzeptionelle Überraschungen bereit hält, sondern nur von den Studierenden einordnebares, zusätzliches Hintergrundwissen sowie weitere Techniken liefert.
In diesem Artikel beschreiben wir die
Konstruktion unserer Vorlesung zur Einführung in die
Softwaretechnik im Grundstudium, in der die in etablierten
Lehrbüchern zur Softwaretechnik (s.o.) vorgestellten
Inhalte um Techniken zur Beschreibung von
Anforderungen und Entwurfsaspekten vollständig formal,
also mit konkreter Syntax und präziser abstrakter
Syntax und Semantik, ergänzt werden, und berichten von
Erfahrungen aus vier Sommersemestern mit der neu
gestalteten Veranstaltung. Schwerpunkt dieses
Artikels sind die Voraussetzungen der Veranstaltung
(insbesondere die Einbettung in den Studienplan),
Konsequenzen der ergänzten Inhalte für Übungen und
Klausur, sowie Organisation und didaktische
Maßnahmen (vor allem Bereich des Übungsbetriebs), mit
denen wir die Vermittlung und Erarbeitung der
neuen Inhalte unterstützen. Die neuen Inhalte als solche
werden für den Bereich Requirements Engineering
in
Der Artikel ist wie folgt strukturiert. In Abschnitt 2 beschreiben wir die Situation der Veranstaltung im Studienplan der Universität Freiburg sowie der Studierenden zu Beginn der Veranstaltung. Abschnitt 3 legt unsere Lernziele dar und beschreibt, wie wir die neuen Inhalte bzgl. Formaler Methoden durch didaktische Maßnahmen im Übungsbetrieb unterstützen. Einen Überblick über die neuen Inhalte, ihre Einbettung in die gesamte Vorlesung und unsere Erfahrungen bzgl. Lernerfolgen gibt Abschnitt 4. Wir schließen den Artikel mit einer Betrachtung von Evaluationsergebnissen und einer Zusammenfassung. 2
Die Veranstaltung ‚Softwaretechnik‘ ist eine Pflichtvorlesung im B. Sc.-Studiengang Informatik der Universität Freiburg mit einem Umfang von 3+1 SWS für Vorlesung und Übung und 6 ECTS-Punkten. Zusätzlich besuchen Studierende des nicht-konsekutiven Masterstudiengangs, der Studiengänge ‚Embedded 1Die URL für das Sommersemester 2018 ist: https://swt. informatik.uni-freiburg.de/teaching/SS2018/swtvl Systems Engineering‘ (ESE) und ‚Mikrosystemtechnik‘ sowie des bivalenten Studiengangs Informatik die Veranstaltung. In den vier Jahren der Veranstaltung haben wir zwischen 80 und 150 angemeldete Teilnehmer::innen beobachtet. Unter den Teilnehmer::innen (der Evaluation2) studierten zwischen 73 und 96 % Informatik, der zu 100 % fehlende Teil wird stark von ESE-Studierenden dominiert. Außer in 2016 strebten jeweils mehr als knapp zwei Drittel der Teilnehmer::innen einen B. Sc.-Abschluss an.
Die ‚Softwaretechnik‘ ist im 4. Semester vorgesehen, d.h. wir können einen zweiteiligen Programmierkurs und Algorithmen & Datenstrukturen, Technische und Praktische Informatik (Betriebssysteme, Netzwerke, Datenbanken) und die MathematikVorlesungen voraussetzen. Logik und die Einführung in die Theoretische Informatik sind in Freiburg im 3. Semester vorgesehen, liegen also auch zeitlich vor der ‚Softwaretechnik‘. Parallel zur ‚Softwaretechnik‘ findet für die B. Sc.-Studierenden der Informatik ein Softwarepraktikum statt (vgl. Abschnitt 3).
Entsprechend der Position der ‚Softwaretechnik‘ im Curriculum und aus der Erfahrung der Jahre vor 2015 gehen wir einerseits davon aus, daß der Großteil der Teilnehmer::innen vor unserer Veranstaltung bzgl. der meisten Themenbereiche der Softwaretechnik über wenig bis sehr wenig Erfahrung verfügt. Andererseits wissen wir aus persönlichen Gesprächen, daß es im nicht-konsekutiven M. Sc.-Programm durchaus einzelne Studierende gibt, die über mehrjährige Berufserfahrung verfügen.
Seit 2016 überprüfen wir diese Annahme durch eine Aufgabe auf dem ersten Übungsblatt, in der wir die Teilnehmer um eine Selbsteinschätzung der Vorkenntnisse in den Themenbereichen (die wir in der ersten Vorlesung jeweils grob umreißen) Projektmanagement (seit 2017), Requirements Engineering, Programmierung, Modellierung und Qualitätssicherung bitten. Wir schlagen in der Aufgabe die folgende, subjektiv zu interpretierende Skala vor (die Übungsblätter sind in Englisch verfasst): 0: I have no experience in that activity whatsoever. I have not taken any related subjects during my studies. 1: I have only performed the activity in the context of a lecture or programming course. 10: I have performed the activity in a project with a large user base (100+ users), a large work volume (36+ person-months) or a specific commercial purpose. I have been responsible for 2Zwischen 26 und 40 Angaben; leider haben wir keinen direkten Zugriff auf Studiengang oder angestrebten Abschluss. the planning and execution of the activity in a software development project within defined resource and time constraints. Tabelle 1 zeigt die bisherigen Ergebnisse, die unsere Annahmen durchweg bestätigen. Etwas überraschend finden wir, daß sich das obere Quartil der Studierenden im Bereich Programmierung regelmäßig als relativ erfahren einschätzte, sich im Bereich Qualitätssicherung (der die Aktivität des Testens einschließt, von der man erwarten sollte, daß diese mit ernsthafter Programmierung einhergeht) als eine oder zwei Stufen geringer erfahren einordnet.
In der zweiten Vorlesung zeigen und diskutieren wir die Ergebnisse des jeweiligen Jahres. Mit der Präsentation der Ergebnisse verbinden wir die folgenden Botschaften: Erstens, daß wir, d.h. die Veranstalter und die Studierenden, es (auch dieses Jahr wieder) mit einem bzgl. Vorerfahrung eher heterogenen Auditorium zu tun haben. Zweitens, daß die Vorlesung explizit für Studierende angelegt ist, die sich zwischen den Werten 0 und 1 einordnen (und daß diese Studierenden in der klaren Mehrheit sind, man also nicht „allein“ ist, wenn man sich dort eingeordnet hat). Drittens, daß für die Studierenden, die sich bei Werten von 5 und höher einordnen, möglicherweise keine Neuigkeiten vermittelt werden, daß diese Studierenden jedoch explizit eingeladen sind, in Form von Fragen oder Kommentaren ihre Vorerfahrung in den Vorlesungs- und Übungsterminen einzubringen. In der Diskussion der Ergebnisse stellen wir heraus, daß die Inhalte der Vorlesung die Studierenden darauf vorbereiten möchten, in Softwarentwicklungsprojekten höherer Stufen mitzuarbeiten, also Projekte die einen größeren Umfang und eine größere Nutzerbasis haben als jedes Projekt, das man im Studium in Freiburg erlebt, sowie üblicherweise einen wirtschaftlichen Aspekt haben. 3
Ein Lernziel unserer Veranstaltung ist zunächst, wie in der Einleitung beschrieben, eine Übersicht über die verschiedenen Themenbereiche der Softwaretechnik entsprechend der etablierten Lehrbücher zu geben. Unser Schwerpunkt ist hierbei die Vermittlung der verschiedenen Probleme, die sich daraus ergeben, daß mehrere Menschen über einen längeren Zeitraum zusammen nichttriviale Softwaresysteme entwickeln, sowie bekannte Lösungsansätze und deren Vorund Nachteile vorzustellen.
Der neue Aspekt unserer Veranstaltung ist die vollständig formale Definition von Beschreibungssprachen und Analysetechniken an den entsprechenden Stellen in der Vorlesung (vgl. Tabelle 2). Die Lernziele sind hier das sichere Verstehen und Anwenden der eingeführten Formalen Methoden, sowie die Interpretation von Analyseergebnissen. Die entsprechenden Inhalte und die Einbettung in die Vorlesung werden in Abschnitt 4 beschrieben.
Wir beschreiben die Ziele unserer Veranstaltung in der ersten Vorlesung, um Missverständnisse (und Enttäuschungen) zu vermeiden. In einer Aufgabe des ersten Übungsblattes bitten wir die Studierenden, ausgehend von der ersten Vorlesung ihre Erwartungen an die Veranstaltung in eigenen Worten zu beschreiben. In der zweiten Vorlesung stellen wir eine Auswahl der Antworten vor, und gehen jeweils darauf ein, inwiefern die Veranstaltung diese Erwartungen erfüllen kann. Ein über die Jahre wiederkehrender Punkt, ist der Wunsch, gutes Design zu lernen. Diese Erwartungen liefern einen guten Anlass, erneut auszuführen, daß ein Ziel der Vorlesung ist, fundamentale Designprobleme zu verstehen und Designentscheidungen präzise zu beschreiben und auf Aspekte guten Designs hin zu analysieren, wir jedoch keine konkreten Verfahren zur Erstellung guter Designs für spezifische Anwendungsfelder diskutieren. Wir plausibilisieren diese Zielsetzung durch eine grobe Beschreibung des weiten Spektrums von Software: von Onlineshops, über Standardanwendungen (Textverarbeitung, etc.), kommerzielle Spiele, Betriebswirtschaftliche Software, bis hin zu sicherheitskritischen, eingebetteten Systemen. Jeder dieser Bereiche hat eigene, bewährte Vorstellungen von gutem Design, die untereinander nicht austauschbar sein müssen. 3.1
Klausur
Ähnlich wie
Bei der Punkteverteilung der Klausur orientieren
wir uns grob an den Stufen der (überarbeiteten)
Taxonomie der Lernziele
Teil unserer Veranstaltung ‚Softwaretechnik‘ ist eine klassische Vorlesung im Umfang von 3 SWS. Um nicht an einem Tag der Woche auf eine Stunde Tutorium umschalten zu müssen, interpretieren wir das 3+1Format als drei Vorlesungen (à 90 Minuten) und ein Tutorium (à 90 Minuten) in zwei Wochen.
Über die vorhandene Infrastruktur zeichnen wir das gesprochene Wort und den Bildschirminhalt auf und stellen die Aufzeichnungen zeitnah zur Verfügung. Auf diese Weise konnten wir die Vorlesungen ohne Skript bestreiten, da das gesprochene Wort jederzeit zum Nachhören verfügbar ist. Weiterhin können die Teilnehmer::innen, denen unser Vortrag zu langsam oder zu ausführlich ist, die Geschwindigkeit beim Anhören der Aufzeichnung selbst bestimmen. Entsprechend der Selbsteinschätzung der Teilnehmer::innen (vgl. Abschnitt 1) sprechen wir in der Vorlesung lieber zu langsam als zu schnell und betrachten neue Inhalte ggf. aus mehreren Perspektiven, was für einige Teilnehmer::innen zu langsam sein kann. In der Evaluation geben, über die Jahre 2016 bis 2018 aggregiert,3 von 99 Rückmeldungen knapp 25 % an, sich die Inhalte hauptsächlich durch Anwesenheit anzueignen, und 18 % bzw. 33 % geben ‚teils/teils‘ bzw. ‚hauptsächlich über die Aufzeichnungen‘ an. Entsprechend haben wir eher geringe Besucherzahlen in der eigentlichen Vorlesung, dafür jedoch Besucher::innen, die die Präsenz für Fragen oder Kommentare nutzen möchten, denen wir, so gut es die Zeit erlaubt, Raum geben.
Das Lernziel, eine Übersicht entsprechend der
etablierten Lehrbücher zu geben, hat für uns zwei
Teilaspekte. Einerseits den Aspekt der Vermittlung
von Techniken und Verfahren und andererseits den
Aspekt „der Mensch steht im Mittelpunkt“
Übungsaufgaben und Tutorate Die Vorlesung wird von Übungen begleitet. Vor der ersten Vorlesung jedes 3er Blocks steht ein Übungsblatt zur Verfügung, das direkt nach dieser Vorlesung teilweise und nach der zweiten Vorlesung des Blocks vollständig bearbeitet werden kann, sodaß für jede Aufgabe mindestens eine Woche zur Bearbeitung zur Verfügung steht. Studierende bearbeiten die Aufgaben in Teams aus 2 bis 3 Personen und können ihre Bearbeitungen bis zur Minute vor Beginn des Tutoriums auf der Lernplattform einreichen.
In den Tutorien legen wir Wert auf Interaktion
(i.S.v.
Für die schriftliche Darstellung in den Einreichungen fordern wir regelmäßig die Form „Problem in eigenen Worten darstellen – eigenen Lösungsvorschlag formulieren – begründen, argumentieren, im besten Falle: beweisen, daß der Lösungsvorschlag das definierte Problem löst“ und halten die Tutor::innen dazu an, in Kommentaren zu den Einreichungen kontinuierlich diese Form nachzufragen.5 Entsprechend sind die (ausgewogen vorkommenden) offenen Modellierungsaufgaben absichtlich unpräzise formuliert. Hierbei ist unserer Erfahrung nach der angemessene Grad an Unschärfe in der Aufgabenstellung im B. Sc.-Programm signifikant geringer als im M. Sc.Programm. Diese absichtliche Unschärfe und die didaktische Absicht kommunizieren wir ganz explizit: wir gehen (stark) davon aus, daß die allerwenigsten Absolventen in ihrer beruflichen Laufbahn präzise Aufgabenstellungen bekommen werden — und unter dieser Annahme können wir ruhig im 4. Semester langsam mit Aufgaben dieser Art beginnen. Im ersten Jahr der Veranstaltung gab es in der Evaluation vereinzelt Wünsche nach ganz klaren Aufgaben. Unsere Hypothese ist, daß in den meisten vorherigen Veranstaltungen präzise Aufgabenstellungen vorherrschen (und den Lernzielen angemessen sind, vgl. auch Abschnitt 4.2) und die ‚Softwaretechnik‘ sich in diesem Aspekt für die Studierenden ungewohnt anfühlt.
Am Tag vor den Tutorien führen wir jeweils ein Tutorium für die Tutor::innen durch, vor dem die Tutor::innen das Übungsblatt selbst skizzenhaft lösen. In diesen Tutors’ Tutorials gehen wir (in der Art der Tutorien für die Studierenden) die Aufgaben durch, diskutieren weiterführende Fragen, legen die Lernziele der jeweiligen Aufgaben und Fragen dar und geben Tips zur Moderation. Der Ablauf der Tutorien steht danach inklusive Vorschlägen für weiterführende Fragen und Lernziele als eine Art „Drehbuch“ zur Verfügung. In der ersten Durchführung hatten wir leichte Sorge, daß sich die Tutor::innen in ihrer gestalterischen Freiheit beschränkt fühlen könnten. Hier waren die Rückmeldungen bisher durchweg positiv: ganz im Gegenteil würden die Tutors’ Tutorials Sicherheit (z.B. im Zeitmanagement) geben und kognitive Kapazitäten für tiefer gehende Fragen und Kommentare von Seiten der Studierenden freihalten. Weiterhin erreichen wir durch diesen Ansatz eine überwiegend gleichbleibende Qualität der Tutorien, unabhängig von dem/der konkreten Tutor::in.
5Nicht zuletzt im Interesse der Studierenden: Wir gehen davon aus, daß gut präsentierte Lösungsvorschläge bei der Klausurvorbereitung zumindest nicht hinderlich sind.
In der auf das Tutorium folgenden Woche geben die Tutor::innen individuelle (für die Klausurzulassung relevante) Bewertungen und Kommentare zu den Einreichungen. Hierbei werden die Einreichungen auf zwei verschiedenen Skalen bewertet. Die für die Klausurzulassung relevante good-will-Skala bewertet „sinnvolle Bearbeitung“ relativ zum Wissen der Studierenden vor dem Tutorium. Hier interpretieren die Tutor::innen unklare Formulierungen im Zweifel zugunsten der Studierenden. Um einen Eindruck von der Bewertung in der Klausur zu geben, bewerten wir außerdem jede Aufgabe auf der evil-Skala, die sich am Punkteschema der Klausur und am Wissen nach dem Tutorium orientiert, insbesondere darüber, wie bestimmte Aufgabenstellungen im Kontext der Veranstaltung im Zweifel zu interpretieren sind. Hier werden unklare Formulierungen oder Fehler in der Syntax zuungunsten der Studierenden gewertet. 4
Für die Darstellung von Vokabular, Problembereichen
und nicht formalen Inhalten folgt unsere Vorlesung
im Wesentlichen dem Lehrbuch
Im folgenden beschreiben wir unsere Erweiterung
der Inhalte um formale Modelle in der
Softwareentwicklung, die sich unserer Wahrnehmung nach
nahtlos an die Diskussion der Begriffe der Modellierung
und die Bedeutung von Modellen in der
Softwareentwicklung bereits im ersten Kapitel von
Tabelle 2 gibt einen Überblick über die Inhalte der Vorlesung. Wir beginnen mit dem Themenbereich Projektmanagement, da die Inhalte dieses Bereichs für die Teilnehmer::innen des parallel im 4. Semester stattfindenden Software-Praktikums (SoPra) für B. Sc.-Studierende nützlich sein können. Es gibt von Seiten der Teilnehmer::innen durchaus den Wunsch nach einer Abstimmung zwischen dem SoPra und der ‚Softwaretechnik‘, der aus verschiedenen Gründen nicht praktikabel (und, da das SoPra eine in sich abgeschlossene Veranstaltung mit eigenen Vorlesungen ist, auch nicht notwendig) ist. Ein Grund ist, daß im SoPra bereits in der dritten Woche die Spezifikation und ein Architekturentwurf abzugeben sind. Ein weiterer Grund ist, daß in jedem Jahr über 30 % der ‚Softwaretechnik‘-Teilnehmer::innen das SoPra nicht in ihrem Studienplan haben und Versuche einer engeren Abstimmung bei diesen Teilnehmer::innen zu signifikanten Verwirrungen geführt haben. Als Kompromiss haben einige Übungsaufgaben einen Bezug zum SoPra, der sich den SoPra-Teilnehmer::innen erschließt, und für die anderen Studierenden einfach „ein Beispielprojekt“ ist.
In der Präsentation und Diskussion der
nichtformalen Inhalte folgen wir
Aufgrund unserer in der Einleitung ausgeführten Beobachtung eines Mangels an geeigneten Lehrbüchern, haben wir die formalen Inhalte selbst ausgewählt bzw. konstruiert. Der Überarbeitung der Veranstaltung lag die Hypothese zugrunde, daß es durch eine angemessene Reduktion des Sprachumfangs möglich ist z.B. die formale Spezifikationssprache für Strukturaspekte OCL vollständig definiert einzuführen und die Idee Formaler Methoden und Analysen zu vermitteln, und gleichzeitig der Vermittlung der etablierten nicht-formalen Inhalte einen angemessenen Raum zu geben. Bei der Auswahl der Teilsprachen von z.B. OCL stand das Ziel im Vordergrund, die formalen Sprachen nicht artifiziell zu vereinfachen, sondern echte Teilsprachen auszuwählen, die in Spezialvorlesungen konservativ erweitert werden. Wir konnten hierbei auf eine langjährige Erfahrung aus Forschungs- und Projektarbeit sowie aus unseren Spezialvorlesungen ‚Software, Design, Modelling, and Analysis in UML‘ (UML) und ‚Real-Time Systems‘ im M. Sc. Informatik zurückgreifen, in denen für die Modellierungssprachen jeweils eine vollständige konkrete und abstrakte Syntax sowie eine formale Semantik eingeführt wird. In der UML-Vorlesung sind dies Klassen- und Objektdiagramme, OCL, StateMachines und Sequenzdiagramme.
Bei der Auswahl der Beispiele in der Vorlesung und der Konstruktion der Übungsaufgaben greifen wir soweit möglich auf reale, industrielle Softwareprojekte (bestenfalls aus unserer eigenen Erfahrung) zurück, da so sichergestellt ist, daß wir Nachfragen in beliebiger Detailtiefe zufriedenstellend beantworten können.6 Dabei verwendet die Vorlesung für die verschiedenen Formalen Methoden verschiedene Beispiele an denen sich die spezifischen Stärken zeigen. Wir möchten (und können redlicherweise) nicht den Eindruck erwecken, daß der Stand der Technik der Formalen Methoden ist, ein Softwaresystem vollständig und durchgängig konsistent formal zu beschreiben. Formale Methoden sind dann effektiv, wenn geeignete Formalismen zur Beschreibung und Analyse spezifischer, besonders kritischer oder komplexer Aspekte von Software mit Bedacht eingesetzt werden.
6Dies ist bei artifiziell konstruierten Beispielen ungleich schwerer herzustellen und kann, wenn es nicht gelingt, unnötige Unzufriedenheit auf Seiten der Studierenden hervorrufen.
Wir nutzen bei der Auswahl der Inhalte die relative späte Lage der Veranstaltung im Studienplan aus (vgl. Abschnitt 2). So bauen wir auf ‚Grundlagen der Theoretischen Informatik‘, die MathematikVorlesungen und ‚Rechnerarchitektur‘ auf, in denen die Studierenden bereits mit verschiedenen Formalen Methoden konfrontiert wurden (wenn auch vielleicht nicht unter diesem Namen). Unsere Veranstaltung zeigt gewissermaßen, wie ein großer Teil des bisher Gelernten in der Softwarekonstruktion angewandt werden kann. 4.1
Im Themenbereich Softwareprojektmanagement
überwiegen nicht-formale Inhalte (vgl. Tabelle 2).
Ein Schwerpunkt sind Softwaremetriken als ein
Aspekt der ingenieurmäßigen, objektivierten
Softwareentwicklung (inklusive des Bewusstseins für
Pseudometriken (vgl.
In den Übungsaufgaben ist anhand von vorgegebenen Prozessbausteinen ein kleines Entwicklungsprojekt zu planen inklusive Besetzung von Rollen mit Personen. Um die Tutor::innen insbesondere auf Fragen und Diskussionen zur Verwendung und zum Nutzen von Prozessmodellen vorzubereiten, haben wir entsprechend des Prinzips „lehren, was wir praktizieren“ in 2018 den Prozess des Übungsbetrieb vollständig modelliert. Die Erläuterung des Prozesses ist aufwendig, dafür weiß über das gesamte Semester jede::r Tutor::in, wer wann welches Artefakt wie zu bearbeiten hat und wir können unsere ganze Aufmerksamkeit den eingereichten Lösungsvorschlägen widmen. 4.2
Der Themenbereich Requirements Engineering (RE)
ist in der Veranstaltung etwas stärker gewichtet als
die weiteren Themenbereiche (vgl. Tabelle 2). Dies
ist vor allem drei Überlegungen geschuldet. Erstens
stimmen wir zu (etwa
Wir sprechen bei unseren Diskussionen i.d.R. über die u.E. besonders herausfordernde Situation eines Softwareentwicklungsvertrages zwischen getrennten Kunden- und Entwicklungsunternehmen. Die Softwareentwicklung in Start-Ups, innerhalb einer Abteilung oder zwischen Abteilungen desselben Unternehmens hat ggf. andere Rahmenbedingungen.
Bei der Vermittlung von Problemen und Techniken des RE arbeiten wir mit zwei (bisher leider nicht empirisch belegten) Hypothesen zu Ursachen von Schwierigkeiten. Eine Ursache sehen wir darin, daß der weitaus überwiegende Teil der Übungsaufgaben, die die Studierenden bis zum 4. Semester bearbeiten, von Fachleuten in Fachsprache präzise formuliert sind (nicht zuletzt, um die Korrektur zu vereinfachen). Entsprechend stellen wir Übungsaufgaben zu unserer Veranstaltung absichtlich unpräzise und halten dazu an, in den Einreichungen zunächst die Aufgabenstellung in eigenen Worten wiederzugeben (vgl. Abschnitt 3.3). Als zweite Ursache vermuten wir, daß der Umgang mit Sprache im Alltag von dem in der RE-Arbeit verschieden ist. Im Alltag sind Menschen üblicherweise gern bereit, einen Satz wie:
Spielfiguren müssen indirekt gesteuert werden. direkt als „klar“ zu akzeptieren und keinen Bedarf für Nachfragen zu sehen (fehlende Information wird plausibel aufgefüllt; man sieht nur Information). In der RE-Arbeit geht es unseres Erachtens beim Blick auf den obigen Satz vor allem darum, zu sehen, welche Information der Satz nicht enthält.
Um diesen Sichtwechsel anzuregen, führen wir eine Übung durch, in der die Studierenden eine textuell gegebene Anforderung analysieren. Diese Übung wird in verschiedenen Ausprägungen im REUnterricht eingesetzt, etwa mit Paaren von studentischen Teams, die jeweils die Kunden- bzw. Entwicklerrolle übernehmen oder mit nicht technisch vorgebildeten (echten) Kunden. Wir verwenden eine Variante mit einem technisch vorgebildeten Kunden, da wir in den anderen Szenarien die Gefahr sehen, daß die Parteien aneinander vorbeireden und es aufwendig ist, eine für alle Beteiligten gute Beispiellösung zu erarbeiten. Unser Kunde ist ein Organisator des SoPra, unsere Anforderung war in 2018 der oben genannte Satz. Die Aufgabe besteht darin, durch Kommunikation mit dem Kunden ein Begriffslexikon zu erarbeiten und die nicht im Satz enthaltenen Informationen „herauszukitzeln“. Um die Aufgabe skalierbar zu gestalten, führen zunächst die Organisatoren unserer Veranstaltung eine Anforderungsanalyse durch und notieren die Findungen in einem Wiki. Die Studierenden kommunizieren mit dem (für sie anonymen) Kunden per Mail, vermittelt durch die Tutor::innen. Mit Hilfe des Wiki können die Tutor::innen die meisten Fragen ihrer Tutanden schon im Stile eines Kunden beantworten, noch unklare Aspekte werden an den SoPra-Organisator weitergeleitet und im Wiki nachgeführt; weiterhin sind die Tutor::innen angehalten, die Kommunikation in der Art eines Coaches zu beobachten und Tips für weitere Fragen zu geben. Für das Tutorium bereiten wir eine Liste von bekannten Beispielspielen vor, die die Anforderung lt. Kunde erfüllen bzw. nicht erfüllen. Im Tutorium sollen die Teilnehmer::innen durch Handzeichen pro Beispiel anzeigen, ob nach ihrer konkreten Anforderungsanalyse das Beispiel vom Kunden akzeptiert oder abgelehnt wird bzw. ob sie sich nicht sicher sind. In 4 Jahren Durchführung dieser Übung hat noch nicht ein Team alle Beispiele korrekt klassifiziert; dies wird durch das Verfahren mit den Handzeichen im Tutorium unmittelbar für die Studierenden erfahrbar.
In der Einführung der Problemstellung der
Anforderungsanalyse und nicht-formalen Beschreibung
von Anforderungen folgen wir
Als Einstieg in die formale Beschreibung von Anforderungen haben wir als eine möglichst einfache Sprache die in vielen Lehrbüchern semi-formal eingeführten Entscheidungstabellen (ET) ausgewählt. ET sind eine der einfachsten Beschreibungssprachen, die mit formaler Semantik und Analysen versehen werden können, sind jedoch weder trivial noch eine artifizielle Lehrsprache. Die schlichten Sprachmittel von ET reichen vollständig aus, um Anforderungen zu beschreiben, die in textueller Form sehr schnell nicht mehr überblickbar, wartbar oder analysierbar sind. T : decision table c1 description of condition c1 ... ... cm description of condition cm a1 description of action a1 ... ... ak description of action ak r1 · · · rn v1,1 · · · v1,n
... ... ... vm,1 · · · vm,n w1,1 · · · w1,n
... ... ...
wk,1 · · · wk,n
Abbildung 2: Konkrete Syntax von ET.
Formal ist eine ET T über disjunkte Mengen von Bedingungen C und Aktionen A eine n × m-Matrix (siehe Abbildung 2) wobei c1, . . . , cm ∈ C, a1, . . . , ak ∈ A, v1,1, . . . , vm,n ∈ {−, ×, ∗}, und w1,1, . . . , wk,n ∈ {−, ×}. Eine wohlgeformte ET hat einen Namen. Spalten (v1,i, . . . , vm,i, w1,i, . . . , wk,i), 1 ≤ i ≤ n, werden Regeln genannt und haben einen eindeutigen Namen (hier: r1, . . . , rn). Die Vektoren (v1,i, . . . , vm,i) und (w1,i, . . . , wk,i) heißen Prämisse und Effekt von Regel ri. Die Semantik einer ET T ist durch die Funktion F gegeben, die jeder Regel r in T eine Formel der propositionalen Logik über C und A wie folgt zuordnet. Seien (v1, . . . , vm) und (w1, . . . , wk) Prämisse und Effekt von r. Dann ist
F (r) := V1≤i≤m F (vi, ci) ∧ V1≤j≤k F (wj , aj) (1) | =:F{pzre(r) } | =:F{ezff (r) } mit F := {(×, x) 7→ x, (−, x) 7→ ¬x, (∗, x) 7→ true}. Die Teilformeln Fpre(r) und Feff (r) heißen Prämissen- bzw. Effektformel.
Eine ET kann wie folgt zur Formalisierung einer Anforderung der Art, daß Systemverhalten in akzeptabel (oder erwünscht) und unerwünscht klassifiziert wird, verwendet werden. Ein System erfüllt die durch ET T gegebene Anforderung genau dann, wenn jedes beobachtbare Systemverhalten durch eine Regel in T erlaubt wird. Formal kann eine Beobachtung eines Systems bzgl. der Bedingungen und Aktionen in C und A, also welche Bedingungen aus C erfüllt sind und welche Aktionen aus A ausgeführt werden, als Boole’sche Belegung σ : C ∪ A → {0, 1} der logischen Variablen in C ∪ A notiert werden. Die Beobachtung σ erfüllt T genau dann, wenn es eine Regel r in T gibt, sodaß σ |= F (r).
Begriffe wie Vollständigkeit können für ET präzise definiert werden, z.B. nennen wir eine ET T (formal) vollständig, wenn die Disjunktion der Prämissenformeln von T eine Tautologie ist. Das Problem der Analyse auf (formale) Vollständigkeit kann auf das Erfüllbarkeitsproblem propositionaler Logik reduziert werden, für das in Form von sogenannten SAT-Solvern Entscheidungswerkzeuge zur Verfügung stehen.
In der Vorlesung ‚Softwaretechnik‘ diskutieren wir
nun nicht eine Reduktionsprozedur oder die
Konstruktion von SAT-Solvern, sondern nehmen eine
Nutzersicht ein, nehmen also zur Kenntnis, daß
Werkzeuge dieser Art existieren. Wir führen am Beispiel der
ET die wichtige Diskussion, wie sich z.B. die formale
Vollständigkeit einer ET zur vollständigen Erfassung
einer Anforderung im Sinne von
Die Übungsaufgaben zu ET umfassen verschiedene
formale Analysen von gegebenen ET sowie eine
Aufgabe, in der ein Transkript eines Kundeninterviews
(mit absichtlichen Redundanzen und
Mehrdeutigkeiten) im Umfang von ca. einer DIN-A4-Seite in eine
ET mit ca. 10 Regeln über jeweils 5 Bedingungen und
Aktionen überführt werden soll. Im Tutorium stellen
wir die (provokante) Frage: Nehmen wir an, man
müsste als Implementierer::in des Kundenwunsches
zwischen Text und ET als Spezifikation wählen, was
wäre die Wahl? Und warum? Meiner Kenntnis nach
hat sich in den 4 Jahren der Veranstaltung noch
niemand ausdrücklich den Text gewünscht. Hier
versuchen wir, einen Aspekt sichtbar zu machen, der
unserer Meinung nach im Kontext formaler
Beschreibungen noch vor der Anwendung von formalen
Analysen steht. Eine formale Beschreibung einer
Anforderung hat den Effekt, daß (mit hoher
Wahrscheinlichkeit) alle im verwendeten Formalismus ausgebildeten
Softwaretechniker::innen zu jeder Zeit dieselbe
Information sehen.8 So sehen wir formale
Beschreibungen zuvorderst als Werkzeug, um auf Seiten der
Softwaretechniker::innen das Risiko von
Missverständnissen zu verringern. Als Analogie verwenden wir z.B.
von Jurist::innen konstruierte Individualverträge,
deren Konsequenzen man als Nicht-Jurist
üblicherweise nicht überblicken kann. Man hat als
Auftraggeber des Individualvertrags jedoch den Anspruch, von
8Gestandene Praktiker::innen berichten, daß es vorkommt, daß
dieselbe Person am selben Tag einen Text verschieden interpretiert.
der Fachperson eine „Übersetzung“ zu erhalten bzw.
darauf, wichtige Szenarien gemeinsam
durchzuspielen. Ebenso hat man als Softwarekunde einen
Anspruch, von den Entwickler::innen deren z.B. in
formaler Form notiertes Verständnis der
Anforderungen erklärt zu bekommen. Dies kann insbesondere
durch Szenarien gelingen (vgl.
Die Klausur umfasst Aufgaben verschiedener
Taxonomie-Stufen zu ET, vom Beweis z.B. der
Vollständigkeit einer ET, über die Analyse einer gegebenen
ET auf Konsistenz bis hin zur Erstellung einer
kleinen ET zu einem Text. Die Ergebnisse (vgl.
Als komplexen Formalismus (mit höherer
Ausdrucksstärke und Informationsdichte, und höherem
Aufwand zur Definition von (abstrakter) Syntax und
Semantik) haben wir Live Sequence Charts
Die Klausur umfasst Aufgaben zur Konstruktion der Automaten sowie erfragt Beispiele für akzeptierte bzw. nicht akzeptierte Systemberechnungen. Nicht zuletzt da die Einführung von LSCs den technisch anspruchsvollsten Teil unserer Vorlesung darstellt, sehen wir diese Aufgaben im „mittleren“ und „schweren“ Bereich, der am Ende die guten und sehr guten Gesamtnoten entscheidet. Mit den Resultaten sind wir auch hier zufrieden, das untere Quartil endet bei 8,5 bzw. 7 von 15 bzw. 16 Punkten, das obere Quartil beginnt bei 13 bzw. 12 Punkten.
Im ersten Jahr waren wir von den guten Ergebnissen bei aller Zuversicht positiv überrascht. Wir hatten uns vereinzelt vorgetragenen Sorgen, daß die LSCSemantik zu schwer sein könnte, nicht völlig entziehen können und entsprechend Vorsorge getragen, die Aufgaben zu LSCs ggf. aus der Wertung zu nehmen. 4.3
Im Themenbereich Softwarearchitektur und Entwurf
liegt der Schwerpunkt auf der Modellierung der
Struktur und des Verhaltens von Softwaresystemen
als Baupläne im Sinne von
Eigenschaften von Strukturen können mit Hilfe der Object Constraint Language (OCL) formalisiert werden. Hier führen wir Proto-OCL ein, eine Teilsprache der OCL, deren konkrete Syntax sich an der den Studierenden vertrauten Form der Logik erster Stufe orientiert. Die Semantik von Proto-OCL ist eine Interpretationsfunktion, die eine gegebene Proto-OCLFormel und einen gegebenen Systemzustand (oder ein vollständiges Objektdiagramm) auf einen der drei (!) Werte true, false und ⊥ abbildet. Wir stellen die Besonderheiten heraus, daß OCL Assoziationen verschiedener Multiplizität verschieden behandelt sowie die Bedingungen, unter denen man eine Auswertung zum dritten Wahrheitswert beobachten kann.
Für die konstruktive Modellierung von Verhalten
führen wir eine einfache Teilsprache von
StateMachines ein. Unsere Communicating Finite
Automata (CFA) sind im Wesentlichen nicht-hierarchische
State-Machines mit Rendezvous-Synchronisation,
d.h. zwei Kanten in verschiedenen Automaten
können eine Transition begründen, wenn je eine
der Kanten bzgl. eines Events sende- bzw.
empfangsbereit ist. Dieses Synchronisationsparadigma
ist mit durch State-Machines implementierten
Behavioural Features in UML vergleichbar jedoch
nicht (ohne weitere Annahmen) identisch. Zu dieser
Abweichung von der UML-Semantik haben wir uns
vorrangig aus zwei Gründen entschieden. Einerseits
erfordert die formale Einführung des abstrakten
Event-Speichers (in der die UML-Semantik
bekanntlich parametrisiert ist) sowie einer konkreten
Ausprägung, etwa einer empfängerseitigen
FIFOQueue, wie sie IBM Rhapsody verwendet, in unserer
UML-Veranstaltung ca. 2 Vorlesungen. Der
Erkenntnisgewinn im Vergleich zum Aufwand erscheint uns
für eine Softwaretechnik-Veranstaltung zu gering.
Andererseits steht mit Uppaal
Die Übungsblätter zu CFA umfassen Aufgaben zur Erstellung eines Modells eines verteilten Algorithmus für Mutual-Exclusion (das den Teilnehmer::innen als Problem aus der Betriebssysteme-Vorlesung bekannt sein müsste), zur Simulation verschiedener Abläufe und zur Verwendung von Uppaal’s Temporallogik (Query Language) zur Spezifikation und Verifikation der Mutual-Exclusion-Eigenschaft. Mit den Übungen verfolgen wir insbesondere das Ziel, das mächtige Modellierungskonzept des Nichtdeterminismus und die durch nebenläufiges Verhalten induzierten Schwierigkeiten sichtbar zu machen.
In der Klausur ist üblicherweise der Transitionsgraph eines gegebenen Systems von mehreren CFAs zu erstellen. Mit den Ergebnissen sind wir durchweg zufrieden, der Median liegt zwischen 10 und 12,25 von 13 Punkten, das obere Quartil beginnt zwischen 12 und 13 Punkten, liegt also im sehr guten Bereich.
Im Themenbereich Qualitätssicherung betrachten wir speziell die Prüfung von Programmcode. Hier diskutieren wir zunächst die Disziplin des Softwaretestens. Dem formalen Charakter der gesamten Veranstaltung folgend, führen wir Testfälle als Paare (In, Soll) aus einer (Menge von) Eingabe(n) und Soll-Wert(en) ein. Eine Ausführung eines Testfalls ist eine Beobachtung des Systems, die Eingaben entsprechend In erhält, was ein einzelner Wert oder eine Sequenz von z.B. Events sein kann. Ein Test ist negativ (Test passed) genau dann, wenn die betrachtete Beobachtung ein Ele9Daß Uppaal für CFAs mit Uhrenvariablen, also Timed Automata, entwickelt wurde, verschweigen wir schlankerhand.
10Aus denselben Überlegungen führen wir kein Werkzeug zur
Erstellung von Klassendiagrammen ein. Die für die Einarbeitung
in die Bedienung der meisten dieser Werkzeuge notwendige Zeit
steht unserer Meinung nach in keinem akzeptablen Verhältnis zu
den Absichten z.B. unserer Übungen (vgl.
11Einige Teilnehmer::innen unserer UML-Veranstaltung, in der
wir IBM Rhapsody verwenden, vermissen die mächtige und leicht
zu bedienende Simulationsfunktion von Uppaal.
ment von Soll ist. Hier betonen wir (
Als gegenüber den etablierten Lehrbüchern
neuen Inhalt präsentieren wir Programmverifikation
nach
Da die Veranstaltung neu konstruiert wurde, beobachten wir seit der ersten Durchführung verschiedene Metriken (vgl. Abschnitt 4.1) auf Indizien für Fehlentwicklungen. Daten beziehen wir aus dem Übungsbetrieb, den Klausuren und der zentralen Evaluation.
In der Evaluation beachten wir besonders die
Aspekte „Workload“ und „Niveau“
Den Lernerfolg bzgl. des Lernziels der Vermittlung von Methoden und Techniken messen wir anhand der Klausurergebnisse, mit denen wir über alle 4 Jahre sehr zufrieden sind. Das viel interessantere Lernziel der Vorbereitung auf das „echte Leben“ läßt sich leider notorisch nicht gut messen. Als ein positives Indiz sehen wir unsere und von Kolleg::innen berichtete Erfahrung aus Vorgesprächen zu individuellen Projekten wie etwa B. Sc.-Arbeiten. Hier nehmen wir die Inhalte der Vorlesung als (angestrebten) soliden Bezugspunkt wahr, um über spezialisierte Aufgabenstellungen zu sprechen. Wir hoffen, daß sich die Veranstaltung ebensogut als Bezugspunkt für den Einstieg in die berufliche Karriere der Studierenden eignet. 6
Formale Methoden werden zunehmend in vielen Bereichen der Softwaretechnik angewandt. Unserer Überzeugung nach ist es hilfreich, wenn die Bedeutung formaler Beschreibungen vollständig durchdrungen wird und die aus formalen Analysen zu ziehenden Schlüsse verstanden werden.
Unsere Erfahrung zeigt, daß es möglich ist, eine Veranstaltung zur Einführung in die Softwaretechnik im Grundstudium um genau diese Aspekte zu ergänzen ohne hierbei die Inhalte der etablierten Lehrbücher zu vernachlässigen.
Danksagungen. Wir danken Sergio Feo Arenis und Christian Schilling für ihre Unterstützung als Assistenten der ersten beiden bzw. des letzten Jahres. Ohne die Gespräche mit Sergio und Christian und ihre Ausarbeitung und Weiterentwicklung der Übungsaufgaben wäre die Veranstaltung in ihrer heutigen Form nur schwer vorstellbar. Weiterhin danken wir unseren stud. Hilfskräften für ihre engagierte Mitarbeit an Aufgaben und Tutorials.