Mathematik und Informatik

Prof. Dr. Paula Herber, Institut für Informatik

Current Publications• 18th International Conference on integrated Formal Methods, {iFM} 2023. Lecture Notes in Computer Science Vol. 14300, 2024 online
Tasche P; Monti RE; Drerup SE; Blohm P; Herber P; Huisman M Deductive Verification of Parameterized Embedded Systems Modeled in {SystemC}. Verification, Model Checking, and Abstract Interpretation - 25th International Conference, {VMCAI} 2024Lecture Notes in Computer Science Vol. 14500, 2024, pp 187-209 online
Adelt Julius; Gebker Julian; Herber Paula Reusable formal models for concurrency and communication in custom real-time operating systems. International Journal on Software Tools for Technology Transfer Vol. 26 (2), 2024, pp 229-245 online
Bodden E; Felderer M; Hasselbring W; Herber P; Koziolek H; Lilienthal C; Matthes F; Prechelt L; Rumpe B; Schaefer I Ernst Denert Software Engineering Award 2022. Ernst Denert Award for Software Engineering 2022: Practice Meets Foundations, 2024, pp 1-8 online
Tasche Philip; Herber Paula A Coverage-Driven Systematic Test Approach for Simultaneous Localization and Mapping. IEEE Conference on Software Testing, Verification and Validation (ICST), 2023, pp 25-36 online
Adelt J; Liebrenz T; Herber P Formal Verification of Intelligent Hybrid Systems that are modeled with Simulink and the Reinforcement Learning Toolbox. Software EngineeringLNI Vol. P-332, 2023, pp 29-30 online
Adelt J.; Bruch S.; Herber P.; Niehage M.; Remke A. Shielded Learning for Resilience and Performance Based on Statistical Model Checking in Simulink. Bridging the Gap Between AI and Reality - First International Conference, AISoLA 2023, Crete, Greece, October 23–28, 2023, ProceedingsLecture Notes in Computer ScienceLecture notes in computer science, 2023, pp 94-118 online
Blohm P; Adelt J; Herber P Safe Integration of Learning in SystemC using Timed Contracts and Model Checking. 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design, MEMOCODE 2023, 2023, pp 12-22 online
Adelt, Julius; Brettschneider, Daniel; Herber, Paula Reusable Contracts for Safe Integration of Reinforcement Learning in Hybrid Systems. Automated Technology for Verification and Analysis - 20th International Symposium (ATVA)Lecture Notes in Computer Science Vol. 13505, 2022, pp 58-74 online
Current ProjectsSafe Integration of Learning In Autonomous cyber-physical Systems

Cyber-physical systems are systems that combine discrete control (or cyber) aspects with physical aspects. We can find examples of such systems in cars, airplanes, or water supply systems. With the current trend towards self-driving cars and smart infrastructures, these systems are becoming increasingly autonomous. This means that they use learning to take good control decisions in unforeseen situations and dynamic environments. While learning significantly increases their flexibility, it also increases their complexity. At the same time, failures often have serious consequences in cyber-physical systems, as they may cause huge financial losses or even loss of lives. Thus, the correctness and reliability of these systems are of vital importance. Formal verification techniques, which establish correctness using rigorous mathematical methods, can provide us with guarantees about crucial safety properties of cyber-physical systems. However, formal verification is known to be enormously expensive. Techniques for automatic verification explore the underlying state space of a given system, which is often too large to be fully explored. Deductive verification techniques provide a powerful solution to this problem by leveraging abstract mathematical reasoning, but they require tremendous effort and expertise to provide the necessary abstractions and proof ideas to guide the verification process. This problem is especially severe for autonomous cyber-physical systems, because the trial-and-error processes and statistical methods that are commonly used in learning are hard to capture formally.The main goal of this project is the safe integration of learning in autonomous cyber-physical systems with acceptable effort. Our key concept to achieve this is reusability. In particular, we investigate reusable abstractions for autonomous cyber-physical systems. By providing novel concepts for systematic reuse of formal specifications and abstractions (for example, property and specification patterns), we will significantly reduce the required manual effort and expertise, and thus increase the applicability and acceptance of deductive verification in industrial design processes for autonomous cyber-physical systems.

SystemC to Timed Automata Transformation Engine STATE is a SystemC to Timed Automata Transformation Engine. It takes a SystemC design as input and transforms it into a corresponding UPPAAL timed automata model. The transformation is based on a formal semantics defined for SystemC in [Her08],[Her10],[Her11],[Pockr11],[Pockr13],[Her13]. The general idea is to map the informally defined semantics of SystemC to the formally well-defined semantics of UPPAAL timed automata. This mapping defines a formal semantics for SystemC, and, at the same time, it enables the automatic transformation from a given SystemC design into a semantically equivalent UPPAAL timed automata model. The transformation preserves the informally defined semantics of SystemC completely. To ease debugging, it also keeps the structure of the original SystemC design transparent to the designer in the UPPAAL model (through prefixing). The current version of STATE supports structs, pointers, and arrays as well as the TLM 2.0 standard. online
E-Mailpaula dot herber at uni-muenster dot de
Phone+49 251 83-32421
FAX+49 251 83-32742
Secretary   Sekretariat Kaiser-Mariani
Frau Julia Kaiser-Mariani
Telefon +49 251 83-32740
Fax +49 251 83-32742
Zimmer 704
AddressProf. Dr. Paula Herber
Institut für Informatik
Fachbereich Mathematik und Informatik der Universität Münster
Einsteinstrasse 62
48149 Münster
Diese Seite editieren