Seminar: Eingebettete Systeme (SS2013)
Übersicht
Ein eingebettetes System (engl. embedded system) ist ein informationsverarbeitendes System, das aus Hard- und Software besteht und in einen technischen Kontext eingebunden (eingebettet) ist. Diese komplexen Systeme haben aufgrund ihrer hohen Integrationsdichte mittlerweile - und für den Benutzer weitestgehend unsichtbar - in zahlreiche Produkte des täglichen Bedarfs Einzug gehalten, etwa in Haushaltsgeräte, Automobile oder Unterhaltungselektronik. Ihr primärer Zweck liegt dabei aber meist nicht in der Verarbeitung und Aufbereitung von Information, sondern vielmehr sind diese "Kleinrechner" zuständig für die Steuerung, Regelung oder Überwachung des Systems, in dem sie eingebettet sind, oder sie sorgen für die Filterung und (De)Codierung von Daten bzw. Signalen.
Die effiziente und modulare Programmierung eingebetteter Systeme erfordert zunehmend den Einsatz des modell-basierten Software-Entwurfs. Dabei dienen gültige (valide) Modelle als Grundlage zum Testen und Verifizieren der angestrebten Spezifikation. Das Themen-Portfolio in diesem Seminar reicht dabei von der Modell-Validierung und formaler Äquivalenzprüfung über Testfallgenerierung und funktionaler Eigenschaftenprüfung bis hin zu einzelnen Werkzeugen wie SPIN oder SMV.
Organisatorisches
Das Seminar findet immer donnerstags um 12:00 Uhr in SE III statt. Als Vortragsthemen stehen dabei die nachfolgend aufgeführten Themen ab sofort zur Verfügung. Wer Interesse an der Bearbeitung eines der angegebenen Themen hat, kann sich dieses bereits im Vorfeld (per Email oder persönlich bei Clemens Mühlberger) oder auch erst in der Einführungsveranstaltung am 18.04.2013 reservieren lassen. Dieses Seminar ist auch für den Bachelor-Studiengang geeignet!
Zu jedem Thema soll in Einzelarbeit ein etwa 30- bis 45-minütiger Vortrag sowie eine schriftliche Ausarbeitung im Umfang von ca. 10 Seiten im LCNS-Format erstellt werden. Der Vortrag soll dann zu einem noch festzulegenden Termin vor den Teilnehmern des Seminars präsentiert werden. Bei den Vorträgen gilt i.Ü. Anwesenheitspflicht für alle Teilnehmer. Zudem ist spätestens eine Woche vor dem jeweiligen Vortragstermin ein Probevortrag vor dem Betreuer verpflichtend. Der entsprechende Betreuer steht bei Fragen, die während der Einarbeitung und Vortragserstellung auftauchen, gerne zur Verfügung! Die Vorträge und Vorlagen zur Ausarbeitung stehen für die Seminarteilnehmer auf der WueCampus-Seite des Seminars bereit. Der dafür notwendige Zugangsschlüssel wird in der Einführungsveranstaltung bekannt gegeben.
Um die Einarbeitung in die jeweiligen Vortragsthemen zu erleichtern, werden zusätzlich für jedes Thema Literaturvorschläge zur Verfügung gestellt. Allerdings müssen die Seminarteilnehmer auch eine eigene Literaturrecherche anstrengen! Neben der Uni-Bibliothek können dabei folgende Zitatsammlungen hilfreich sein:
- CiteSeer (http://citeseer.ist.psu.edu/)
- CiteBase (http://www.citebase.org/)
- Google Scholar (http://scholar.google.de/)
Die erfolgreiche Teilnahme (d.h. kontinuierliche Anwesenheit, Probevortrag, Vortrag und Ausarbeitung) wird durch einen Leistungsschein bzw. ECTS-Punkte belohnt. Für weitere Auskünfte steht der jeweilige Betreuer gerne zur Verfügung!
Themen- und Terminübersicht
Einführungsveranstaltung
| Termin: 18.04.2013 |
| Vortragender: Clemens Mühlberger |
In dieser Einführungsveranstaltung werden einige, für das Seminar wesentliche Begriffe (z.B. Eingebettetes System, Betriebssystem, ...) kurz erläutert, sowie die bereitgestellten Themen vorgestellt. Eine Themenreservierung ist ebenso möglich, sowie die Erörterung des organisatorischen Ablaufs. |
Model Validation - vergeben
| Betreuer: C. Mühlberger |
| Termin: 16.05.2013 |
Kapitel 2.1-2.5: Model Validation, aus: "Embedded Systems and Software Validation", A. Roychoudhury, p. 7-38 |
Code Coverage - vergeben
| Betreuer: C. Mühlberger |
| Termin: 16.05.2013 |
Kapitel 5: Code Coverage, aus: "Functional Verification Coverage - Measurement and Analysis", Piziali Andrew, p. 79-96 |
Assertion Coverage - vergeben
| Betreuer: C. Mühlberger |
| Termin: 23.05.2013 |
Kapitel 6: Assertion Coverage, aus: "Functional Verification Coverage - Measurement and Analysis", Piziali Andrew, p. 97-108 |
Formale Äquivalenzprüfung - vergeben
| Betreuer: C. Mühlberger |
| Termin: 23.05.2013 |
Kapitel 7.1: Formale Äquivalenzprüfung eingebetteter Software, aus: "Digitale Hardware/Software-Systeme - Spezifikation und Verifikation", Teich J., Haubelt Ch., p. 362-390 |
Testfallgenerierung - vergeben
| Betreuer: C. Mühlberger |
| Termin: 06.06.2013 |
Kapitel 7.2: Testfallgenerierung zur simulativen Eigenschaftsprüfung, aus: "Digitale Hardware/Software-Systeme - Spezifikation und Verifikation", Teich J., Haubelt Ch., p. 391-415 |
Funktionale Eigenschaftsprüfung - vergeben
| Betreuer: C. Mühlberger |
| Termin: 06.06.2013 |
Kapitel 7.3: Formale funktionale Eigenschaftsprüfung von Programmen, aus: "Digitale Hardware/Software-Systeme - Spezifikation und Verifikation", Teich J., Haubelt Ch., p. 416-430 |
Zeitanalyse - vergeben
| Betreuer: C. Mühlberger |
| Termin: 13.06.2013 |
Kapitel 7.4: Zeitanalyse, aus: "Digitale Hardware/Software-Systeme - Spezifikation und Verifikation", Teich J., Haubelt Ch., p. 431-447 |
Das Validierungstool SPIN - vergeben
| Betreuer: C. Mühlberger |
| Termin: 13.06.2013 |
Kapitel 2.9: The SPIN Validation Tool, aus: "Embedded Systems and Software Validation", A. Roychoudhury, p. 82-85 |
Das Validierungstool SMV - vergeben
| Betreuer: C. Mühlberger |
| Termin: 20.06.2013 |
Kapitel 2.10: The SMV Validation Tool, aus: "Embedded Systems and Software Validation", A. Roychoudhury, p. 86-88 |
Planbarkeitsanalyse mit UPPAAL - vergeben
| Betreuer: C. Mühlberger |
| Termin: 20.06.2013 |
Kapitel 4: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1, aus: "Model-Based Design for Embedded Systems", Nicolescu G., Mosterman P. J., p. 93-120 |
Fallbeispiel: Luftfahrtelektronik
| Betreuer: C. Mühlberger |
| Termin: |
Quentin Enard et al.: "Design-driven Development of Dependable Applications - A Case Study in Avionics", aus: "3rd International Conference on Pervasive and Embedded Computing and Communication Systems" (PECCS) 2013, Barcelona (Spain), p. 177-188 |
