Now showing1 - 2 of 2
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Data-driven probabilistic evaluation of logic properties with PAC-confidence on Mealy machines
    Cyber-Physical Systems (CPS) are complex systems that require powerful models for tasks like verification, diagnosis, or debugging. Often, suitable models are not available and manual extraction is difficult. Data-driven approaches then provide a solution to, e.g., diagnosis tasks and verification problems based on data collected from the system. In this paper, we consider CPS with a discrete abstraction in the form of a Mealy machine. We propose a data-driven approach to determine the safety probability of the system on a finite horizon of n time steps. The approach is based on the Probably Approximately Correct (PAC) learning paradigm. Thus, we elaborate a connection between discrete logic and probabilistic reachability analysis of systems, especially providing an additional confidence on the determined probability. The learning process follows an active learning paradigm, where new learning data is sampled in a guided way after an initial learning set is collected. We validate the approach with a case study on an automated lane-keeping system.
    Publicationtype: Conference Paper
      7
  • Some of the metrics are blocked by your 
    Item type:Publication,
    Information flow analysis – understanding the trade-offs between static and dynamic analysis
    (VDE Verlag, 2025-03) ; ;
    Information Flow Analysis (IFA) is an established approach to understand designs and their vulnerabilities with respect to information leaks. Dynamic simulation-based analysis methods have been proposed and are widely used due to their computational efficiency. However, they may miss to identifiy all possible information flow in a design. On the other hand less scalable formal IFA is exact, but may not be capable of analyzing larger designs. The actual comparison has not been done before. We compare formal and dynamic analysis to investigate the trade-offs. We give examples of their limitations. We explain how IFA runs using a solver for Satisfiability Modulo Theories (SMT) and show experimental results demonstrating the effects on real designs.
    Publicationtype: Conference Paper
      19