Logo des Repositoriums

Auflistung nach Autor:in "Runge, Tobias"

1 - 2 von 2
  • ConferencePaper
    Skill-Based Verification of Cyber-Physical Systems
    (Software Engineering 2021, 2021) Knüppel, Alexander; Jatzkowski, Inga; Nolte, Marcus; Runge, Tobias; Thüm, Thomas; Schaefer, Ina
    This work has been accepted at the 23rd International Conference on Fundamental Approaches to Software Engineering, held as part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020. The increase of complexity in modeling cyber-physical systems poses a challenge for formally ensuring their functional correctness. Lack of expert knowledge and scalability are two limiting factors that prohibit a seamless integration into today's software engineering processes. To address this challenge, we propose to adopt and formalize the notion of skill graphs, an abstract and easy-to-use modeling notion for representing automated vehicle driving maneuvers. For formally verifying that skill graphs are well-formed and comply with a given set of safety requirements, we incorporate hybrid programs into our formalization. Hybrid programs constitute a program notion for cyber-physical systems on the basis of differential dynamic logic, which enables deductive and compositional verification following the idea of Hoare-style reasoning. That is, simpler verified skill graphs can be combined to exhibit complex maneuvers while validity is retained (i.e., without the need of re-verification). To showcase the benefits of our theoretical considerations, we implemented our framework in an open-source tool named Skeditor and conducted a case study exhibiting an automatic vehicle follow mode.
  • ConferencePaper
    Tool Support for Correctness-by-Construction
    (Software Engineering 2021, 2021) Runge, Tobias; Schaefer, Ina; Cleophas, Loek; Thüm, Thomas; Kourie, Derrick; Watson, Bruce W.
    This work was published in International Conference on Fundamental Approaches to Software Engineering 2019. We tackled a fundamental problem of missing tool support of the correctness-by-construction (CbC) methodology that was proposed by Dijsktra and Hall and revised to a light-weight and more amenable version by Kourie and Watson. Correctness-by-construction (CbC) is an incremental approach to create programs using a set of small, easily applicable refinement rules that guarantee the correctness of the program with regard to its pre- and postcondition specifications. Our goal was to implement a functional and user-friendly IDE, so that developers will adapt to the CbC approach and benefit from its advantages (e.g., defects can be easily tracked through the refinement structure of the program). The tool has a hybrid textual and graphical IDE that programmers can use to refine a specification to a correct implementation. The textual editor fits to programmers that want to stay in their familiar environment, while the graphical editor highlights the refinement structure of the program to give visual feedback if errors occur using KeY as verification backend. The tool was evaluated regarding feasibility and effort to develop correct programs. Here, slight benefits in comparison to a standard verification approach were discovered.