Logo des Repositoriums

Auflistung nach Schlagwort "Formal Methods"

1 - 4 von 4
  • Konferenzbeitrag
    Applicability of Model Checking for Verifying Spacecraft Operational Designs
    (Modellierung 2024, 2024) Chrszon, Philipp; Maurer, Paulina; Saleip, George; Müller, Sascha; Fischer, Philipp M. ; Gerndt, Andreas; Felderer, Michael
    This is a summary of the paper Applicability of Model Checking for Verifying Spacecraft Operational Designs which has been published at the 26th International Conference on Model Driven Engineering Languages and Systems (MODELS 23).
  • Konferenzbeitrag
    Data-Driven Design and Evaluation of SMT Meta-Solving Strategies
    (Software Engineering 2022, 2022) Mues, Malte; Howar, Falk
    The 36th IEEE/ACM International Conference on Automated Software Engineering (2021) accepted the paper ‘Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost’ [MH21a] and selected it for an ACM SIGSOFT Distinguished Paper Award. The paper presents four generally applicable patterns for the combination of multiple SMT decision procedures in a meta-solving strategy and demonstrates how a meta-solving strategy for string constraints can be developed in a data-driven approach based on these patterns: The paper cleans up and merges existing collections of SMT benchmarks in string theory solving to evaluate and compare derived meta-solving strategies. Notably, we can demonstrate on the available data that commonly used strategies as earliest returning SMT solver do not always return the most reliable result if all available SMT solvers are combined. Instead, cross-checking strategies work slightly better at moderate overhead.
  • Konferenzbeitrag
    Rethinking multi-layer multi-domain network monitoring
    (5. DFN-Forum Kommunikationstechnologien – Verteilte Systeme im Wissenschaftsbereich, 2012) Liu, Feng; Marcu, Patricia; Schmitz, David; Yampolskiy, Mark
    Accurate and efficient network fault localisation based on monitoring is obviously one of the vital but also formidable tasks for successful network operations. With proliferations of large-scale network services, e.g. Géant E2E links, monitoring and fault localisation across multiple domains with data obtained from different network layers are becoming unprecedentedly important. Many efforts have been invested to tackle the challenges posed by fault localisation, nevertheless, most approaches only suggest partial solutions to the problematics of multi-domain multi-layer aspects. Most importantly, a comprehensive view and deep understanding of the problem is still missing. In this paper, we intend to systematically discuss challenges and their implications posed by fault localisation with consideration on multi-domain and multi-layer monitoring data. The contributions of this paper are manifold: first we identify key research challenges regarding multiple layer monitoring for fault localisation across domains; then based on the identified multiple layer network patterns, we establish comprehensive problem dimensions in a systematic and structured way which holds key to the solution development; finally we propose a formal definitions on information model which captures essential characteristics of multiple network layers across domains.
  • Workshopbeitrag
    Understanding Parameters of Deductive Verification: An Empirical Investigation of KeY
    (Software Engineering and Software Management 2019, 2019) Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina
    As formal verification of software systems is a complex task comprising many algorithms and heuristics, modern theorem provers offer numerous parameters that are to be selected by a user to control how a piece of software is verified. Evidently, the number of parameters even increases with each new release. One challenge is that default parameters are often insufficient to close proofs automatically and are not optimal in terms of verification effort. The verification phase becomes hardly accessible for non-experts, who typically must follow a time-consuming trial-and-error strategy to choose the right parameters even for trivial pieces of software. To aid users of deductive verification, we apply machine learning techniques to empirically investigate which parameters and combinations thereof impair or improve provability and verification effort. We exemplify our procedure on the deductive verification system KeY 2.6.1 and specified extracts of OpenJDK, and formulate 53 hypotheses of which only three have been rejected. We identified parameters that represent a trade-off between high provability and low verification effort, enabling the possibility to prioritize the selection of a parameter for either direction. Our insights give tool builders a better understanding of their control parameters and constitute a stepping stone towards automated deductive verification and better applicability of verification tools for non-experts.