====== Formale und semiformale Methoden für eingebettete Software ====== ~~NOTOC~~ ==== Inhalt ==== Der Begriff “formale Methoden” fasst eine Vielzahl von **Techniken zur mathematischen Modellierung und Verifikation** von Computersystemen zusammen: formale Spezifikationssprachen (z.B. ‘Z’), Automaten, Temporallogik, Prozesskalküle, Model-Checking usw. Sie werden in der Softwaretechnik und in der industriellen Praxis in sicherheitskritischen Bereichen angewendet um Fehlerfreiheit zu beweisen oder plausibel zu machen, um Betriebssicherheit zu gewährleisten und um technische Systeme auf die Erfüllung von Anforderungen zu überprüfen. \\ Sowohl formale als auch semiformale Methoden haben eine strikt definierte **Syntax und Semantik** für Sprachelemente. Semiformale Modelle eignen sich typischerweise zur unzweideutigen Kommunikation von Systemanforderungen und -eigenschaften, darüber hinaus auch zu einfachen Modellanalysen, z.B. einer Duplikatserkennung. \\ Formalen Methoden liegt zusätzlich ein **Kalkül** zugrunde, darin unterscheiden sie sich von semiformalen Ansätzen und gängigen Programmiersprachen. Man kann mit formalen Modellen also “rechnen”: Man kann sie ineinander und in kanonische Darstellungen transformieren, sie so vergleichen und weitergehende Eigenschaften, auch Systemeigenschaften, analysieren. Die zugrunde liegende Annahme ist: besitzt das Modell eine Eigenschaft, dann besitzt das modellierte System sie auch. \\ Ist die Erstellung eines korrekten formalen Modells weniger aufwendig als die fehlerfreie Beschreibung des gewünschten Verhaltens in einer Programmiersprache, so ermöglicht die formale Spezifikation u.U. nicht nur eine **frühzeitige Analyse** des geplanten Systems, sondern ist auch kosteneffizient. Der Einsatz formaler Methoden in der industriellen Software-Entwicklung steht jedoch noch ganz am Anfang. === Voraussetzungen === * **In diesem Seminar sind nur Masterstudenten zugelassen.** * Ggf. ist Vorwissen für die Bearbeitung einzelner Themen von Vorteil. * Bitte geben Sie relevantes Vorwissen bei Ihrer Anmeldung mit an, um Ihre Chance auf Zuteilung zu erhöhen. === Themen === * [[http://theory.stanford.edu/~aiken/publications/papers/popl05.pdf|Scalable Error Detection using Boolean Satisfiability]] * Betreuer: [[lehrstuhl:mitarbeiter:bohlender]] * Geeignet für: Master * [[http://link.springer.com/chapter/10.1007%2F978-3-540-75698-9_2|Slicing Abstractions]] * Betreuer: [[lehrstuhl:mitarbeiter:simon]] * Geeignet für: Master * [[http://www.di.ens.fr/~cousot/publications.www/CousotEtAl-FMSD-v35n3pp229-264-dec-2009.pdf|Why does Astree scale up?]] * Betreuer: [[lehrstuhl:mitarbeiter:simon]] * Geeignet für: Master * [[http://link.springer.com/chapter/10.1007/978-3-662-46681-0_5|C2E2: A Verification Tool for Stateflow Models]] * Betreuer: [[lehrstuhl:mitarbeiter:makhlouf]] * Geeignet für: Master * [[http://dl.acm.org/citation.cfm?id=1064165.1064173&coll=DL&dl=GUIDE&CFID=518716659&CFTOKEN=83077992|Syntax Error Repair for a Java-based Parser Generator]] * Betreuer: [[lehrstuhl:mitarbeiter:obster]] * Geeignet für: Master * [[http://link.springer.com/chapter/10.1007/978-3-319-13338-6_19|Supervisory Control of Discrete-Event Systems via IC3]] * Betreuer: [[lehrstuhl:mitarbeiter:goebe]] * Geeignet für: Master * Der betreuende Mitarbeiter ist zurzeit im Ausland. Daher ist nur eine Fernbetreuung via E-Mail und Skype möglich. * [[http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1470160| Convex optimization proves software correctness]] * Betreuer: [[lehrstuhl:mitarbeiter:dernehl]] * Geeignet für: Master * [[http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6093675|Efficient model checking of PSL safety properties]] * Betreuer: [[lehrstuhl:mitarbeiter:foerster]] * Geeignet für: Master * [[http://dx.doi.org/10.1016/j.scico.2014.06.011|Contracts-refinement proof system for component-based embedded systems]] * Betreuer: [[lehrstuhl:mitarbeiter:foerster]] * Geeignet für: Master ==== Organisation ==== Es wird eine Einführungsveranstaltung geben in der die Themen und der zeitliche Ablauf des Seminars vorgestellt werden. Abgeschlossen wird das Seminar durch eine schriftliche Ausarbeitung auf Deutsch oder Englisch, sowie einer mündlichen Präsentation. Dieses Seminar wird organisatorisch zusammen mit zwei weiteren Themen unter dem Titel "Ausgesuchte Themen zur Eingebetteten Software" geführt. Es gibt einen gemeinsamen Lernraum im L2P, eine gemeinsame Campus-Veranstaltung und eine gemeinsame Einführungsveranstaltung. Die Notenmeldung erfolgt jedoch unter dem entsprechend gewählten Titel. === Terminplanung === Mittwoch, 7.10.2015 -- Kickoff\\ Donnerstag, 8.10.2015 -- Themenwahl\\ Donnerstag, 29.10.2015 -- Abgabe Structure & Bibliography\\ Freitag, 30.10.2015 -- Abmelde-Deadline\\ Sonntag 6.12.2015 -- First Version\\ Sonntag 17.1.2016 -- Final Version\\ Sonntag 7.2.2016 -- Slides Draft === Sprache === * Organisation: Deutsch/Englisch * Thematische Bearbeitung (Ausarbeitung + Präsentation): Deutsch oder Englisch. === Hinweise zur Anmeldung === Die Anmeldung erfolgt über die Zentrale Vergabe von Studien- und Seminarplätzen. Bitte geben Sie eventuelle Vorkenntnisse dort an. Eine Anmeldung über das Campus System ist nicht erforderlich. === Kriterien für eine erfolgreiche Teilnahme === * Verfassen einer schriftlichen Ausarbeitung (Abgabe als PDF) und Einhaltung der Rahmenbedingungen (Siehe Einführungsveranstaltung) * Folien und Abschlussvortrag (Abgabe der Folien als PDF oder ppt(x)) * Einhaltung aller Fristen * Anwesenheit bei allen Pflichtterminen === Art der Veranstaltung === Seminar (4 ECTS) === Campus/L2P === [[https://www3.elearning.rwth-aachen.de/ws15/15ws-45873|L2P ist aktiv ab ca. 6-8 Wochen vor Vorlesungsbeginn]]\\ [[https://www.campus.rwth-aachen.de/rwth/all/event.asp?mode=user&gguid=0x613FB23A5D8D324D888232C95BC988C0&tguid=0x0B473CF286B45B4984CD02565C07D6F8|Campus Link]] === Rückfragen=== Für Rückfragen wenden Sie sich bitte an [[:lehrstuhl:mitarbeiter:obster]].