BME MDA - a Műegyetem Digitális Archivuma
Not a member yet
47877 research outputs found
Sort by
Az izraeli-palesztin konfliktus 2023. október 7. óta fennálló új aspektusának médiakeretezése a magyarországi sajtóban
No full textEvaluation of a graph distance metric to assess the diversity of timed automata
No full textReliable testing and benchmarking of modelling tools require diverse inputs. However, diversity has no precise definition in this context, nor is there a given level of acceptance. While there is one diversity metric [1] that can be used to assess diversity for structural models, there is no such metric for behavioural models, like timed automata. In our research, we work on adapting the structural diversity metrics presented in [1] to behavioural models. We evaluate the structural diversity of timed automata by first transforming the models to a unified, structural format and then applying the structural diversity metric. In this paper, we present a way to adapt the distance metric to timed automata and we apply it to an existing benchmark suite. We evaluate the metric both manually – checking whether models that are similar according to the metric actually show similar behaviours –, and automatically – checking whether verification algorithms perform similarly well/poorly (with respect to other algorithms) on ’similar’ models. We show that – despite only considering structural differences – the metric can be useful for finding models with similar behaviours among timed automata
An approach to formal verification of atomic swap protocols
Get PDFAtomic swaps are crucial for trustless cryptocurrency transactions between different blockchains, yet they currently face several challenges in terms of security and usability. The complexity of communication processes and cryptographic primitives in existing protocols means that many cannot be quickly reviewed, or the reviewing is too difficult, lacking appropriate formal methods for model verification. These issues hinder the scalability of blockchain technology and limit its broader adoption, potentially suppressing innovation in decentralized financial systems and applications. This paper models Adaptor signatures, which are used to realize Point Time-Locked Contracts (PTLC) atomic swaps, based on the Dolev-Yao model. This paper proposes a standard atomic swap formal verification model based on its cryptographic primitives and uses Finite State Automata (FSA) to verify the communication protocol's workflow in the UPPAAL tool, summarizing how to securely and effectively conduct atomic swap protocols. Secure and efficient atomic swap protocols will promote the scalability of blockchain technology, encourage wider adoption, and aid in the development of more efficient cross-chain transactions
