Overview of my Research (Poster [pdf])
Problem Statement: Concurrency is an ubiquitous phenomenon in real-world cyber-physical systems (CPSs). Still logical methods for the analysis of CPSs lack support for modeling and verifying parallelism. This misalignment leaves only the error-prone rephrasing of natural parallelism into monolithic/sequential models. Moreover, it obstructs compositional verification along the parallel subcomponents, which is the key to the large-scale verification of concurrent CPSs.
Distributed CPSs are the class of multidynamic systems combining discrete, continous, and communication dynamics.
Mission: To overcome the shortcomings described above, I study extensions of differential dynamic logic (dL) to concurrency. The dynamic logic of communicating hybrid programs (dLCHP) enables modeling and verification of distributed CPSs. This system class captures wide-ranging applications, e.g. in autonomous driving and robot collision avoidance.
Increase the Trust: Although formal verification is considered the royal approach to safety (especially for CPSs), the correctness of many formal methods itself is based on a shaky foundation. Therefore, dLCHP has a proof calculus based on uniform substitution. The uniform substitution approach enables a close alignment of theorem prover implementations and their logic, as well as, the implementation by means of a microkernel. This increases the trust one can put into the verification results significantly compared to results obtained from tools based on tens of thousands of lines of soundness-critical implementation.
Autonomous driving is a prime example for distributed CPSs, where the relevance for safety verification is inherently evident due to the direct impact of correct behavior on people's health and lives.
|||Marvin Brieger, Stefan Mitsch, and André Platzer. Uniform substitution for dynamic logic with communicating hybrid programs. In CADE, 2023. [ bib | DOI | arXiv | pdf | slides ]|
|||Marvin Brieger, Stefan Mitsch, and André Platzer. Dynamic logic of communicating hybrid programs. CoRR, abs/2302.14546, 2023. [ bib | DOI | pdf ]|
This file was generated by bibtex2html 1.99.