arXiv subjects

Sumana Ghosh

Publications and source records attributed to Sumana Ghosh.

9 recordsLinked to original sources

arXiv2026

FORSLICE: An Automated Formal Framework for Efficient PRB-Allocation towards Slicing Multiple Network Services

Network slicing is a modern 5G technology that provides efficient network experience for diverse use cases. It is a technique for partitioning a single physical network infrastructure into multiple virtual networks, called slices, each equipped for specific services and requirements. In this work, we particularly deal with radio access network (RAN) slicing and resource allocation to RAN slices. In 5G, physical resource blocks (PRBs) being the fundamental units of radio resources, our main focus is to allocate PRBs to the slices efficiently. While addressing a spectrum of needs for multiple services or the same services with multi-priorities, we need to ensure two vital system properties: i) fairness to every service type (i.e., providing the required resources and a desired range of throughput) even after prioritizing a particular service type, and ii) PRB-optimality or minimizing the unused PRBs in slices. These serve as the core performance evaluation metrics for PRB-allocation in our work. We adopt the 3-layered hierarchical PRB-partitioning technique for allocating PRBs to network slices. The case-specific, AI-based solution of the state-of-the-art method lacks sufficient correctness to ensure consistent system performance. To achieve guaranteed correctness and completeness, we leverage formal methods and propose the first approach for a fair and optimal PRB distribution to RAN slices. We formally model the PRB-allocation problem as a 3-layered framework, FORSLICE, specifically by employing satisfiability modulo theories. Next, we apply formal verification to ensure that the desired system properties: fairness and PRB-optimality, are satisfied by the model. The proposed method offers an efficient, versatile and automated approach compatible with all 3-layered hierarchical network structure configurations, yielding significant system property improvements compared to the baseline.

cs.NI↗

arXiv2026

Precision Switching Schedule for Efficient Control Implementations

Modern cyber-physical systems, such as automotive control, rely on feedback controllers that regulate the system towards desired a setpoint. In practice, however, the controller must also be scheduled efficiently on resource-constrained processors, where the choice of numerical precision for controller implementation directly affects both control quality and computational cost. This trade-off is critical: higher precision improves control performance but increases runtime, while lower precision executes faster in the processor but may degrade overall system performance. In this work, we propose the first approach for a precision switching schedule, where the controller switches between different floating-point precisions to balance control performance and enhance computational efficiency. We formulate this problem as a multi-objective optimization, expressed as a Mixed-Integer Quadratic Program (MIQP) with sound linearizations and error bounds that capture roundoff effects from different precision implementations. Our method efficiently computes a switching schedule that ensures the system output remains within a specified reference band. Through experimental evaluation on standard benchmark control systems, we demonstrate that switching between 32-bit and 16-bit floating-point implementations offers an average runtime reduction of 26.5% compared to 32-bit execution and a 27.6% improvement in control performance over 16-bit execution, while maintaining near-optimal overall performance.

eess.SY↗

arXiv2026

MPBMC: Multi-Property Bounded Model Checking with GNN-guided Clustering

Formal verification of designs with multiple properties has been a long-standing challenge for the verification research community. The task of coming up with an effective strategy that can efficiently cluster properties to be solved together has inspired a number of proposals, ranging from structural clustering based on the property cone of influence (COI) to leverage runtime design and verification statistics. In this paper, we present an attempt towards functional clustering of properties utilizing graph neural network (GNN) embeddings for creating effective property clusters. We propose a hybrid approach that can exploit neural functional representations of hardware circuits and runtime design statistics to speed up the performance of Bounded Model Checking (BMC) in the context of multi-property verification (MPV). Our method intelligently groups properties based on their functional embedding and design statistics, resulting in speedup in verification results. Experimental results on the HWMCC benchmarks show the efficacy of our proposal with respect to the state-of-the-art.

cs.LO↗

arXiv2024

Configuring Safe Spiking Neural Controllers for Cyber-Physical Systems through Formal Verification

Spiking Neural Networks (SNNs) are a subclass of neuromorphic models that have great potential to be used as controllers in Cyber-Physical Systems (CPSs) due to their energy efficiency. They can benefit from the prevalent approach of first training an Artificial Neural Network (ANN) and then translating to an SNN with subsequent hyperparameter tuning. The tuning is required to ensure that the resulting SNN is accurate with respect to the ANN in terms of metrics like Mean Squared Error (MSE). However, SNN controllers for safety-critical CPSs must also satisfy safety specifications, which are not guaranteed by the conversion approach. In this paper, we propose a solution which tunes the $temporal$ $window$ hyperparameter of the translated SNN to ensure both accuracy and compliance with the safe range specification that requires the SNN outputs to remain within a safe range. The core verification problem is modelled using mixed-integer linear programming (MILP) and is solved with Gurobi. When the controller fails to meet the range specification, we compute tight bounds on the SNN outputs as feedback for the CPS developer. To mitigate the high computational cost of verification, we integrate data-driven steps to minimize verification calls. Our approach provides designers with the confidence to safely integrate energy-efficient SNN controllers into modern CPSs. We demonstrate our approach with experimental results on five different benchmark neural controllers.

cs.ET↗

arXiv2024

Study of ion induced Inner Shell Ionization cross section through electron capture mechanism

Electron Capture (EC) cross-section from K, L and M shells of the target atoms to the vacant K, L and M shells of the projectile ions have been calculated by deriving the accurate momentum transfer to the captured electrons for different charge states. Several correction factors like polarization correction, relativistic effects (R) of the target wave function, Coulomb-deflection factor (C) due to the effect of the repulsion between the projectile and the target nucleus, correction for projectile energy loss have been introduced. The mean charge state of the projectiles inside the target material has been estimated using suitable empirical models and the fractional charge state distribution has been calculated considering Lorentz distribution. Fractional distribution of charge state of the projectile ions is used to obtain the charge state contributions of the electron capture cross-sections. The effect of Simultaneous Multiple Ionization (SMI) has been considered in the theory of Direct Coulomb Ionization (DCI). The theoretically obtained total cross-sections have been compared with the experimental findings obtained from various literature. The computation scheme has been depicted through sample calculations of ionization cross-sections through electron capture mechanism.

physics.atom-ph↗

arXiv2023

Study of bremsstrahlung radiation coming from a transmission type x-ray generator and its application on EDXRF technique

We have demonstrated the use of the bremsstrahlung radiation in energy dispersive x-ray fluorescence technique as a tool to perform non-destructive elemental analysis of solid samples employed in inter-disciplinary science research. The bremsstrahlung radiation can be taken from a small, portable, transmission type x-ray generator. As our knowledge goes, till date, this is the first attempt to generate bremsstrahlung spectrum theoretically from a portable transmission type x-ray generator and compared it with the actual observation. Theoretically generated bremsstrahlung spectra are also found to be in good agreement with the experimentally observed spectra obtained with various operating anode voltages of the x-ray generator. A computer program has been developed utilizing few atomic parameters to obtain the elemental concentrations in the sample by a single run using the whole bremsstrahlung. The knowledge of incoming x-ray flux, geometry of experimental arrangements is not required in this technique. To validate the technique, we have taken two samples: an Indian one rupee coin of the year 2000 and a NIST made brass sample, whose compositions are well known. We used these samples to expose to the bremsstrahlung radiation, produced by the operating anode voltages 20, 25, and 30 KV. The relative concentrations of different elements are determined, which is in good agreement with the earlier results.

physics.ins-det↗

arXiv2022

Theoretical studies on multiple ionisation and electron capture processes in heavy ion induced M-shell ionisation

Multiple ionisation and electron capture are found to be vital mechanisms for K and L x-ray emissions along with the direct coulomb ionisation in heavy ion-atom collisions. Naturally, these two mechanisms may also be significant for M x-ray emissions also. However, these mechanisms associating with the M-shell are highly complex and not yet studied convincingly. We, in this work, have discussed about theoretical techniques to study these mechanisms in more general way, which in turn, almost resolved the wide gap between the theories and experiments regarding M-shell prevalent in literature up to a good extent. We have justified this technique with a few representative cases; for example, the silicon and sulphur projectile ions colliding with the gold and bismuth targets at beam energies ranging from 5 to 10 MeV. Here, we see that the capture contribution is much higher than that coming from the multiple ionisation effect. The combined effects of direct coulomb ionisation associated with simultaneous multiple ionisation and electron capture give a better agreement with the measurements up to a good extent.

physics.atom-ph↗

arXiv2020

Skip to Secure: Securing Cyber-physical Control Loops with Intentionally Skipped Executions

We consider the problem of provably securing a given control loop implementation in the presence of adversarial interventions on data exchange between plant and controller. Such interventions can be thwarted using continuously operating monitoring systems and also cryptographic techniques, both of which consume network and computational resources. We provide a principled approach for intentional skipping of control loop executions which may qualify as a useful control theoretic countermeasure against stealthy attacks which violate message integrity and authenticity. As is evident from our experiments, such a control theoretic counter-measure helps in lowering the cryptographic security measure overhead and resulting resource consumption in Control Area Network (CAN) based automotive CPS without compromising performance and safety.

cs.CR↗

arXiv2018

Time Evolution of Density Parameters for Matter and Dark Energy and their Interaction Term in Brans-Dicke Gravity

In the framework of Brans-Dicke (BD) theory, the first part of the present study determines the time dependence of BD parameter, energy density and equation of state (EoS) parameter of the cosmic fluid in a universe expanding with acceleration, preceded by a phase of deceleration. For this purpose, a scale factor has been chosen such that the deceleration parameter, obtained from it, shows a signature flip with time. Considering the dark energy to be responsible for the entire pressure, the time evolution of energy parameters for matter and dark energy and the EoS parameter for dark energy have been determined. An effective interaction term, between matter and dark energy, has been proposed and calculated. Its negative value at the present time indicates conversion of matter into dark energy. Using this term, the time dependence of the rates of change of matter and dark energy has been determined. It is found that the nature of dependence of the scalar field upon the scale factor plays a very important role in governing the time evolution of the cosmological quantities studied here. The present study provides us with a simple way to determine the time evolution of dark energy for a homogeneous and isotropic universe of zero spatial curvature, without involving any self-interaction potential or cosmological constant in the formulation.

gr-qc↗