|Reactive Systems Group|
|Building: E 1.1, Room: 1.08|
|Phone:||+49 681 302 5654|
|eMail:||schwenger at react.uni-saarland.de|
|Office Hours:||Whenever my door is open|
- Runtime Verification
Rarely are safety-critical systems sufficiently simple to be verified statically. So rather than verifying the correctness of all traces, testing validates the system on a select set of presumably-relevant executions. Runtime verification goes one step further: It keeps a close eye on the running system and thus verifies a single trace. This trace is by its nature highly relevant. Upon observation of undesired behavior, mitigation procedures can be initiated.
- Cyber-Physical Systems
The interaction of a computer system with physical processes is a clash of two worlds: a computer works in a clocked, discrete world with clear semantics. When the processor’s clock rises, the internal state changes, when it falls, the world stands still. The real, physical world, however, is chaotic: nature does not wait for a clock tick to apply changes. Yet, the interaction of machines with the real world is essential: machines control power plants, cars, satellites and factories. So assisting the development process and finding suitable abstractions is a task worth pursuing.
Development for safety-critical software roughly follows the following pattern: assess requirements, formalize them, develop software complying to the requirements by hand, automatically verify them against the formal specification. If the verification fails, refine the software. Formal program synthesis aims at simplifying this process: assess requirements, formalize them, automatically synthesize a program that complies with the requirements by construction.
|[BFSST20]||RTLola Cleared for Take-Off: Monitoring Autonomous Aircraft.
Joint work with Jan Baumeister, Bernd Finkbeiner, Sebastian Schirmer and Christoph Torens. CAV 2020. July 2020.
|[FSS20]||Simplex Architecture Meets RTLola.
Joint work with Bernd Finkbeiner and Jessica Schmidt. MT@CPSWeek 2020. April 2020.
|[MNS+20]||From LTL to rLTL Monitoring: Improved Monitorability through Robust Semantics.
Joint work with Corto Mascle, Daniel Neider, Paulo Tabuada, Alexander Weinert, and Martin Zimmermann. HSCC 2020. April 2020.
Slides, Technical Report
|[Schw19]||Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS.
Master Thesis at Saarland University. September 2019.
|[BFST19a]||FPGA Stream-Monitoring of Real-time Properties.
Joint work with Jan Baumeister, Bernd Finkbeiner, and Hazem Torfah. EMSOFT 2019. October 2019.
|[BFST19b]||On the Similarities of Aircraft and Humans: Monitoring CPS with StreamLAB.
Joint work with Jan Baumeister, Bernd Finkbeiner, and Hazem Torfah. CyberCardia@ESWeek 2019. October 2019.
|[FFS+19b]||StreamLAB: Stream-based Monitoring of Cyber-physical Systems.
Joint work with Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Marvin Stenger, Leander Tentrup and Hazem Torfah. CAV 2019. July 2019.
|[FFS+19a]||Real-time Stream Monitoring with StreamLAB.
Joint work with Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Leander Tentrup and Hazem Torfah. MT@CPSWeek 2019. March 2019.
|[STH+16]||From OpenCCG to AI Planning: Detecting Infeasible Edges in Sentence Generation.
Joint work with Álvaro Torralba, Jörg Hoffmann, David Howcroft, and Vera Demberg, COLING 2016. December 2016.
|[Schw16]||When a Sentece Falls apart. Using Heuristically Guided Dead End Detection in Natural Language Processing.
Bachelor Thesis at Saarland University. December 2016.
- Nobody’s Perfect: Monitoring Systems that Work Most of the Time: Slides
Invited Talk at Toyota Research Institute, Boston, October 2019.
- Let’s not Trust Experience Blindly: Formal Runtime Verification for CPS: Slides
Invited Talk at New York University and Yale University, October 2019.
- FPGA Stream-Monitoring of Real-time Properties: Slides, Paper
Conference Talk at EMSOFT 2019, New York, October 2019.
- Let’s not Trust Experience Blindly: Formal Monitoring of Humans and other CPS: Slides
Master Thesis Talk at Saarland University, August 2019
- StreamLAB: Stream-based Monitoring of Cyber-Physical Systems: Slides, Paper
Conference Talk at CAV 2019, New York, July 2019.
- Real-time Stream Monitoring with StreamLAB: Slides, Paper
Workshop Talk at MT@CPSWeek 2019. Montreal, April 2019
- XMas 4.0 Digitalisierung am Nordpol Slides (de), (en)
Christmas Lecture for 24h Lecture, Saarland University, December 2017
|StreamLAB||Real-Time Stream Monitoring Framework|
|rLTL Monitor||Monitor Construction for Robust LTL|
- Stefan Oswald: Research Assistant, ongoing
Static Analyses for RTLola Specifications
- Jessica Schmidt: Bachelor Thesis, ongoing
Monitoring Glycogen Levels
- Florian Kohn: Research Assistant, ongoing
RTLola Network Intrusion Detection
- Carsten Gerstacker: Master Thesis
Specification-Aided Trajectory Prediction with Recurrent Neural Networks
- Stefan Oswald: Bachelor Thesis, 2020
Verifiable Runtime Monitor Generation for Lola Specifications (pdf coming soon)
Co-advised by Noemi Passing
- Daniel Schäfer: Master Thesis, ongoing
Knowledge-based Programming for an Accelerated Synthesis
- Sanny Schmitt: Research Assistant, ongoing
Learning Hybrid Automata
- Jan Baumeister: Master Thesis, 2020
Tracing Correctness: A Practical Approach to Traceable Runtime Monitoring
- Paul Bungert: Bachelor Thesis, 2019
Monitoring Hybrid Automata (pdf coming soon)
- Rafael Dewes: Research Assistant, 2019
Synthesis of Autonomous Robots
- Daniel Schäfer: Research Assistant, 2019
Synthesis of Autonomous Robots
- Jan Baumeister: Research Assistant, 2018 – 2019
Translating RTLola Specifications to FPGA
- Hendrik Leidinger: Master Thesis, 2019
Learning the Desired Behavior for Causality Analyses
- Christoph Rosenhauer: Bachelor Thesis, 2019
Compiling Lola 2.0 to C
- Marvin Hofmann: Bachelor Thesis, 2018
Runtime Verification of Critical Web-based Systems
- Lukas Stemmler: Bachelor Thesis 2018
Communication Rules for Static Networks
- Reviewer for NASA FM’20
- Reviewer for CSL’20.
(Mostly) Useful References
|How to Write Well||Compilation of common mistakes|
|How to Write Papers so People Can Read Them||Slides by Derek Dreyer|
| On Preparing
||Slides by Ranjit Jhala|
|Github||Thesis Template, Keyboard Layout for CS People, etc.|
|Summer 2019||Assistant for Hybrid Systems|
|Summer 2018||Assistant for Embedded Systems|
|Winter 2017||Assistant for Time Machine|
|Summer 2017||Coach for Mathematics Precourse|
|Winter 2016||Tutor for Verification at the Reactive Systems Group|
|Summer 2016||Student Tutor for Embedded Systems at the Reactive Systems Group|
|Summer 2015||Tutor for Artificial Intelligence at the Foundations of Artificial Intelligence Group|
|Winter 2014||Tutor for Theoretical Computer Science at the Computational Complexity Group|
|Summer 2014||Tutor for System Architecture at the Real-Time and Embedded Systems Lab|