Exercise: Introduction to Formal Software Analysis (Ü Inf-GSoZu) (080045)- Dozent/in
- Prof. Dr. Dirk Nowotka
- Angaben
- Übung, 2 SWS
Unterrichtssprache Englisch
Zeit und Ort: Di 8:30 - 10:00, CAP4 - R.13.1304 a
vom 23.4.2024 bis zum 14.7.2024
- Zusätzliche Informationen
- Erwartete Teilnehmerzahl: 25
- Zugeordnet zu: Inf-GSoZu: Introduction to Formal Software Analysis (080040)
Forschungsprojekt - Zuverlässige Systeme (080008)- Dozentinnen/Dozenten
- Prof. Dr. Dirk Nowotka, Lukas Haschke, M.Sc., M.Sc. Marek Hummel
- Angaben
- Studienprojekt, benoteter Schein, ECTS-Studium, ECTS-Credits: 10
Praesenzveranstaltung
Zeit und Ort: n.V.
Bemerkung zu Zeit und Ort: n. V.
- Voraussetzungen / Organisatorisches
- Zusammenfassung
Im Rahmen dieses Forschungsprojektes bieten wir Studierenden die Gelegenheit, aktiv an dem CAPTN FördeAreal (https://captn.sh/foerde-areal/) Projekt teilzunehmen. FördeAreal ist generell eine Unternehmung mit mehreren Akteuren und Partnern, neben der CAU auch die FH Kiel und weiteren wirtschaftlichen Unternehmen. Die Studierenden sollen unserem Team bei den Aufgaben der CAU für den Versuchsträger WaveLab unterstützen. Konkret geht es dabei um die Entwicklung von Software und KI-Systemen, welche die Daten der Sensoren der WaveLab auswerten, verarbeiten, vereinigen und weiterleiten. Fokuspunkte sind hierbei die Stabilität und Zuverlässigkeit der Systeme, der Grad der Zuversicht der eingehenden und ausgehenden Sensordaten und Prognosen.
- Inhalt
- Lernziele:
Ein Forschungsprojekt dient dazu, den Studierenden einen wirklichen Einblick in wissenschaftliche Arbeit und dessen Alltag zu bieten. Während unweigerlich das Wissen in verschiedene Aspekte vertieft wird, lernen die Studierenden durch dieses praxisnahe Projekt die Organisation und Arbeitsweisen einer Arbeitsgruppe kennen, die Vielfalt an Forschungsfragen, die sich ergeben, und die direkte Anwendbarkeit von den Ergebnissen an dem Versuchsträger. Es wird gelernt, wie wissenschaftliche Fragestellungen entstehen und entwickelt werden, wie diese dann geprüft und umgesetzt und dann schließlich evaluiert werden. Darüberhinaus werden jegliche Ergebnisse auch schriftlich und mündlich präsentiert.
Insbesondere sind folgende Ziele zu erreichen:
- Spezifikation der Forschungsfrage und der Ziele im Rahmen des Forschungsprojektes in Form eines Research Proposals.
- Arbeit in einem Team inklusive Selbst- und Gruppenorganisation, Prozessmanagement, Terminplanung und Aufgabenverteilung.
- Entwicklung von Komponenten zur Datenverarbeitung auf dem Forschungsschiff, und deren Integration in bestehende verteilte Systeme.
Fokus des Projektes soll sein, dass die ausgehenden fusionierten Daten in dem passenden Format und Umfang für weiterführende Systeme sind (Input für RL Training) und auch so zur Verfügung gestellt werden, dass diese gut angebunden werden können. Potenzielle Forschungsfragen in diesem Vorhaben können sein:
- Bestimmung der Positionen anderer Schiffe mittels optischer Sensorik: Wie können aus Bounding Boxes erkannter Schiffe, deren Position und Bewegung relativ zum Forschungsschiff bestimmt werden?
- Tracking der anderen Schiffe und Prediction von Bewegungsverhalten anderer Akteure.
- Verifikation der entwickelten Algorithmen. Z.B. durch Petri-Netze oder Timed Automata sollen die Komponenten und deren dynamisches Verhalten modelliert und formal verifiziert werden.
- Visualisierung von Seekarten und dynamische Darstellung von erkannten Objekten auf der Kieler Förde. Wie kann ein zuverlässiger Webservice entwickelt werden, um in Echtzeit die Wahrnehmung des Schiffes darzustellen.
*Weitere Voraussetzungen:*
Keine zwingenden Voraussetzungen. Grundlegende Kenntnisse in Programmierung, System Architecture, Software Engineering und Reinforcement Learning sind allerdings hilfreich, welche im Idealfall in den entsprechenden Modulen gelehrt werden. Darüberhinaus werden Tools wie Git, Docker, ssh etc. genutzt und hauptsächlich Python, mit den entsprechenden Data-Science und ML Modulen.
*Prüfungsleistungen:*
Präsentationen, Bericht und wissenschaftliche Arbeit.
*Teilnahme:*
Bitte senden Sie eine Mail an Marek Hummel (mhu@informatik.uni-kiel.de), um teilzunehmen oder weitere Informationen zu erhalten.
- Zusätzliche Informationen
- Erwartete Teilnehmerzahl: 6
Inf-GSoZu: Introduction to Formal Software Analysis (Inf-GSoZu) (080040)- Dozent/in
- Prof. Dr. Dirk Nowotka
- Angaben
- Vorlesung, 4 SWS, ECTS-Studium, ECTS-Credits: 8
Unterrichtssprache Englisch
Zeit und Ort: Do 12:15 - 13:45, 14:15 - 15:45, CAP4 - R.13.1304 a (außer Do 23.5.2024); Einzeltermine am 23.5.2024 12:15 - 13:45, OS75/S3 - R.31; 23.5.2024 14:15 - 15:45, OS75/S2 - R.210
vom 14.4.2024 bis zum 14.7.2024
- Inhalt
- Kurzfassung:
In this course we consider basic principles and techniques for the detection of errors and the certification of the absence of certain errors in software systems. The covered areas include testing, model-checking, and abstract interpretation.
Lernziele:
A successful attendant of this course will gain an understanding in techniques and formal methods for error finding and proving of program properties. He or she will be able to evaluate different analysis methods and to employ them.
Lehrinhalte:
The course breaks down into three parts.
Part one: Testing. A systematic approach to various aspects of testing is presented: code inspections and walk throughs, control-flow coverage, data-flow coverage, black-box and white-box testing, test suites, conformance testing.
Part two: Model-checking. The issue of modelling a program is considered. The temporal logic CTL is introduced as a formalism to express program properties. CTL model-checking algorithms are presented.
Part three: Abstract interpretation. The underlying theory is introduced and applications in the area of static code analysis are presented.
Basic knowledge in logic and theoretical foundations of computer science
Prüfungsleistung:
Oral exam over 30 minutes
Lehr- und Lernmethoden:
Lecture with beamer and white-board presentation; exercises for the application of theoretical concepts and self-assessment
- Empfohlene Literatur
- Glenford J. Myers: Methodisches Testen von Programmen. R. Oldenbourg Verlag, 7. Auflage 2001 (Englische Originalfassung: The Art of Software Testing. John Wiley and Sons, 1979)
Gerard J. Holzmann: Design and Validation of Communication Protocols. Prentice Hall Software Series, 1991.
Edmund C. Clarke, Orna Grumberg und Doron A. Peled: Model Checking. MIT Press, 2000.
Flemming Nielson, Hanne Riis Nielson und Chris Hankin: Principles of Program Analysis. Springer Verlag, 1999.
- Zusätzliche Informationen
- Erwartete Teilnehmerzahl: 25
- Zugeordnete Lehrveranstaltungen
- UE: Exercise: Introduction to Formal Software Analysis (080045)
-
Dozent/in: Prof. Dr. Dirk Nowotka
Zeit und Ort: Di 8:30 - 10:00, CAP4 - R.13.1304 a
Inf-MPAlgKombSeq: Masterprojekt - Algorithmik und Kombinatorik von sequenziellen Strukturen (Inf-MPAlgKombSeq) (080009)- Dozentinnen/Dozenten
- Prof. Dr. Dirk Nowotka, Dr. Pamela Fleischmann, Annika Huch
- Angaben
- Übung, 4 SWS, ECTS-Studium, ECTS-Credits: 10
Praesenzveranstaltung
Zeit und Ort: n.V.
Vorbesprechung: 25.3.2024, 10:00 - 11:00 Uhr
- Inhalt
- Storing the 2-dimensional concept of graphs as linear words is of broad interest. One way is not to linearise the adjacency matrix but to store whether to nodes are adjacent by alternating the corresponding letters in the word. In this project, we switch the perspective, i.e. coming from words - in particular k-local words, we are interested which graphs are represented by then.
- Zusätzliche Informationen
- Erwartete Teilnehmerzahl: 5
|
|
