=Paper=
{{Paper
|id=Vol-2358/paper-02
|storemode=property
|title=Formale Methoden in der Softwaretechnik-Vorlesung
(Formal Methods in the Software Engineering Lecture)
|pdfUrl=https://ceur-ws.org/Vol-2358/paper-02.pdf
|volume=Vol-2358
|authors=Bernd Westphal
|dblpUrl=https://dblp.org/rec/conf/seuh/Westphal19
}}
==Formale Methoden in der Softwaretechnik-Vorlesung
(Formal Methods in the Software Engineering Lecture)==
https://ceur-ws.org/Vol-2358/paper-02.pdf
Formale Methoden in der
Softwaretechnik-Vorlesung
Bernd Westphal, Albert-Ludwigs-Universität Freiburg
westphal@informatik.uni-freiburg.de
Zusammenfassung informal • informal •
Dieser Artikel stellt die Ergänzung einer Einfüh-
rung in die Softwaretechnik um Formale Metho- semi-formal • semi-formal •
den im Bereich Requirements Engineering, Software-
Modellierung und Qualitätssicherung vor. Wir be-
schreiben die Konstruktion der Veranstaltung und be- formal formal
richten empirische Daten und Erfahrungen aus 4 Jah- • • • •
ren der Durchführung. Ein Schwerpunkt ist die Be- simple complex
schreibung der verwendeten didaktischen Methoden (a) (b)
zur Vermittlung der neuen Inhalte. Abbildung 1: Einführung Formaler Methoden.
Abstract
This article presents the extension of an introductory den (Semi-)Entscheidungsprozeduren. Das Ziel der
course on software engineering by formal methods Ergänzung um Formale Methoden ist motiviert durch
in the topic areas requirements engineering, software unsere Erfahrung in zahlreichen Projekten mit Part-
modelling, and quality assurance. We describe the nern aus der Industrie von kleinen Anbietern sicher-
construction of the course and report empirical data heitskritischer Systeme (z.B. (Arenis u. a., 2016))
and experience from 4 years of conducting the course. bis hin zu großen Automobilanbietern und Zuliefe-
A focus of this article is the description of didactical rern (z.B. (Langenfeld u. a., 2016)). In der Projekt-
methods employed for teaching the new content. arbeit nehmen wir eine klare Nachfrage nach und
Anwendung (!) von Formalen Methoden im oben ge-
1 Einleitung nannten Sinne in verschiedenen Bereichen der Soft-
Im Studienplan des Bachelorstudiums der Informatik waretechnik in den Firmen wahr. Hierbei steht übli-
der Universität Freiburg ist eine einsemestrige Veran- cherweise nicht die vollständige und umfassende for-
staltung zur Einführung in die Disziplin der Softwa- male Beschreibung von Anforderungen und Entwurfs-
retechnik vorgesehen. Das Modulhandbuch fordert, entscheidungen bzgl. Struktur und Verhalten im Vor-
wie in Deutschland nicht unüblich, eine Übersicht dergrund (wie es etwa im Luft- und Raumfahrtbe-
über die Problembereiche, Konzepte und Techniken reich teilweise angestrebt wird), sondern eine ange-
der Softwaretechnik, wie sie von den bekannten Lehr- messene Verwendung von Formalen Methoden, um
büchern, etwa (Sommerville, 2010; Balzert, 2009; bestimmte, besonders kritische oder risikobehaftete
Ludewig u. Lichter, 2013), abgedeckt werden. Im Jah- Aspekte von Software zu beschreiben und zu ana-
re 2015 stand eine Überarbeitung der Vorlesung ‚Soft- lysieren. Dem entsprechend möchten wir heute be-
waretechnik‘ an, über deren Resultat wir in diesem ginnen, die in vielen Einführungen in die Software-
Artikel berichten. technik fest etablierte (semi-formale) Modellierung
Zwei Ziele standen bei der Überarbeitung der Ma- von Softwareaspekten in unserer Einführungsveran-
terialien im Fokus. Erstens ein „Zurechtrücken“ der staltung um eine formale Sicht zu erweitern und den
Proportionen der verschiedenen Bereiche der Softwa- Studierenden eine Übersicht über Konzepte, Möglich-
retechnik in den Materialien (die über mehrere Jah- keiten und Voraussetzungen Formaler Methoden für
re von verschiedenen Veranstaltern verwendet und ihre zukünftigen Berufssituationen zu vermitteln.
bearbeitet wurden), und zweitens eine neue Ergän- Mit diesem Ziel ergibt sich neben der üblichen
zung der Materialien um eine verständliche und nach- Herausforderung, aus dem umfangreichen Angebot
vollziehbare Einführung formaler Beschreibungsspra- der Lehrbücher eine ausgewogene Vorlesung zusam-
chen und Analysetechniken (kurz Formale Metho- menzustellen, die Herausforderung, Lehrmaterialien
den), also Beschreibungssprachen mit formal defi- für den Bereich Formale Methoden auszuwählen bzw.
nierter Syntax und Semantik und darauf aufbauen- herzustellen. Interessanterweise ist die zweite Her-
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 21
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
ausforderung keine Teilmenge der ersteren. In den den Rahmen unserer Veranstaltung sprengen würde
etablierten Lehrbüchern (s.o.) und dem vorhandenen und für unsere Lernziele nicht notwendig ist. Weiter-
Material wird ganz überwiegend ein Ansatz verfolgt, hin ist das Material u.E. so weit von der (heutigen
den wir in Abbildung 1(a) visualisieren. Wir sehen und mutmaßlich morgigen) Lebenswirklichkeit und
die für z.B. die Beschreibung von Anforderungen ver- den etablierten Lehrbüchern entfernt, daß wir anneh-
fügbaren Mittel auf einer Achse, die von informal men müssen, daß es Studierenden unnötig schwer
(rein natürlichsprachlich), über semi-formal (mit for- fallen würde, andere Lehrbücher oder Fortbildungen
maler konkreter Syntax, aber ohne formale abstrakte in der Arbeitssituation zu unserer Veranstaltung in
Syntax oder Semantik) hin zu formal (mathematisch Bezug zu setzen. Unser (zugegeben: hoher) Anspruch
präzise definierte Syntax und Semantik) reichen. Die an unsere Veranstaltung ist, daß nach der Teilnahme
vorgenannten Lehrbücher und Materialien bewegen an unserer Veranstaltung keines der etablierten Lehr-
sich auf dieser Achse zwischen informal und semi- bücher große konzeptionelle Überraschungen bereit
formal und geben kurze Ausblicke auf Formale Me- hält, sondern nur von den Studierenden einordne-
thoden, indem Beispiele auf einer intuitiven Ebene bares, zusätzliches Hintergrundwissen sowie weitere
diskutiert werden. Bei diesem Ansatz sehen wir ein Techniken liefert.
inhärentes Problem, das bereits Lehman & Buth (Leh- In diesem Artikel beschreiben wir die Konstrukti-
mann u. a., 2015) beschreiben: „Es darf nicht erwar- on unserer Vorlesung zur Einführung in die Softwa-
tet werden, dass die Studierenden UML Modelle er- retechnik im Grundstudium, in der die in etablierten
stellen können, wenn in der Vorlesung nur die einzel- Lehrbüchern zur Softwaretechnik (s.o.) vorgestellten
nen Symbole durchgearbeitet werden und dann auf Inhalte um Techniken zur Beschreibung von Anforde-
dieser Basis in der Prüfung Analyseaufgaben auf ei- rungen und Entwurfsaspekten vollständig formal, al-
nem gegebenen Diagramm gestellt werden.“ Streng so mit konkreter Syntax und präziser abstrakter Syn-
genommen können wir schon nicht erwarten, daß tax und Semantik, ergänzt werden, und berichten von
Studierende in Bloom’s Taxonomie echt leichtere Auf- Erfahrungen aus vier Sommersemestern mit der neu
gaben, wie etwa gegebene Objektdiagramme darauf- gestalteten Veranstaltung. Schwerpunkt dieses Arti-
hin analysieren, zu welchem der (drei) Wahrheits- kels sind die Voraussetzungen der Veranstaltung (ins-
werte eine gegebene OCL-Formel ausgewertet wird, in besondere die Einbettung in den Studienplan), Kon-
Übungen so zu bearbeiten, daß gegenüber den Tu- sequenzen der ergänzten Inhalte für Übungen und
tor::innen die Korrektheit der Lösung argumentiert Klausur, sowie Organisation und didaktische Maß-
(im besten Falle: bewiesen) werden kann bzw. von nahmen (vor allem Bereich des Übungsbetriebs), mit
Seiten der Tutor::innen die Inkorrektheit eines Lö- denen wir die Vermittlung und Erarbeitung der neu-
sungsvorschlags bewiesen und systematisch erklärt en Inhalte unterstützen. Die neuen Inhalte als solche
werden kann. Unser Lösungsansatz besteht darin, in werden für den Bereich Requirements Engineering
der Veranstaltung Endpunkte der Formalitätsachse zu in (Westphal, 2018) vorgestellt und sind zudem auf
behandeln. Wir diskutieren sowohl informale Ansät- der Homepage der Veranstaltung frei zugänglich.1
ze (und im Themenbereich Requirements Enginee- Der Artikel ist wie folgt strukturiert. In Abschnitt 2
ring verschiedene semi-formale Ansätze) und sprin- beschreiben wir die Situation der Veranstaltung im
gen dann zu vollständig definierten Beschreibungs- Studienplan der Universität Freiburg sowie der Stu-
sprachen, die für den Zweck der Vorlesung (bis auf dierenden zu Beginn der Veranstaltung. Abschnitt 3
eine Ausnahme) auf einen essentiellen Kern reduziert legt unsere Lernziele dar und beschreibt, wie wir die
sind (vgl. Abbildung 1(b)). Auf diese Weise geben wir neuen Inhalte bzgl. Formaler Methoden durch didak-
eine konkrete Übersicht über die gesamte Achse. Für tische Maßnahmen im Übungsbetrieb unterstützen.
eine ausgewählte Beschreibungssprache diskutieren Einen Überblick über die neuen Inhalte, ihre Einbet-
wir mehr als einen essentiellen Kern, um zu demons- tung in die gesamte Vorlesung und unsere Erfahrun-
trieren, daß es eine orthogonale Achse der Einfach- gen bzgl. Lernerfolgen gibt Abschnitt 4. Wir schließen
heit formaler Beschreibungssprachen gibt (Einfach- den Artikel mit einer Betrachtung von Evaluationser-
heit sowohl bzgl. der Ausdrucksstärke als auch bzgl. gebnissen und einer Zusammenfassung.
des Aufwands, zu einer vollständigen Definition (von
abstrakter Syntax und Semantik) zu gelangen). 2 Kontext der Veranstaltung und
Für den Bereich der Formalen Methoden in der
Situation der Studierenden
Softwaretechnik steht mit (Bjørner, 2006a,b,c) ein Die Veranstaltung ‚Softwaretechnik‘ ist eine Pflicht-
dreibändiges Lehrbuch zur Verfügung, das versucht, vorlesung im B. Sc.-Studiengang Informatik der Uni-
die Softwareentwicklung vollständig aus formaler versität Freiburg mit einem Umfang von 3+1 SWS für
Sicht zu vermitteln. Wir haben uns aus zwei Grün- Vorlesung und Übung und 6 ECTS-Punkten. Zusätz-
den dagegen entschieden, diesem Lehrbuch zu fol- lich besuchen Studierende des nicht-konsekutiven
gen. Zunächst scheint uns das Ziel des Materials von Masterstudiengangs, der Studiengänge ‚Embedded
Bjørner zu sein, formale Beschreibungssprachen mög- 1 Die URL für das Sommersemester 2018 ist: https://swt.
lichst in vollem Umfang darzustellen, was schlicht informatik.uni-freiburg.de/teaching/SS2018/swtvl
2
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 22
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
Tabelle 1: Selbsteinschätzung der Erfahrung (Minimum · 1., 2., 3. Quartil · Maximum).
Proj. Mgmt. Req. Eng. Programm. Modellierung QA
2016 (77 Antw.) – 0 · 1 · 1 · 3 · 9 1 · 2 · 3 · 5 · 10 0 · 1 · 1 · 2 · 7 0 · 1 · 2 · 3 · 9
2017 (87 Antw.) 0 · 0 · 1 · 3 · 10 0 · 1 · 1 · 4 · 10 0 · 2 · 3 · 5 · 10 0 · 1 · 1 · 3 · 10 0 · 1 · 1 · 4 · 10
2018 (64 Antw.) 0 · 0 · 1 · 3 · 8 0 · 0 · 1 · 2 · 8 1 · 1 · 3 · 5 · 10 0 · 1 · 1 · 3 · 9 0 · 1 · 2 · 4 · 10
Systems Engineering‘ (ESE) und ‚Mikrosystemtech- the planning and execution of the activity in a software deve-
nik‘ sowie des bivalenten Studiengangs Informatik lopment project within defined resource and time constraints.
die Veranstaltung. In den vier Jahren der Veranstal-
tung haben wir zwischen 80 und 150 angemelde- Tabelle 1 zeigt die bisherigen Ergebnisse, die unse-
te Teilnehmer::innen beobachtet. Unter den Teilneh- re Annahmen durchweg bestätigen. Etwas überra-
mer::innen (der Evaluation2 ) studierten zwischen 73 schend finden wir, daß sich das obere Quartil der
und 96 % Informatik, der zu 100 % fehlende Teil Studierenden im Bereich Programmierung regelmä-
wird stark von ESE-Studierenden dominiert. Außer in ßig als relativ erfahren einschätzte, sich im Bereich
2016 strebten jeweils mehr als knapp zwei Drittel der Qualitätssicherung (der die Aktivität des Testens ein-
Teilnehmer::innen einen B. Sc.-Abschluss an. schließt, von der man erwarten sollte, daß diese
Die ‚Softwaretechnik‘ ist im 4. Semester vor- mit ernsthafter Programmierung einhergeht) als eine
gesehen, d.h. wir können einen zweiteiligen Pro- oder zwei Stufen geringer erfahren einordnet.
grammierkurs und Algorithmen & Datenstrukturen, In der zweiten Vorlesung zeigen und diskutieren
Technische und Praktische Informatik (Betriebssyste- wir die Ergebnisse des jeweiligen Jahres. Mit der Prä-
me, Netzwerke, Datenbanken) und die Mathematik- sentation der Ergebnisse verbinden wir die folgenden
Vorlesungen voraussetzen. Logik und die Einführung Botschaften: Erstens, daß wir, d.h. die Veranstalter
in die Theoretische Informatik sind in Freiburg im und die Studierenden, es (auch dieses Jahr wieder)
3. Semester vorgesehen, liegen also auch zeitlich vor mit einem bzgl. Vorerfahrung eher heterogenen Au-
der ‚Softwaretechnik‘. Parallel zur ‚Softwaretechnik‘ ditorium zu tun haben. Zweitens, daß die Vorlesung
findet für die B. Sc.-Studierenden der Informatik ein explizit für Studierende angelegt ist, die sich zwi-
Softwarepraktikum statt (vgl. Abschnitt 3). schen den Werten 0 und 1 einordnen (und daß die-
Entsprechend der Position der ‚Softwaretechnik‘ im se Studierenden in der klaren Mehrheit sind, man al-
Curriculum und aus der Erfahrung der Jahre vor so nicht „allein“ ist, wenn man sich dort eingeordnet
2015 gehen wir einerseits davon aus, daß der Groß- hat). Drittens, daß für die Studierenden, die sich bei
teil der Teilnehmer::innen vor unserer Veranstaltung Werten von 5 und höher einordnen, möglicherweise
bzgl. der meisten Themenbereiche der Softwaretech- keine Neuigkeiten vermittelt werden, daß diese Stu-
nik über wenig bis sehr wenig Erfahrung verfügt. dierenden jedoch explizit eingeladen sind, in Form
Andererseits wissen wir aus persönlichen Gesprä- von Fragen oder Kommentaren ihre Vorerfahrung in
chen, daß es im nicht-konsekutiven M. Sc.-Programm den Vorlesungs- und Übungsterminen einzubringen.
durchaus einzelne Studierende gibt, die über mehr- In der Diskussion der Ergebnisse stellen wir heraus,
jährige Berufserfahrung verfügen. daß die Inhalte der Vorlesung die Studierenden dar-
Seit 2016 überprüfen wir diese Annahme durch auf vorbereiten möchten, in Softwarentwicklungspro-
eine Aufgabe auf dem ersten Übungsblatt, in der jekten höherer Stufen mitzuarbeiten, also Projekte
wir die Teilnehmer um eine Selbsteinschätzung der die einen größeren Umfang und eine größere Nutzer-
Vorkenntnisse in den Themenbereichen (die wir in basis haben als jedes Projekt, das man im Studium in
der ersten Vorlesung jeweils grob umreißen) Projekt- Freiburg erlebt, sowie üblicherweise einen wirtschaft-
management (seit 2017), Requirements Engineering, lichen Aspekt haben.
Programmierung, Modellierung und Qualitätssiche-
rung bitten. Wir schlagen in der Aufgabe die folgende, 3 Ziele und Konstruktion
subjektiv zu interpretierende Skala vor (die Übungs-
blätter sind in Englisch verfasst):
der Veranstaltung
Ein Lernziel unserer Veranstaltung ist zunächst, wie
0: I have no experience in that activity whatsoever. I have not
taken any related subjects during my studies. in der Einleitung beschrieben, eine Übersicht über
die verschiedenen Themenbereiche der Softwaretech-
1: I have only performed the activity in the context of a lecture nik entsprechend der etablierten Lehrbücher zu ge-
or programming course.
ben. Unser Schwerpunkt ist hierbei die Vermittlung
10: I have performed the activity in a project with a large user ba- der verschiedenen Probleme, die sich daraus ergeben,
se (100+ users), a large work volume (36+ person-months) daß mehrere Menschen über einen längeren Zeit-
or a specific commercial purpose. I have been responsible for raum zusammen nichttriviale Softwaresysteme entwi-
2 Zwischen 26 und 40 Angaben; leider haben wir keinen direk- ckeln, sowie bekannte Lösungsansätze und deren Vor-
ten Zugriff auf Studiengang oder angestrebten Abschluss. und Nachteile vorzustellen.
3
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 23
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
Der neue Aspekt unserer Veranstaltung ist die voll- Bei der Punkteverteilung der Klausur orientieren
ständig formale Definition von Beschreibungsspra- wir uns grob an den Stufen der (überarbeiteten) Ta-
chen und Analysetechniken an den entsprechenden xonomie der Lernziele (Bloom, 1956; Anderson u. a.,
Stellen in der Vorlesung (vgl. Tabelle 2). Die Lernzie- 2001). Circa 50 % der Punkte entfallen auf „leichte“
le sind hier das sichere Verstehen und Anwenden der Aufgaben (Vokabular, einfache Verfahren verstehen
eingeführten Formalen Methoden, sowie die Interpre- und wie in den Übungen (jedoch auf andere Proble-
tation von Analyseergebnissen. Die entsprechenden me) anwenden), ca. 33 % der Punkte entfallen auf
Inhalte und die Einbettung in die Vorlesung werden „mittlere“ Aufgaben (ähnlich wie Übungsaufgaben, je-
in Abschnitt 4 beschrieben. doch Analyse bzw. Transfer notwendig) und ca. 17 %
der Punkte sind für „schwere“ Aufgaben (nicht in
Wir beschreiben die Ziele unserer Veranstaltung in den Übungen besprochen, neue Sichten auf diskutier-
der ersten Vorlesung, um Missverständnisse (und Ent- te Konzepte, offenere kreative Aufgaben) vorgesehen.
täuschungen) zu vermeiden. In einer Aufgabe des ers- Unsere Absicht ist, Kompetenzen über alle kognitiven
ten Übungsblattes bitten wir die Studierenden, aus- Kategorien hinweg zu prüfen; in der o.g. Punktever-
gehend von der ersten Vorlesung ihre Erwartungen teilung reicht es z.B. zum Bestehen nicht aus, alle
an die Veranstaltung in eigenen Worten zu beschrei- „schweren“ Aufgaben (ggf. intuitiv oder zufällig) zu
ben. In der zweiten Vorlesung stellen wir eine Aus- lösen, sondern es sind Punkte aus den Bereichen Ver-
wahl der Antworten vor, und gehen jeweils darauf stehen und Anwenden zum Bestehen notwendig.
ein, inwiefern die Veranstaltung diese Erwartungen
erfüllen kann. Ein über die Jahre wiederkehrender 3.2 Vorlesungen
Punkt, ist der Wunsch, gutes Design zu lernen. Diese Teil unserer Veranstaltung ‚Softwaretechnik‘ ist eine
Erwartungen liefern einen guten Anlass, erneut aus- klassische Vorlesung im Umfang von 3 SWS. Um nicht
zuführen, daß ein Ziel der Vorlesung ist, fundamenta- an einem Tag der Woche auf eine Stunde Tutorium
le Designprobleme zu verstehen und Designentschei- umschalten zu müssen, interpretieren wir das 3+1-
dungen präzise zu beschreiben und auf Aspekte gu- Format als drei Vorlesungen (à 90 Minuten) und ein
ten Designs hin zu analysieren, wir jedoch keine kon- Tutorium (à 90 Minuten) in zwei Wochen.
kreten Verfahren zur Erstellung guter Designs für spe- Über die vorhandene Infrastruktur zeichnen wir
zifische Anwendungsfelder diskutieren. Wir plausibi- das gesprochene Wort und den Bildschirminhalt auf
lisieren diese Zielsetzung durch eine grobe Beschrei- und stellen die Aufzeichnungen zeitnah zur Verfü-
bung des weiten Spektrums von Software: von Onli- gung. Auf diese Weise konnten wir die Vorlesungen
neshops, über Standardanwendungen (Textverarbei- ohne Skript bestreiten, da das gesprochene Wort je-
tung, etc.), kommerzielle Spiele, Betriebswirtschaftli- derzeit zum Nachhören verfügbar ist. Weiterhin kön-
che Software, bis hin zu sicherheitskritischen, einge- nen die Teilnehmer::innen, denen unser Vortrag zu
betteten Systemen. Jeder dieser Bereiche hat eigene, langsam oder zu ausführlich ist, die Geschwindig-
bewährte Vorstellungen von gutem Design, die unter- keit beim Anhören der Aufzeichnung selbst bestim-
einander nicht austauschbar sein müssen. men. Entsprechend der Selbsteinschätzung der Teil-
nehmer::innen (vgl. Abschnitt 1) sprechen wir in der
3.1 Klausur Vorlesung lieber zu langsam als zu schnell und be-
trachten neue Inhalte ggf. aus mehreren Perspekti-
Ähnlich wie (Lehmann u. a., 2015), haben wir sehr ven, was für einige Teilnehmer::innen zu langsam
früh in der Überarbeitung der Veranstaltung mit sein kann. In der Evaluation geben, über die Jah-
der Vorbereitung der Klausur begonnen. Laut Mo- re 2016 bis 2018 aggregiert,3 von 99 Rückmeldun-
dulhandbuch ist eine schriftliche Prüfung vorgese- gen knapp 25 % an, sich die Inhalte hauptsächlich
hen und somit war klar, daß die Vorlesung notwen- durch Anwesenheit anzueignen, und 18 % bzw. 33 %
dig schriftlich prüfbare Inhalte in hinreichendem Um- geben ‚teils/teils‘ bzw. ‚hauptsächlich über die Auf-
fang und Tiefe präsentieren muß. Um das Risiko zeichnungen‘ an. Entsprechend haben wir eher ge-
zu mindern, zum zentral festgelegten Klausurtermin ringe Besucherzahlen in der eigentlichen Vorlesung,
keine geeignete Klausur stellen zu können, haben dafür jedoch Besucher::innen, die die Präsenz für Fra-
wir, ausgehend von einem ersten Entwurf des Zu- gen oder Kommentare nutzen möchten, denen wir, so
schnitts der Vorlesung, Aufgabenskizzen und eine gut es die Zeit erlaubt, Raum geben.
grobe Festlegung der Proportionen für die Themen- Das Lernziel, eine Übersicht entsprechend der eta-
bereiche erstellt. Vorlesungsinhalte, Klausuraufgaben blierten Lehrbücher zu geben, hat für uns zwei
und Übungsinhalte wurden dann im Sinne eines gu- Teilaspekte. Einerseits den Aspekt der Vermittlung
ten Constructive Alignments (Biggs u. Tang, 2011) auf- von Techniken und Verfahren und andererseits den
einander abgestimmt. Zum Ende der Vorlesungszeit Aspekt „der Mensch steht im Mittelpunkt“ (Ludewig
2015 stand für die Studierenden zur Klausurvorberei- u. Lichter, 2013). Der erste Aspekt ist relativ gut prüf-
tung eine Beispielklausur zur Verfügung, seit 2016 ist
die Beispielklausur mit dem ersten Vorlesungstag auf 3 Im Jahr 2015 wurde in der Evaluation zum Vortragsbesuch
der Lernplattform verfügbar. eine andere, nicht gut vergleichbare Frage gestellt.
4
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 24
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
bar (und kann als Vorbereitung auf die Klausur gese- hen sind. Weiterführende technische Fragen können
hen werden). Zum zweiten Aspekt ist unser Ziel, das konstruiert werden, indem man die gezeigte Problem-
(gesprochene und schriftliche) Kommunizieren von stellung leicht modifiziert und eine erneute Analyse
Softwaretechnik-Problemen und Lösungsideen und erfragt. Bei der Diskussion von Lösungen und weiter-
die Analyse und Bewertung von Lösungsideen ein- führenden Fragen achten die Tutor::innen auf präzise
zuüben. Dieser zweite Aspekt ist ungleich schwerer Sprache, insbesondere die korrekte Verwendung von
prüfbar (und kann als Vorbereitung auf „das echte Softwaretechnik-Fachsprache.
Leben“ gesehen werden) und findet in unserer Veran- Für die schriftliche Darstellung in den Einreichun-
staltung schwerpunktmäßig im Übungsbetrieb statt gen fordern wir regelmäßig die Form „Problem in ei-
(siehe folgender Abschnitt). genen Worten darstellen – eigenen Lösungsvorschlag
formulieren – begründen, argumentieren, im besten
3.3 Übungsaufgaben und Tutorate Falle: beweisen, daß der Lösungsvorschlag das defi-
Die Vorlesung wird von Übungen begleitet. Vor der nierte Problem löst“ und halten die Tutor::innen da-
ersten Vorlesung jedes 3er Blocks steht ein Übungs- zu an, in Kommentaren zu den Einreichungen kon-
blatt zur Verfügung, das direkt nach dieser Vorlesung tinuierlich diese Form nachzufragen.5 Entsprechend
teilweise und nach der zweiten Vorlesung des Blocks sind die (ausgewogen vorkommenden) offenen Mo-
vollständig bearbeitet werden kann, sodaß für jede dellierungsaufgaben absichtlich unpräzise formuliert.
Aufgabe mindestens eine Woche zur Bearbeitung zur Hierbei ist unserer Erfahrung nach der angemesse-
Verfügung steht. Studierende bearbeiten die Aufga- ne Grad an Unschärfe in der Aufgabenstellung im
ben in Teams aus 2 bis 3 Personen und können ihre B. Sc.-Programm signifikant geringer als im M. Sc.-
Bearbeitungen bis zur Minute vor Beginn des Tutori- Programm. Diese absichtliche Unschärfe und die di-
ums auf der Lernplattform einreichen. daktische Absicht kommunizieren wir ganz explizit:
In den Tutorien legen wir Wert auf Interaktion wir gehen (stark) davon aus, daß die allerwenigs-
(i.S.v. (Krusche u. a., 2017)). Das heißt, es sind nicht ten Absolventen in ihrer beruflichen Laufbahn präzi-
die Tutor::innen, die eine Beispiellösung vorstellen, se Aufgabenstellungen bekommen werden — und un-
die „passiv konsumiert“ werden kann („man trifft sich ter dieser Annahme können wir ruhig im 4. Semester
nicht mehr nur, um ‚gemeinsam zuzuhören‘“ (Siege- langsam mit Aufgaben dieser Art beginnen. Im ersten
ris, 2017)),4 sondern der Modus der Tutorien ist „wir Jahr der Veranstaltung gab es in der Evaluation ver-
erarbeiten eine gute Lösung zusammen“ bzw. „wir einzelt Wünsche nach ganz klaren Aufgaben. Unsere
analysieren und bewerten Lösungsvorschläge und Hypothese ist, daß in den meisten vorherigen Veran-
diskutieren weiterführende Fragen“. Die Tutor::innen staltungen präzise Aufgabenstellungen vorherrschen
sehen wir im Tutorium vor allem als Moderator::in, (und den Lernzielen angemessen sind, vgl. auch Ab-
nicht als Vortragende::r. Hierbei sollen die Lösungs- schnitt 4.2) und die ‚Softwaretechnik‘ sich in diesem
wege und -überlegungen transparent werden. Zu die- Aspekt für die Studierenden ungewohnt anfühlt.
sem Zweck sind die Tutor::innen angehalten, für die Am Tag vor den Tutorien führen wir jeweils ein Tu-
technischen Aufgaben (im Sinne des Retrieval-Based- torium für die Tutor::innen durch, vor dem die Tu-
Learning) die Teilnehmer::innen zunächst nach den tor::innen das Übungsblatt selbst skizzenhaft lösen.
relevanten Definitionen zu fragen. Bei kleinen Auf- In diesen Tutors’ Tutorials gehen wir (in der Art der
gaben schreiben die Tutor::innen Lösungsvorschläge Tutorien für die Studierenden) die Aufgaben durch,
aus dem Auditorium auf den Bildschirm, bei größe- diskutieren weiterführende Fragen, legen die Lernzie-
ren Aufgaben bringen die Tutor::innen bemerkens- le der jeweiligen Aufgaben und Fragen dar und geben
werte Lösungen mit ins Tutorium und stellen sie zur Tips zur Moderation. Der Ablauf der Tutorien steht
Diskussion. Die bemerkenswert guten oder eigenarti- danach inklusive Vorschlägen für weiterführende Fra-
gen Lösungen werden aus sogenannten Early Submis- gen und Lernziele als eine Art „Drehbuch“ zur Verfü-
sions ausgewählt. Wir bieten denjenigen Teams, die gung. In der ersten Durchführung hatten wir leich-
24 Stunden vor dem Tutorium Lösungen einreichen, te Sorge, daß sich die Tutor::innen in ihrer gestal-
einen 10 %-Bonus auf die erzielten Zulassungspunk- terischen Freiheit beschränkt fühlen könnten. Hier
te. Beispiele für weiterführende Fragen ergeben sich waren die Rückmeldungen bisher durchweg positiv:
z.B. im Bereich des Requirements Engineering wie ganz im Gegenteil würden die Tutors’ Tutorials Sicher-
folgt. Eine technische Aufgabe kann darin bestehen, heit (z.B. im Zeitmanagement) geben und kognitive
eine gegebene Formalisierung einer Anforderung auf Kapazitäten für tiefer gehende Fragen und Kommen-
(formale) Vollständigkeit zu untersuchen. Ausgehend tare von Seiten der Studierenden freihalten. Weiter-
von der (technischen) Lösung ergibt sich die Frage, hin erreichen wir durch diesen Ansatz eine überwie-
wie das Resultat in der Rolle Requirements Engineer gend gleichbleibende Qualität der Tutorien, unabhän-
zu interpretieren ist und welche Konsequenzen für gig von dem/der konkreten Tutor::in.
die Kommunikation mit der Kundenseite ggf. zu zie-
5 Nicht zuletzt im Interesse der Studierenden: Wir gehen davon
4 Auch wenn einige Studierende sich dies lt. Evaluation wün- aus, daß gut präsentierte Lösungsvorschläge bei der Klausurvorbe-
schen würden. reitung zumindest nicht hinderlich sind.
5
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 25
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
Tabelle 2: Kursinhalte und Struktur.
Vorlesungen Themenbereich Inhaltsübersicht
1 Einleitung Software, Engineering, Software Engineering; Erfolgreiche Softwareent-
wicklung, Empirische Daten zum Erfolg von Softwareprojekten; Aufbau
des Kurses, Bezug zu anderen Lehrveranstaltungen, Organisatorisches.
2–5 Projektmanagement Softwaremetriken, Skalen; Kostenschätzung (Experten- und algorithmi-
sche Schätzung); Projekt, Prozess, Prozess Modellierung; Prozedurmodel-
le; Prozessmodelle (Agil, V-Modell (semi-formal)).
6 – 10 Requirements Engineering Vokabular: Anforderungen, Anforderungsanalyse; Anforderungen im Ent-
wicklungsprozess; Eigenschaften von Anforderungsspezifikationen (Voll-
ständigkeit, Konsistenz, . . . ), Arten von Anforderungen, Analysetechniken;
Dictionary; Spezifikationssprachen für Anforderungen: natürlichsprachli-
che Pattern, Entscheidungstabellen (formal), Use Cases und -Diagramme
(semi-formal), LSCs (formal).
11 – 14 Design & Architektur Modell; Sichten; Strukturmodellierung für Software (Klassen- und Objekt-
diagramme (formal), Proto-OCL (formal)); Designprinzipien; Design Pat-
terns; Verhaltensmodellierung für Software (Communicating Finite Auto-
mata (formal), Query Language (formal)); ein Ausblick zu UML State-
Machines.
15 – 18 Qualitätssicherung Testfall, Testausführung, falsch/richtig positive/negative Ergebnisse (for-
mal); Grenzen des Softwaretestens; Glas-Box-Testen (Anweisungs-,
Verzeigungs-, Term-Überdeckung); Modell-basiertes Testen, Runtime-Veri-
fikation; Programmverifikation (formal), Code Review.
In der auf das Tutorium folgenden Woche geben los an die Diskussion der Begriffe der Modellierung
die Tutor::innen individuelle (für die Klausurzulas- und die Bedeutung von Modellen in der Softwareent-
sung relevante) Bewertungen und Kommentare zu wicklung bereits im ersten Kapitel von (Ludewig u.
den Einreichungen. Hierbei werden die Einreichun- Lichter, 2013) anfügt. In der Diskussion der (gegen-
gen auf zwei verschiedenen Skalen bewertet. Die für über (Ludewig u. Lichter, 2013)) neuen Inhalte bemü-
die Klausurzulassung relevante good-will-Skala be- hen wir uns, dem evidenzbasierten Stil des Lehrbuchs
wertet „sinnvolle Bearbeitung“ relativ zum Wissen zu folgen, also rationale Wertungen zu ermöglichen
der Studierenden vor dem Tutorium. Hier interpre- und soweit möglich die (ursprünglichen) Quellen an-
tieren die Tutor::innen unklare Formulierungen im zugeben. Entsprechend zeigen wir anhand von Bei-
Zweifel zugunsten der Studierenden. Um einen Ein- spielen, was Formale Methoden konkret leisten kön-
druck von der Bewertung in der Klausur zu geben, be- nen, was ihre Fürsprecher::innen versprechen und
werten wir außerdem jede Aufgabe auf der evil-Skala, welche Kritik vorgebracht wird, sodaß die Studieren-
die sich am Punkteschema der Klausur und am Wis- den Vor- und Nachteile verantwortlich und kontext-
sen nach dem Tutorium orientiert, insbesondere dar- abhängig abwägen können.
über, wie bestimmte Aufgabenstellungen im Kontext
der Veranstaltung im Zweifel zu interpretieren sind. Tabelle 2 gibt einen Überblick über die Inhalte
Hier werden unklare Formulierungen oder Fehler in der Vorlesung. Wir beginnen mit dem Themenbereich
der Syntax zuungunsten der Studierenden gewertet. Projektmanagement, da die Inhalte dieses Bereichs
für die Teilnehmer::innen des parallel im 4. Semes-
4 Formale Methoden in der ter stattfindenden Software-Praktikums (SoPra) für
B. Sc.-Studierende nützlich sein können. Es gibt von
Softwaretechnik-Vorlesung Seiten der Teilnehmer::innen durchaus den Wunsch
Für die Darstellung von Vokabular, Problembereichen nach einer Abstimmung zwischen dem SoPra und
und nicht formalen Inhalten folgt unsere Vorlesung der ‚Softwaretechnik‘, der aus verschiedenen Grün-
im Wesentlichen dem Lehrbuch (Ludewig u. Lichter, den nicht praktikabel (und, da das SoPra eine in sich
2013). Wir schätzen an diesem Lehrbuch die expli- abgeschlossene Veranstaltung mit eigenen Vorlesun-
zit adressierte Sicht, „dass sich Software-Engineering gen ist, auch nicht notwendig) ist. Ein Grund ist, daß
vor allem mit den Menschen befasst, die Software in im SoPra bereits in der dritten Woche die Spezifika-
Auftrag geben, entwickeln und ändern oder benut- tion und ein Architekturentwurf abzugeben sind. Ein
zen“ und das u.E. sehr gelungene „[B]emühen [...] weiterer Grund ist, daß in jedem Jahr über 30 % der
um eine rationale Wertung“ und darum, „alle Quel- ‚Softwaretechnik‘-Teilnehmer::innen das SoPra nicht
len [...] vollständig anzugeben“. in ihrem Studienplan haben und Versuche einer en-
Im folgenden beschreiben wir unsere Erweiterung geren Abstimmung bei diesen Teilnehmer::innen zu
der Inhalte um formale Modelle in der Softwareent- signifikanten Verwirrungen geführt haben. Als Kom-
wicklung, die sich unserer Wahrnehmung nach naht- promiss haben einige Übungsaufgaben einen Bezug
6
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 26
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
zum SoPra, der sich den SoPra-Teilnehmer::innen er- Wir nutzen bei der Auswahl der Inhalte die re-
schließt, und für die anderen Studierenden einfach lative späte Lage der Veranstaltung im Studienplan
„ein Beispielprojekt“ ist. aus (vgl. Abschnitt 2). So bauen wir auf ‚Grundla-
In der Präsentation und Diskussion der nicht- gen der Theoretischen Informatik‘, die Mathematik-
formalen Inhalte folgen wir (Ludewig u. Lichter, Vorlesungen und ‚Rechnerarchitektur‘ auf, in denen
2013), wobei wir im Zweifel direkt auf die ursprüng- die Studierenden bereits mit verschiedenen Forma-
lichen Quellen zurückgreifen, z.B. die Normtexte IE- len Methoden konfrontiert wurden (wenn auch viel-
EE 601.12 und ISO 24765 für Vokabular und IE- leicht nicht unter diesem Namen). Unsere Veranstal-
EE 830 zur Struktur von Anforderungsdokumenten. tung zeigt gewissermaßen, wie ein großer Teil des
In den folgenden Abschnitten geben wir einen Über- bisher Gelernten in der Softwarekonstruktion ange-
blick über die von uns ergänzten formalen und semi- wandt werden kann.
formalen Inhalte.
4.1 Themenbereich
Aufgrund unserer in der Einleitung ausgeführten
Softwareprojektmanagement
Beobachtung eines Mangels an geeigneten Lehrbü-
chern, haben wir die formalen Inhalte selbst ausge- Im Themenbereich Softwareprojektmanagement
wählt bzw. konstruiert. Der Überarbeitung der Veran- überwiegen nicht-formale Inhalte (vgl. Tabelle 2).
staltung lag die Hypothese zugrunde, daß es durch ei- Ein Schwerpunkt sind Softwaremetriken als ein
ne angemessene Reduktion des Sprachumfangs mög- Aspekt der ingenieurmäßigen, objektivierten Soft-
lich ist z.B. die formale Spezifikationssprache für wareentwicklung (inklusive des Bewusstseins für
Strukturaspekte OCL vollständig definiert einzufüh- Pseudometriken (vgl. (Ludewig u. Lichter, 2013))).
ren und die Idee Formaler Methoden und Analysen Ein weiterer Schwerpunkt ist die Prozessmodellie-
zu vermitteln, und gleichzeitig der Vermittlung der rung. Hier führen wir zunächst eine semi-formale7
etablierten nicht-formalen Inhalte einen angemesse- graphische Beschreibungssprache für Prozesse ein,
nen Raum zu geben. Bei der Auswahl der Teilspra- bestehend aus Rollen, Artefakten, Aktivitäten und
chen von z.B. OCL stand das Ziel im Vordergrund, den entsprechenden Relationen. Wie zeigen, wie
die formalen Sprachen nicht artifiziell zu vereinfa- ein konkreter Ablauf (oder Prozess) einer Softwa-
chen, sondern echte Teilsprachen auszuwählen, die reentwicklung modelliert werden kann (deskriptiv,
in Spezialvorlesungen konservativ erweitert werden. Abbild), um dann zu zeigen, wie ein graphisches Pro-
Wir konnten hierbei auf eine langjährige Erfahrung zessmodell präskriptiv (Vorbild) verwendet werden
aus Forschungs- und Projektarbeit sowie aus unse- kann, um Prozessabläufe vorzugeben. Wir verwen-
ren Spezialvorlesungen ‚Software, Design, Modelling, den unsere graphische Beschreibungssprache, um
and Analysis in UML‘ (UML) und ‚Real-Time Sys- konkrete Prozedur- und Prozessmodelle (Wasserfall,
tems‘ im M. Sc. Informatik zurückgreifen, in denen V-Modell, XP, Scrum) vorzustellen bzw. setzen die
für die Modellierungssprachen jeweils eine vollständi- Notation z.B. der V-Modell-Beschreibung zu unserer
ge konkrete und abstrakte Syntax sowie eine forma- Teilsprache in Beziehung.
le Semantik eingeführt wird. In der UML-Vorlesung In den Übungsaufgaben ist anhand von vorgegebe-
sind dies Klassen- und Objektdiagramme, OCL, State- nen Prozessbausteinen ein kleines Entwicklungspro-
Machines und Sequenzdiagramme. jekt zu planen inklusive Besetzung von Rollen mit Per-
Bei der Auswahl der Beispiele in der Vorlesung und sonen. Um die Tutor::innen insbesondere auf Fragen
der Konstruktion der Übungsaufgaben greifen wir so- und Diskussionen zur Verwendung und zum Nutzen
weit möglich auf reale, industrielle Softwareprojekte von Prozessmodellen vorzubereiten, haben wir ent-
(bestenfalls aus unserer eigenen Erfahrung) zurück, sprechend des Prinzips „lehren, was wir praktizieren“
da so sichergestellt ist, daß wir Nachfragen in belie- in 2018 den Prozess des Übungsbetrieb vollständig
biger Detailtiefe zufriedenstellend beantworten kön- modelliert. Die Erläuterung des Prozesses ist aufwen-
nen.6 Dabei verwendet die Vorlesung für die verschie- dig, dafür weiß über das gesamte Semester jede::r
denen Formalen Methoden verschiedene Beispiele an Tutor::in, wer wann welches Artefakt wie zu bearbei-
denen sich die spezifischen Stärken zeigen. Wir möch- ten hat und wir können unsere ganze Aufmerksam-
ten (und können redlicherweise) nicht den Eindruck keit den eingereichten Lösungsvorschlägen widmen.
erwecken, daß der Stand der Technik der Formalen
4.2 Themenbereich
Methoden ist, ein Softwaresystem vollständig und
Requirements Engineering
durchgängig konsistent formal zu beschreiben. For-
male Methoden sind dann effektiv, wenn geeignete Der Themenbereich Requirements Engineering (RE)
Formalismen zur Beschreibung und Analyse spezifi- ist in der Veranstaltung etwas stärker gewichtet als
scher, besonders kritischer oder komplexer Aspekte die weiteren Themenbereiche (vgl. Tabelle 2). Dies
von Software mit Bedacht eingesetzt werden. ist vor allem drei Überlegungen geschuldet. Erstens
stimmen wir zu (etwa (Sedelmaier u. Landes, 2017)),
6 Dies ist bei artifiziell konstruierten Beispielen ungleich schwe-
rer herzustellen und kann, wenn es nicht gelingt, unnötige Unzu- 7 d.h. präzise konkrete Syntax, informelle Beschreibung der Be-
friedenheit auf Seiten der Studierenden hervorrufen. deutung.
7
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 27
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
daß dem Themenbereich RE in der Softwareentwick- ist, eine für alle Beteiligten gute Beispiellösung zu er-
lung eine besondere Relevanz zukommt. Die Rele- arbeiten. Unser Kunde ist ein Organisator des SoPra,
vanz wird dabei in den späteren Themenbereichen unsere Anforderung war in 2018 der oben genannte
sehr natürlich aufgegriffen: Der Begriff der Korrekt- Satz. Die Aufgabe besteht darin, durch Kommunika-
heit von Softwareentwürfen (insbesondere bzgl. des tion mit dem Kunden ein Begriffslexikon zu erarbei-
Verhaltens) und von Software ist relativ zu einer An- ten und die nicht im Satz enthaltenen Informationen
forderung. Etwa ein Algorithmus kann nur als korrekt „herauszukitzeln“. Um die Aufgabe skalierbar zu ge-
(bzgl. einer Anforderung) bewiesen werden, wenn stalten, führen zunächst die Organisatoren unserer
es eine formale Beschreibung der Anforderung gibt. Veranstaltung eine Anforderungsanalyse durch und
Zweitens beobachten wir, daß die Vermittlung von notieren die Findungen in einem Wiki. Die Studieren-
Problemen und Techniken des RE für Studierende mit den kommunizieren mit dem (für sie anonymen) Kun-
wenig oder keiner Vorerfahrung eine besondere Her- den per Mail, vermittelt durch die Tutor::innen. Mit
ausforderung darstellt (vgl. Selbsteinschätzung der Hilfe des Wiki können die Tutor::innen die meisten
Studierenden, Abschnitt 2). Drittens führen wir in un- Fragen ihrer Tutanden schon im Stile eines Kunden
serer Veranstaltung im Themenbereich RE zum ers- beantworten, noch unklare Aspekte werden an den
ten Mal Formale Methoden ein. SoPra-Organisator weitergeleitet und im Wiki nach-
Wir sprechen bei unseren Diskussionen i.d.R. über geführt; weiterhin sind die Tutor::innen angehalten,
die u.E. besonders herausfordernde Situation eines die Kommunikation in der Art eines Coaches zu be-
Softwareentwicklungsvertrages zwischen getrennten obachten und Tips für weitere Fragen zu geben. Für
Kunden- und Entwicklungsunternehmen. Die Softwa- das Tutorium bereiten wir eine Liste von bekannten
reentwicklung in Start-Ups, innerhalb einer Abtei- Beispielspielen vor, die die Anforderung lt. Kunde er-
lung oder zwischen Abteilungen desselben Unterneh- füllen bzw. nicht erfüllen. Im Tutorium sollen die Teil-
mens hat ggf. andere Rahmenbedingungen. nehmer::innen durch Handzeichen pro Beispiel anzei-
Bei der Vermittlung von Problemen und Techniken gen, ob nach ihrer konkreten Anforderungsanalyse
des RE arbeiten wir mit zwei (bisher leider nicht das Beispiel vom Kunden akzeptiert oder abgelehnt
empirisch belegten) Hypothesen zu Ursachen von wird bzw. ob sie sich nicht sicher sind. In 4 Jahren
Schwierigkeiten. Eine Ursache sehen wir darin, daß Durchführung dieser Übung hat noch nicht ein Team
der weitaus überwiegende Teil der Übungsaufgaben, alle Beispiele korrekt klassifiziert; dies wird durch das
die die Studierenden bis zum 4. Semester bearbei- Verfahren mit den Handzeichen im Tutorium unmit-
ten, von Fachleuten in Fachsprache präzise formu- telbar für die Studierenden erfahrbar.
liert sind (nicht zuletzt, um die Korrektur zu vereinfa- In der Einführung der Problemstellung der An-
chen). Entsprechend stellen wir Übungsaufgaben zu forderungsanalyse und nicht-formalen Beschreibung
unserer Veranstaltung absichtlich unpräzise und hal- von Anforderungen folgen wir (Rupp u. a., 2014).
ten dazu an, in den Einreichungen zunächst die Auf- Wir beginnen die Diskussion von Beschreibungsspra-
gabenstellung in eigenen Worten wiederzugeben (vgl.
chen am nicht-formalen Ende der in Abbildung 1(b)
Abschnitt 3.3). Als zweite Ursache vermuten wir, daß dargestellten Achse mit der natürlichsprachlichen Be-
der Umgang mit Sprache im Alltag von dem in der schreibung und Sprach-Patterns (Rupp u. a., 2014)
RE-Arbeit verschieden ist. Im Alltag sind Menschen
und diskutieren Eigenschaften guter Anforderungsdo-
üblicherweise gern bereit, einen Satz wie: kumente wie Vollständigkeit. Die Präsentation wech-
Spielfiguren müssen indirekt gesteuert werden. selt dann ans formale Ende der Achse und dort
zu einem möglichst einfachen Formalismus (vgl. Ab-
direkt als „klar“ zu akzeptieren und keinen Bedarf schnitt 4.2.1), um dann im semi-formalen Bereich
für Nachfragen zu sehen (fehlende Information wird z.B. User Stories und Use Cases einzuführen. Ein kom-
plausibel aufgefüllt; man sieht nur Information). In plexer Formalismus (vgl. Abschnitt 4.2.2) und ein
der RE-Arbeit geht es unseres Erachtens beim Blick Rückblick schließen den Themenbereich ab.
auf den obigen Satz vor allem darum, zu sehen, wel-
4.2.1 Entscheidungstabellen
che Information der Satz nicht enthält.
Um diesen Sichtwechsel anzuregen, führen wir Als Einstieg in die formale Beschreibung von Anfor-
eine Übung durch, in der die Studierenden eine derungen haben wir als eine möglichst einfache Spra-
textuell gegebene Anforderung analysieren. Diese che die in vielen Lehrbüchern semi-formal eingeführ-
Übung wird in verschiedenen Ausprägungen im RE- ten Entscheidungstabellen (ET) ausgewählt. ET sind
Unterricht eingesetzt, etwa mit Paaren von studenti- eine der einfachsten Beschreibungssprachen, die mit
schen Teams, die jeweils die Kunden- bzw. Entwickler- formaler Semantik und Analysen versehen werden
rolle übernehmen oder mit nicht technisch vorgebil- können, sind jedoch weder trivial noch eine artifi-
deten (echten) Kunden. Wir verwenden eine Varian- zielle Lehrsprache. Die schlichten Sprachmittel von
te mit einem technisch vorgebildeten Kunden, da wir ET reichen vollständig aus, um Anforderungen zu be-
in den anderen Szenarien die Gefahr sehen, daß die schreiben, die in textueller Form sehr schnell nicht
Parteien aneinander vorbeireden und es aufwendig mehr überblickbar, wartbar oder analysierbar sind.
8
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 28
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
T : decision table r1 ··· rn ET die wichtige Diskussion, wie sich z.B. die formale
c1 description of condition c1 v1,1 v1,n
.. .. ..
···
..
Vollständigkeit einer ET zur vollständigen Erfassung
..
. . . . . einer Anforderung im Sinne von (Rupp u. a., 2014)
cm description of condition cm vm,1 ··· vm,n verhält. Eine Analyse einer formalen Beschreibung
a1 description of action a1 w1,1 w1,n
.. .. ..
···
..
bzgl. einer Eigenschaft wie Vollständigkeit kann po-
..
. . . . . sitiv (Eigenschaft nicht gegeben) oder negativ aus-
ak description of action ak wk,1 ··· wk,n fallen und dieses Ergebnis kann (wie Testresultate)
falsch oder richtig sein. Ein Grund für ein falsch-
Abbildung 2: Konkrete Syntax von ET.
positives Resultat kann z.B. ein simpler Schreibfeh-
ler beim Verfassen der formalen Beschreibung sein.
Formal ist eine ET T über disjunkte Mengen von Be- Ein positives Resultat liefert jedoch in jedem Fall ein
dingungen C und Aktionen A eine n × m-Matrix (sie- Indiz dafür, daß uns z.B. in der Anforderungserfas-
he Abbildung 2) wobei c1 , . . . , cm ∈ C, a1 , . . . , ak ∈ sung ein Fehler unterlaufen ist und dieses Indiz ist
A, v1,1 , . . . , vm,n ∈ {−, ×, ∗}, und w1,1 , . . . , wk,n ∈ im Zweifel zusammen mit den Kunden zu klären. Für
{−, ×}. Eine wohlgeformte ET hat einen Namen. ET liefern die Werkzeuge im positiv-Fall sogar alle Be-
Spalten (v1,i , . . . , vm,i , w1,i , . . . , wk,i ), 1 ≤ i ≤ n, wer- obachtungen, die in T nicht berücksichtigt werden,
den Regeln genannt und haben einen eindeutigen Na- und die sich üblicherweise gut in die Begriffs- und Er-
men (hier: r1 , . . . , rn ). Die Vektoren (v1,i , . . . , vm,i ) fahrungswelt der Kunden übersetzen und als solche
und (w1,i , . . . , wk,i ) heißen Prämisse und Effekt von klären lassen. Die Formalisierung einer Anforderung
Regel ri . Die Semantik einer ET T ist durch die Funk- und die formale Analyse kann also sicherstellen, daß
tion F gegeben, die jeder Regel r in T eine Formel alle Probleme, die zu positiven Resultaten führen, er-
der propositionalen Logik über C und A wie folgt zu- kannt und ggf. ausgeräumt werden. Die formale Ana-
ordnet. Seien (v1 , . . . , vm ) und (w1 , . . . , wk ) Prämisse lyse kann nicht sicherstellen, daß die Anforderungs-
und Effekt von r. Dann ist analyse als solche vollständig ist, da falsch-negative
Resultate möglich sind. Ob der Aufwand der Formali-
V V
F (r) := sierung und Analyse von Anforderungen oder Design-
1≤i≤m F (vi , ci ) ∧ 1≤j≤k F (wj , aj ) (1)
| {z } | {z } ideen das verringerte Fehlerrisiko rechtfertigt, ist je
=:Fpre (r) =:Feff (r) nach Projektkontext zu entscheiden.
Die Übungsaufgaben zu ET umfassen verschiedene
mit F := {(×, x) 7→ x, (−, x) 7→ ¬x, (∗, x) 7→
formale Analysen von gegebenen ET sowie eine Auf-
true}. Die Teilformeln Fpre (r) und Feff (r) heißen
gabe, in der ein Transkript eines Kundeninterviews
Prämissen- bzw. Effektformel.
(mit absichtlichen Redundanzen und Mehrdeutigkei-
Eine ET kann wie folgt zur Formalisierung einer
ten) im Umfang von ca. einer DIN-A4-Seite in eine
Anforderung der Art, daß Systemverhalten in akzep-
ET mit ca. 10 Regeln über jeweils 5 Bedingungen und
tabel (oder erwünscht) und unerwünscht klassifiziert
Aktionen überführt werden soll. Im Tutorium stellen
wird, verwendet werden. Ein System erfüllt die durch
wir die (provokante) Frage: Nehmen wir an, man
ET T gegebene Anforderung genau dann, wenn je-
müsste als Implementierer::in des Kundenwunsches
des beobachtbare Systemverhalten durch eine Regel
zwischen Text und ET als Spezifikation wählen, was
in T erlaubt wird. Formal kann eine Beobachtung ei-
wäre die Wahl? Und warum? Meiner Kenntnis nach
nes Systems bzgl. der Bedingungen und Aktionen in
hat sich in den 4 Jahren der Veranstaltung noch nie-
C und A, also welche Bedingungen aus C erfüllt sind
mand ausdrücklich den Text gewünscht. Hier versu-
und welche Aktionen aus A ausgeführt werden, als
chen wir, einen Aspekt sichtbar zu machen, der unse-
Boole’sche Belegung σ : C ∪ A → {0, 1} der logischen
rer Meinung nach im Kontext formaler Beschreibun-
Variablen in C ∪ A notiert werden. Die Beobachtung
gen noch vor der Anwendung von formalen Analy-
σ erfüllt T genau dann, wenn es eine Regel r in T
sen steht. Eine formale Beschreibung einer Anforde-
gibt, sodaß σ |= F (r).
rung hat den Effekt, daß (mit hoher Wahrscheinlich-
Begriffe wie Vollständigkeit können für ET präzise keit) alle im verwendeten Formalismus ausgebildeten
definiert werden, z.B. nennen wir eine ET T (formal) Softwaretechniker::innen zu jeder Zeit dieselbe Infor-
vollständig, wenn die Disjunktion der Prämissenfor- mation sehen.8 So sehen wir formale Beschreibun-
meln von T eine Tautologie ist. Das Problem der Ana- gen zuvorderst als Werkzeug, um auf Seiten der Soft-
lyse auf (formale) Vollständigkeit kann auf das Erfüll- waretechniker::innen das Risiko von Missverständnis-
barkeitsproblem propositionaler Logik reduziert wer- sen zu verringern. Als Analogie verwenden wir z.B.
den, für das in Form von sogenannten SAT-Solvern von Jurist::innen konstruierte Individualverträge, de-
Entscheidungswerkzeuge zur Verfügung stehen. ren Konsequenzen man als Nicht-Jurist üblicherwei-
In der Vorlesung ‚Softwaretechnik‘ diskutieren wir se nicht überblicken kann. Man hat als Auftragge-
nun nicht eine Reduktionsprozedur oder die Kon- ber des Individualvertrags jedoch den Anspruch, von
struktion von SAT-Solvern, sondern nehmen eine Nut-
zersicht ein, nehmen also zur Kenntnis, daß Werkzeu- 8 Gestandene Praktiker::innen berichten, daß es vorkommt, daß
ge dieser Art existieren. Wir führen am Beispiel der dieselbe Person am selben Tag einen Text verschieden interpretiert.
9
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 29
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
der Fachperson eine „Übersetzung“ zu erhalten bzw. 4.3 Themenbereich Entwurf
darauf, wichtige Szenarien gemeinsam durchzuspie- Im Themenbereich Softwarearchitektur und Entwurf
len. Ebenso hat man als Softwarekunde einen An- liegt der Schwerpunkt auf der Modellierung der
spruch, von den Entwickler::innen deren z.B. in for- Struktur und des Verhaltens von Softwaresystemen
maler Form notiertes Verständnis der Anforderun- als Baupläne im Sinne von (Lamport, 2015). Zur
gen erklärt zu bekommen. Dies kann insbesondere Strukturmodellierung führen wir eine übersichtliche
durch Szenarien gelingen (vgl. (Arenis u. a., 2016)). Teilsprache der Klassendiagramme von UML ein, die
Für jedes von dem/der Kund::in formulierte Szena- im wesentlichen Klassen mit Attributen von Basisty-
rio können Entwickler::innen auf Basis der formalen pen und gerichteten Assoziationen der Multiplizitä-
Beschreibung Auskunft geben, ob ihrem Verständnis ten 0,1 und 0,∗ mit Ownership umfasst.Neben der be-
nach dieses Szenario erwünscht oder unerwünscht kannten Sicht, Klassendiagramme als Visualisierung
ist. Bei Verwendung formaler Beschreibungen ist die- von (Klassen in) Programmen zu betrachten, beto-
se Auskunft objektiv und beliebig reproduzierbar. nen wir die Sicht eines abstrakten (von der Pro-
Die Klausur umfasst Aufgaben verschiedener Taxo- grammierung zunächst unabhängigen) Strukturmo-
nomie-Stufen zu ET, vom Beweis z.B. der Vollstän- dells. Die abstrakte Syntax eines Klassendiagramms
digkeit einer ET, über die Analyse einer gegebenen ist eine Signatur mit Klassen, Basis- und abgeleiteten
ET auf Konsistenz bis hin zur Erstellung einer klei- Typen, und je Klasse der Menge der Attribute dieser
nen ET zu einem Text. Die Ergebnisse (vgl. (Westphal, Klasse. Die Semantik eines Klassendiagramms ist die
2018)) sind sehr erfreulich. Den gesamten Aufgaben- Menge der über dieser Signatur bildbaren System-
bereich lösten in 2015 bis 2017 mehr als 50 % der zustände (OMG, 2006), d.h. partiellen Funktionen,
Teilnehmer::innen mit 14 bzw. 13 von 15 Punkten, die (einige) Objektidentitäten auf jeweils eine Bele-
liegen also im guten oder sehr guten Bereich, obwohl gung der Attribute mit Werten abbilden. Systemzu-
wir die Analyseaufgabe klar den „schweren“ Aufga- stände können graphisch (ohne Informationsverlust)
ben der Klausur zuordnen. Die Grenze zum unteren durch vollständige Objektdiagramme dargestellt wer-
Quartil liegt bei erfreulichen 12,5 bzw. 12 Punkten. den. Hier stellen wir die Anwendung von Objektdia-
4.2.2 Live Sequence Charts grammen in der Dokumentation und Spezifikation
Als komplexen Formalismus (mit höherer Ausdrucks- heraus. Wenn der Aufwand, bestimmte Annahmen
stärke und Informationsdichte, und höherem Auf- einer Datenstruktur z.B. mit OCL zu formalisieren,
wand zur Definition von (abstrakter) Syntax und Se- in einem Projekt als zu hoch bewertet wird, kann
mantik) haben wir Live Sequence Charts (Damm u. eine geeignete Auswahl von Objektdiagrammen her-
Harel, 2001) (LSCs) ausgewählt, eine formale Vari- vorragend zur Spezifikation dieser Annahmen „durch
ante der weit verbreiteten Sequenzdiagramme. Wir Beispiel“ verwendet werden. Wenn etwa eine Listen-
führen die Automatensemantik für LSCs nach (Klo- struktur nur unter der Annahme verwendet werden
se u. Wittke, 2001) ein, inklusive Chart-Modus, Cold darf, daß keine Zyklen konstruiert werden.
Conditions, und Pre-Charts. Ein System erfüllt eine Eigenschaften von Strukturen können mit Hilfe der
(universelle) LSC genau dann, wenn alle Berechnun- Object Constraint Language (OCL) formalisiert wer-
gen des Systems von dem aus der LSC konstruier- den. Hier führen wir Proto-OCL ein, eine Teilspra-
ten Automaten akzeptiert werden. Weiterhin führen che der OCL, deren konkrete Syntax sich an der den
wir aus, wie LSCs (bzw. ihre Automaten) in der auto- Studierenden vertrauten Form der Logik erster Stufe
matischen Testdurchführung verwendet werden kön- orientiert. Die Semantik von Proto-OCL ist eine In-
nen (Klose u. Lettrari, 2001). terpretationsfunktion, die eine gegebene Proto-OCL-
Die Klausur umfasst Aufgaben zur Konstruktion Formel und einen gegebenen Systemzustand (oder
der Automaten sowie erfragt Beispiele für akzeptier- ein vollständiges Objektdiagramm) auf einen der drei
te bzw. nicht akzeptierte Systemberechnungen. Nicht (!) Werte true, false und ⊥ abbildet. Wir stellen die
zuletzt da die Einführung von LSCs den technisch an- Besonderheiten heraus, daß OCL Assoziationen ver-
spruchsvollsten Teil unserer Vorlesung darstellt, se- schiedener Multiplizität verschieden behandelt sowie
hen wir diese Aufgaben im „mittleren“ und „schwe- die Bedingungen, unter denen man eine Auswertung
ren“ Bereich, der am Ende die guten und sehr guten zum dritten Wahrheitswert beobachten kann.
Gesamtnoten entscheidet. Mit den Resultaten sind Für die konstruktive Modellierung von Verhalten
wir auch hier zufrieden, das untere Quartil endet bei führen wir eine einfache Teilsprache von State-
8,5 bzw. 7 von 15 bzw. 16 Punkten, das obere Quartil Machines ein. Unsere Communicating Finite Automa-
beginnt bei 13 bzw. 12 Punkten. ta (CFA) sind im Wesentlichen nicht-hierarchische
Im ersten Jahr waren wir von den guten Ergebnis- State-Machines mit Rendezvous-Synchronisation,
sen bei aller Zuversicht positiv überrascht. Wir hatten d.h. zwei Kanten in verschiedenen Automaten
uns vereinzelt vorgetragenen Sorgen, daß die LSC- können eine Transition begründen, wenn je eine
Semantik zu schwer sein könnte, nicht völlig entzie- der Kanten bzgl. eines Events sende- bzw. emp-
hen können und entsprechend Vorsorge getragen, die fangsbereit ist. Dieses Synchronisationsparadigma
Aufgaben zu LSCs ggf. aus der Wertung zu nehmen. ist mit durch State-Machines implementierten
10
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 30
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
Behavioural Features in UML vergleichbar jedoch ment von Soll ist. Hier betonen wir ((Ludewig u. Lich-
nicht (ohne weitere Annahmen) identisch. Zu dieser ter, 2013) folgend) besonders den Aspekt, daß die
Abweichung von der UML-Semantik haben wir uns Begriffe des positiven und negativen Tests relativ zu
vorrangig aus zwei Gründen entschieden. Einerseits Soll-Werten (die sich ggf. aus (formalen) Anforderun-
erfordert die formale Einführung des abstrakten gen ableiten lassen) definiert sind. Die Resultate der
Event-Speichers (in der die UML-Semantik be- Klausuraufgaben zum Testen sind durchweg ordent-
kanntlich parametrisiert ist) sowie einer konkreten lich, jedoch sind wir jedes Jahr wieder überrascht,
Ausprägung, etwa einer empfängerseitigen FIFO- daß eine signifikante Anzahl der Studierenden keine
Queue, wie sie IBM Rhapsody verwendet, in unserer Soll-Werte angibt, obwohl explizit nach einer erfolglo-
UML-Veranstaltung ca. 2 Vorlesungen. Der Erkennt- sen Test-Suite gefragt wird.
nisgewinn im Vergleich zum Aufwand erscheint uns Als gegenüber den etablierten Lehrbüchern neu-
für eine Softwaretechnik-Veranstaltung zu gering. en Inhalt präsentieren wir Programmverifikation
Andererseits steht mit Uppaal (Larsen u. a., 1997) nach (Hoare, 1969) in der Form des Lehrbuchs (Apt
ein Werkzeug zur Erstellung, Simulation und Verifi- u. a., 2009). Für die Übungen verwenden wir das
kation von (insbesondere)9 CFAs mit einer reichen Web-Interface des Verifying C Compilers (Cohen u. a.,
Programmiersprache für Guards und Aktionen zur 2009) (VCC) und diskutieren als weiterführende Fra-
Verfügung, das nicht zuletzt aufgrund seines sehr gut gen den Unterschied zwischen der Verifikation eines
auf das Wesentliche reduzierten User-Interfaces10 Algorithmus und der Verifikation eines C-Programms
hervorragend für unsere Ziele geeignet ist.11 unter Annahmen über die Ausführungsplattform. Die
Die Übungsblätter zu CFA umfassen Aufgaben zur Klausuraufgabe besteht üblicherweise darin, eine ge-
Erstellung eines Modells eines verteilten Algorithmus gebene Beweisskizze mit den verwendeten Axiomen
für Mutual-Exclusion (das den Teilnehmer::innen als und Beweisregeln zu annotieren. Hier erreicht das
Problem aus der Betriebssysteme-Vorlesung bekannt obere Quartil zwischen 5,5 und 7 von 7 Punkten, das
sein müsste), zur Simulation verschiedener Abläu- untere Quartil endet bei 3 bis 5 Punkten.
fe und zur Verwendung von Uppaal’s Temporallogik
(Query Language) zur Spezifikation und Verifikati- 5 Lehrevaluation
on der Mutual-Exclusion-Eigenschaft. Mit den Übun- Da die Veranstaltung neu konstruiert wurde, beob-
gen verfolgen wir insbesondere das Ziel, das mäch- achten wir seit der ersten Durchführung verschiedene
tige Modellierungskonzept des Nichtdeterminismus Metriken (vgl. Abschnitt 4.1) auf Indizien für Fehlent-
und die durch nebenläufiges Verhalten induzierten wicklungen. Daten beziehen wir aus dem Übungsbe-
Schwierigkeiten sichtbar zu machen. trieb, den Klausuren und der zentralen Evaluation.
In der Klausur ist üblicherweise der Transitions- In der Evaluation beachten wir besonders die
graph eines gegebenen Systems von mehreren CFAs Aspekte „Workload“ und „Niveau“ (Uttl u. a., 2017)
zu erstellen. Mit den Ergebnissen sind wir durchweg und die Freitexte. Den Workload sehen über alle
zufrieden, der Median liegt zwischen 10 und 12,25 4 Jahre gesehen rund 62 % der Studierenden als ‚mit-
von 13 Punkten, das obere Quartil beginnt zwischen tel‘ und rund 30 % als ‚hoch‘, das Niveau sehen rund
12 und 13 Punkten, liegt also im sehr guten Bereich. 62 % als ‚angemessen‘ und rund 29 % als ‚hoch‘. Dies
4.4 Themenbereich Qualitätssicherung entspricht vollständig unserem Ziel für eine universi-
täre Lehrveranstaltung.
Im Themenbereich Qualitätssicherung betrachten wir
Den Lernerfolg bzgl. des Lernziels der Vermittlung
speziell die Prüfung von Programmcode. Hier disku-
von Methoden und Techniken messen wir anhand der
tieren wir zunächst die Disziplin des Softwaretestens.
Klausurergebnisse, mit denen wir über alle 4 Jahre
Dem formalen Charakter der gesamten Veranstaltung
sehr zufrieden sind. Das viel interessantere Lernziel
folgend, führen wir Testfälle als Paare (In, Soll) aus
der Vorbereitung auf das „echte Leben“ läßt sich lei-
einer (Menge von) Eingabe(n) und Soll-Wert(en) ein.
der notorisch nicht gut messen. Als ein positives In-
Eine Ausführung eines Testfalls ist eine Beobachtung
diz sehen wir unsere und von Kolleg::innen berichte-
des Systems, die Eingaben entsprechend In erhält,
te Erfahrung aus Vorgesprächen zu individuellen Pro-
was ein einzelner Wert oder eine Sequenz von z.B.
jekten wie etwa B. Sc.-Arbeiten. Hier nehmen wir die
Events sein kann. Ein Test ist negativ (Test passed) ge-
Inhalte der Vorlesung als (angestrebten) soliden Be-
nau dann, wenn die betrachtete Beobachtung ein Ele-
zugspunkt wahr, um über spezialisierte Aufgabenstel-
9 Daß Uppaal für CFAs mit Uhrenvariablen, also Timed Automa- lungen zu sprechen. Wir hoffen, daß sich die Veran-
ta, entwickelt wurde, verschweigen wir schlankerhand. staltung ebensogut als Bezugspunkt für den Einstieg
10 Aus denselben Überlegungen führen wir kein Werkzeug zur
in die berufliche Karriere der Studierenden eignet.
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 6 Zusammenfassung
den Absichten z.B. unserer Übungen (vgl. (Glinz, 1996)).
11 Einige Teilnehmer::innen unserer UML-Veranstaltung, in der Formale Methoden werden zunehmend in vielen
wir IBM Rhapsody verwenden, vermissen die mächtige und leicht Bereichen der Softwaretechnik angewandt. Unserer
zu bedienende Simulationsfunktion von Uppaal. Überzeugung nach ist es hilfreich, wenn die Bedeu-
11
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 31
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
tung formaler Beschreibungen vollständig durchdrun- [Glinz 1996] G LINZ, M.: The Teacher: “Concepts!”
gen wird und die aus formalen Analysen zu ziehen- The Student: “Tools!”. In: Softwaret.-Trends 16
den Schlüsse verstanden werden. (1996), Nr. 1
Unsere Erfahrung zeigt, daß es möglich ist, eine
Veranstaltung zur Einführung in die Softwaretechnik [Hoare 1969] H OARE, C. A. R.: An axiomatic basis
im Grundstudium um genau diese Aspekte zu ergän- for computer programming. In: CACM 12 (1969),
zen ohne hierbei die Inhalte der etablierten Lehrbü- Nr. 10, S. 576–580
cher zu vernachlässigen. [IEEE 1990] IEEE: Standard Glossary of Software En-
Danksagungen. Wir danken Sergio Feo Arenis und gineering Terminology, 1990. – Std 610.12-1990
Christian Schilling für ihre Unterstützung als Assistenten
[IEEE 1998] IEEE: Recommended Practice for Softwa-
der ersten beiden bzw. des letzten Jahres. Ohne die Ge-
re Req. Specifications, 1998. – Std 830-1998
spräche mit Sergio und Christian und ihre Ausarbeitung
und Weiterentwicklung der Übungsaufgaben wäre die Ver- [ISO/IEC/IEEE 2010] ISO/IEC/IEEE: Systems and
anstaltung in ihrer heutigen Form nur schwer vorstellbar. software eng. – Vocabulary, 2010. – 24765:2010(E)
Weiterhin danken wir unseren stud. Hilfskräften für ihre
engagierte Mitarbeit an Aufgaben und Tutorials. [Klose u. Lettrari 2001] K LOSE, J. ; L ETTRARI, M.:
Scenario-based Monitoring and Testing of Real-
Literatur time UML models. In: G OGOLLA, M. (Hrsg.) u. a.:
UML Bd. 2185, Springer, 2001 (LNCS)
[Anderson u. a. 2001] A NDERSON, L. W. (Hrsg.) u. a.:
A Revision of Bloom’s Taxonomy of Educational Ob- [Klose u. Wittke 2001] K LOSE, J. ; W ITTKE, H.: An
jectives. Longman, 2001 Automata Based Representation of Live Sequence
Charts. In: M ARGARIA, T. (Hrsg.) u. a.: TACAS,
[Apt u. a. 2009] A PT, K. R. ; B OER, F. S. ; O LDEROG,
Springer, 2001 (LNCS 2031)
E.-R.: Verification of Sequential and Concurrent Pro-
grams. Springer, 2009 [Krusche u. a. 2017] K RUSCHE, S. ; F RANKENBERG, N.
von ; A FIFI, S.: Experiences of a Software Engi-
[Arenis u. a. 2016] A RENIS, S. F. ; W ESTPHAL, B. u. a.:
neering Course based on Interactive Learning. In:
Ready for testing: ensuring conformance to indus-
SEUH, 2017, S. 32–40
trial standards through formal verification. In:
FAoC 28 (2016), Nr. 3, S. 499–527 [Lamport 2015] L AMPORT, L.: Who builds a house
without drawing blueprints? In: CACM 58 (2015),
[Balzert 2009] B ALZERT, H.: Lehrbuch der Softwa-
Nr. 4, S. 38–41
retechnik: Basiskonzepte und Requirements Enginee-
ring. 3rd. Spektrum, 2009 [Langenfeld u. a. 2016] L ANGENFELD, V. ; P OST, A.
u. a.: Requirements Defects over a Project Lifeti-
[Biggs u. Tang 2011] B IGGS, J. ; TANG, C.: Teaching
me. In: D ANEVA, M. (Hrsg.) u. a.: REFSQ Bd. 9619,
for Quality Learning at University. 4th. Open Uni-
Springer, 2016 (LNCS), S. 145–160
versity Press, 2011
[Larsen u. a. 1997] L ARSEN, K. G. ; P ETTERSSON, P. ;
[Bjørner 2006a] B JØRNER, .: SWE, Vol. 1: Abstraction
Y I, W.: U PPAAL in a Nutshell. In: STTT 1 (1997),
and Modelling. Springer, 2006
Dezember, Nr. 1, S. 134–152
[Bjørner 2006b] B JØRNER, D.: SWE, Vol. 2: Specifica-
[Lehmann u. a. 2015] L EHMANN, T. u. a.: Lecture En-
tion of Systems and Languages. Springer, 2006
gineering. In: S CHMOLITZKY, A. (Hrsg.) u. a.: SEUH
[Bjørner 2006c] B JØRNER, D.: SWE, Vol. 3: Domains, Bd. 1332, CEUR-WS, 2015, S. 103–109
Req. and Software Design. Springer, 2006
[Ludewig u. Lichter 2013] L UDEWIG, J. ; L ICHTER, H.:
[Bloom 1956] B LOOM, B. S. (Hrsg.): Taxonomy of Software Engineering. 3rd. dpunkt, 2013
Educat. Objectives: Cognitive Domain. Longman,
[OMG 2006] OMG: Object Constraint Language, Ver-
1956
sion 2.0. formal/06-05-01, 2006
[Cohen u. a. 2009] C OHEN, E. u. a.: VCC: A Practical
[Rupp u. a. 2014] R UPP, C. u. a.: Requirements-
System for Verifying Concurrent C. In: B ERGHOFER,
Engineering und -Management. 6th. Hanser, 2014
S. (Hrsg.) u. a.: TPHOLs Bd. 5674, Springer, 2009
(LNCS), S. 23–42 [Sedelmaier u. Landes 2017] S EDELMAIER, Y. ; L AN -
DES , D.: Experiences in Teaching and Learning Req.
[Damm u. Harel 2001] D AMM, W. ; H AREL, D.: LSCs:
Engineering on a Sound Didactical Basis. In: D AVO -
Breathing Life into Message Sequence Charts. In:
LI , R. (Hrsg.) u. a.: ITiCSE, ACM, 2017, S. 116–121
FMSD 19 (2001), Juli, Nr. 1, S. 45–80
[Siegeris 2017] S IEGERIS, J.: LearnTeamPlenum. In:
SEUH, 2017, S. 1–7
12
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 32
Formale Methoden in der Softwaretechnik-Vorlesung
Bernd Westphal, Uni Freiburg
[Sommerville 2010] S OMMERVILLE, I.: Software Engi- lated. In: Stud. Educat. Eval. 54 (2017), S. 22 – 42
neering. 9th. Pearson, 2010
[Westphal 2018] W ESTPHAL, B.: An Undergraduate
[Uttl u. a. 2017] U TTL, B. u. a.: Meta-analysis of fa- Requirements Engineering Curriculum with Formal
culty’s teaching effectiveness: Student evaluation Methods. In: REET, IEEE, 2018, S. 1–11
of teaching ratings and student learning are not re-
13
V. Thurner, O. Radfelder, K. Vosseberg (Hrsg.): SEUH 2019 33