arXiv subjects

Miroslav Popovic

Publications and source records attributed to Miroslav Popovic.

15 recordsLinked to original sources

arXiv2026

Evidence-Grounded Ensemble Diagnosis of 802.11 Packet Captures: A Multi-Stage Pipeline with Deterministic Reliability Scoring

Diagnosing 802.11 packet captures requires expert protocol knowledge, is slow, inconsistent across engineers, and unscalable. LLM-based approaches sound plausible but fabricate protocol events absent from captures (especially truncated traces), produce uncalibrated confidence scores, and suffer evaluation bias when golden references are co-produced by the model under test. We introduce PROBE (Protocol Reasoning Over evidence-Based Ensembles), a multi-stage pipeline addressing all three failures. It integrates (i) deterministic PCAP-to-text normalization with frame-level verifiability, (ii) multi-run, multi-candidate ensembles with optional cross-model second opinion and progressive obfuscation, (iii) a verdict-aware evidence framework treating absence of failure evidence as contributing evidence, and (iv) a fully deterministic composite reliability score from evidence validity, run-to-run stability, and cross-model agreement without LLM self-assessment. On 87 enterprise Wi-Fi captures (104 capture-reviewer pairs), single-pass LLM analysis raises weighted evidence F1 from 0.871 (expert baseline) to 0.912 but misses critical frames in 35% of cases. Naive ensemble voting drops below baseline (0.842) as majority voting amplifies conservative verdicts: 50% of confirmed failures are misclassified as 'no issue' or 'insufficient evidence.' Adding evidence-grounded reconciliation achieves 0.957 F1, a 96% auto-accept rate, and a worst-case floor above 0.70. LLM self-reported confidence clusters at 0.95 regardless of difficulty (71% report exactly 0.95), confirming it is uninformative. We also introduce a model-agnostic evaluation framework using per-field assertion matching, eliminating circular bias from model-co-produced golden references.

cs.LG↗

arXiv2025

Formal Verification of a Generic Algorithm for TDM Communication Over Inter Satellite Links

The Python Testbed for Federated Learning Algorithms is a simple FL framework targeting edge systems, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the universal TDM communication in the current time slot. The first two were formally verified in a previous paper using the CSP process algebra, and in this paper, we use the same approach to formally verify the third one, in two phases. In the first phase, we construct the CSP model as a faithful representation of the real Python code. In the second phase, the model checker PAT automatically proves correctness of the third generic algorithm by proving its deadlock freeness (safety property) and successful termination (liveness property).

cs.DC↗

arXiv2025

Generic Algorithm for Universal TDM Communication Over Inter Satellite Links

The original Python Testbed for Federated Learning Algorithms is a light FL framework, which provides the three generic algorithms: the centralized federated learning, the decentralized federated learning, and the TDM communication (i.e., peer data exchange) in the current time slot. The limitation of the latter is that it allows communication only between pairs of network nodes. This paper presents the new generic algorithm for the universal TDM communication that overcomes this limitation, such that a node can communicate with an arbitrary number of peers (assuming the peers also want to communicate with it). The paper covers: (i) the algorithm's theoretical foundation, (ii) the system design, and (iii) the system validation. The main advantage of the new algorithm is that it supports real-world TDM communications over inter satellite links.

cs.DC↗

arXiv2025

On the Efficiency of Dynamic Transaction Scheduling in Blockchain Sharding

Sharding is a technique to speed up transaction processing in blockchains, where the $n$ processing nodes in the blockchain are divided into $s$ disjoint groups (shards) that can process transactions in parallel. We study dynamic scheduling problems on a shard graph $G_s$ where transactions arrive online over time and are not known in advance. Each transaction may access at most $k$ shards, and we denote by $d$ the worst distance between a transaction and its accessing (destination) shards (the parameter $d$ is unknown to the shards). To handle different values of $d$, we assume a locality sensitive decomposition of $G_s$ into clusters of shards, where every cluster has a leader shard that schedules transactions for the cluster. We first examine the simpler case of the stateless model, where leaders are not aware of the current state of the transaction accounts, and we prove a $O(d \log^2 s \cdot \min\{k, \sqrt{s}\})$ competitive ratio for latency. We then consider the stateful model, where leader shards gather the current state of accounts, and we prove a $O(\log s\cdot \min\{k, \sqrt{s}\}+\log^2 s)$ competitive ratio for latency. Each leader calculates the schedule in polynomial time for each transaction that it processes. We show that for any $\epsilon > 0$, approximating the optimal schedule within a $(\min\{k, \sqrt{s}\})^{1 -\epsilon}$ factor is NP-hard. Hence, our bound for the stateful model is within a poly-log factor from the best possibly achievable. To the best of our knowledge, this is the first work to establish provably efficient dynamic scheduling algorithms for blockchain sharding systems.

cs.DC↗

arXiv2025

Translating Federated Learning Algorithms in Python into CSP Processes Using ChatGPT

The Python Testbed for Federated Learning Algorithms is a simple Python FL framework that is easy to use by ML&AI developers who do not need to be professional programmers and is also amenable to LLMs. In the previous research, generic federated learning algorithms provided by this framework were manually translated into the CSP processes and algorithms' safety and liveness properties were automatically verified by the model checker PAT. In this paper, a simple translation process is introduced wherein the ChatGPT is used to automate the translation of the mentioned federated learning algorithms in Python into the corresponding CSP processes. Within the process, the minimality of the used context is estimated based on the feedback from ChatGPT. The proposed translation process was experimentally validated by successful translation (verified by the model checker PAT) of both generic centralized and decentralized federated learning algorithms.

cs.AI↗

arXiv2025

Federated Isolation Forest for Efficient Anomaly Detection on Edge IoT Systems

Recently, federated learning frameworks such as Python TestBed for Federated Learning Algorithms and MicroPython TestBed for Federated Learning Algorithms have emerged to tackle user privacy concerns and efficiency in embedded systems. Even more recently, an efficient federated anomaly detection algorithm, FLiForest, based on Isolation Forests has been developed, offering a low-resource, unsupervised method well-suited for edge deployment and continuous learning. In this paper, we present an application of Isolation Forest-based temperature anomaly detection, developed using the previously mentioned federated learning frameworks, aimed at small edge devices and IoT systems running MicroPython. The system has been experimentally evaluated, achieving over 96% accuracy in distinguishing normal from abnormal readings and above 78% precision in detecting anomalies across all tested configurations, while maintaining a memory usage below 160 KB during model training. These results highlight its suitability for resource-constrained environments and edge systems, while upholding federated learning principles of data privacy and collaborative learning.

cs.LG↗

arXiv2024

Towards Formal Verification of Federated Learning Orchestration Protocols on Satellites

Python Testbed for Federated Learning Algorithms (PTB-FLA) is a simple FL framework targeting smart Internet of Things in edge systems that provides both generic centralized and decentralized FL algorithms, which implement the corresponding FL orchestration protocols that were formally verified using the process algebra CSP. This approach is appropriate for systems with stationary nodes but cannot be applied to systems with moving nodes. In this paper, we use celestial mechanics to model spacecraft movement, and timed automata (TA) to formalize and verify the centralized FL orchestration protocol, in two phases. In the first phase, we created a conventional TA model to prove traditional properties, namely deadlock freeness and termination. In the second phase, we created a stochastic TA model to prove timing correctness and to estimate termination probability.

cs.DC↗

arXiv2024

Fast Transaction Scheduling in Blockchain Sharding

Sharding is a promising technique for addressing the scalability issues of blockchain, and this technique is especially important for IoT, edge, or mobile computing. It divides the $n$ participating nodes into $s$ disjoint groups called shards, where each shard processes transactions in parallel. We examine batch scheduling problems on the shard graph $G_s$, where we find efficient schedules for a set of transactions. First, we present a centralized scheduler where one of the shards is considered as a leader, who receives the transaction information from all of the other shards and determines the schedule to process the transactions. For general graphs, where a transaction and its accessing objects are arbitrarily far from each other with a maximum distance $d$, the centralized scheduler provides $O(kd)$ approximation to the optimal schedule, where $k$ is the maximum number of shards each transaction accesses. Next, we provide a centralized scheduler with a bucketing approach that offers improved bounds for the case where $G_s$ is a line graph, or the $k$ objects are randomly selected. Finally, we provide a distributed scheduler where shards do not require global transaction information. We achieve this by using a hierarchical clustering of the shards and using the centralized scheduler in each cluster. We show that the distributed scheduler has a competitive ratio of $O(A_{CS} \cdot \log d \cdot \log s)$, where $A_{CS}$ is the approximation ratio of the centralized scheduler. To our knowledge, we are the first to give provably fast transaction scheduling algorithms for blockchain sharding systems. We also present simulation results for our schedulers and compare their performance with a lock-based approach. The results show that our schedulers are generally better with up to 3x lower latency and 2x higher throughput.

cs.DC↗

arXiv2024

MicroPython Testbed for Federated Learning Algorithms

Recently, Python Testbed for Federated Learning Algorithms emerged as a low code and generative large language models amenable framework for developing decentralized and distributed applications, primarily targeting edge systems, by nonprofessional programmers with the help of emerging artificial intelligence tools. This light framework is written in pure Python to be easy to install and to fit into a small IoT memory. It supports formally verified generic centralized and decentralized federated learning algorithms, as well as the peer-to-peer data exchange used in time division multiplexing communication, and its current main limitation is that all the application instances can run only on a single PC. This paper presents the MicroPyton Testbed for Federated Learning Algorithms, the new framework that overcomes its predecessor's limitation such that individual application instances may run on different network nodes like PCs and IoTs, primarily in edge systems. The new framework carries on the pure Python ideal, is based on asynchronous I/O abstractions, and runs on MicroPython, and therefore is a great match for IoTs and devices in edge systems. The new framework was experimentally validated on a wireless network comprising PCs and Raspberry Pi Pico W boards, by using application examples originally developed for the predecessor framework.

cs.DC↗

arXiv2024

Developing Elementary Federated Learning Algorithms Leveraging the ChatGPT

The Python Testbed for Federated Learning Algorithms is a simple Python FL framework easy to use by ML&AI developers who do not need to be professional programmers, and this paper shows that it is also amenable to emerging AI tools. In this paper, we successfully developed three elementary FL algorithms using the following three steps process: (i) specify context, (ii) ask ChatGPT to complete server and clients' callback functions, and (iii) verify the generated code.

cs.DC↗

arXiv2023

A Federated Learning Algorithms Development Paradigm

At present many distributed and decentralized frameworks for federated learning algorithms are already available. However, development of such a framework targeting smart Internet of Things in edge systems is still an open challenge. A solution to that challenge named Python Testbed for Federated Learning Algorithms (PTB-FLA) appeared recently. This solution is written in pure Python, it supports both centralized and decentralized algorithms, and its usage was validated and illustrated by three simple algorithm examples. In this paper, we present the federated learning algorithms development paradigm based on PTB-FLA. The paradigm comprises the four phases named by the code they produce: (1) the sequential code, (2) the federated sequential code, (3) the federated sequential code with callbacks, and (4) the PTB-FLA code. The development paradigm is validated and illustrated in the case study on logistic regression, where both centralized and decentralized algorithms are developed.

cs.DC↗

arXiv2023

A Simple Python Testbed for Federated Learning Algorithms

Nowadays many researchers are developing various distributed and decentralized frameworks for federated learning algorithms. However, development of such a framework targeting smart Internet of Things in edge systems is still an open challenge. In this paper, we present our solution to that challenge called Python Testbed for Federated Learning Algorithms. The solution is written in pure Python, and it supports both centralized and decentralized algorithms. The usage of the presented solution is both validated and illustrated by three simple algorithm examples.

cs.DC↗

arXiv2023

Correct orchestration of Federated Learning generic algorithms: formalisation and verification in CSP

Federated learning (FL) is a machine learning setting where clients keep the training data decentralised and collaboratively train a model either under the coordination of a central server (centralised FL) or in a peer-to-peer network (decentralised FL). Correct orchestration is one of the main challenges. In this paper, we formally verify the correctness of two generic FL algorithms, a centralised and a decentralised one, using the CSP process calculus and the PAT model checker. The CSP models consist of CSP processes corresponding to generic FL algorithm instances. PAT automatically proves the correctness of the two generic FL algorithms by proving their deadlock freeness (safety property) and successful termination (liveness property). The CSP models are constructed bottom-up by hand as a faithful representation of the real Python code and is automatically checked top-down by PAT.

cs.DC↗

arXiv2023

PSTM Transaction Scheduler Verification Based on CSP and Testing

Many online transaction scheduler architectures and algorithms for various software transactional memories have been designed in order to maintain good system performance even for high concurrency workloads. Most of these algorithms were directly implemented in a target programming language, and experimentally evaluated, without theoretical proofs of correctness and analysis of their performance. Only a small number of these algorithms were modeled using formal methods, such as process algebra CSP, in order to verify that they satisfy properties such as deadlock-freeness and starvation-freeness. However, as this paper shows, using solely formal methods has its disadvantages, too. In this paper, we first analyze the previous CSP model of PSTM transaction scheduler by comparing the model checker PAT results with the manually derived expected results, for the given test workloads. Next, according to the results of this analysis, we correct and extend the CSP model. Finally, based on PAT results for the new CSP model, we analyze the performance of PSTM online transaction scheduling algorithms from the perspective of makespan, number of aborts, and throughput. Based on our findings, we may conclude that for the complete formal verification of trustworthy software, both formal verification and it's testing must be jointly used.

cs.DC↗

arXiv2020

Electrical properties of thermal oxide scales on pure iron in liquid lead-bismuth eutectic

The impedance behavior of pre-oxidized iron in liquid lead-bismuth eutectic (LBE) at 200 oC is studied using electrochemical impedance spectroscopy. The structures and resistance of oxide grown on iron oxidized in air at different temperatures and durations are compared. The results show that the resistance of the oxide film increases with increasing oxidizing temperature, due to the formation of a thicker scale and fewer defects. At the same temperature (600 oC), increasing the oxidation time can also reduce the defect concentration in the oxide film and improve the impedance of the oxide scale in LBE.

physics.app-ph↗