More Like this

1. STAMINA in C++: Modernizing an Infinite-State Probabilistic Model Checker

   https://doi.org/10.1007/978-3-031-43835-6_7  

   Jeppson, Josh; Volk, Matthias; Israelsen, Bryant; Roberts, Riley; Williams, Andrew; Buecherl, Lukas; Myers, Chris J; Zheng, Hao; Winstead, Chris; Zhang, Zhen (September 2023, Lecture notes in computer science)

   Jansen, N; Tribastone, M (Ed.)

   Improving the scalability of probabilistic model checking (PMC) tools is crucial to the verification of real-world system designs. The STAMINA infinite-state PMC tool achieves scalability by iteratively constructing a partial state space for an unbounded continuous-time Markov chain model, where a majority of the probability mass resides. It then performs time-bounded transient PMC. It can efficiently produce an accurate probability bound to the property under verification. We present a new software architecture design and the C++ implementation of the STAMINA 2.0 algorithm, integrated with the STORM model checker. This open-source STAMINA implementation offers a high degree of modularity and provides significant optimizations to the STAMINA 2.0 algorithm. Performance improvements are demonstrated on multiple challenging benchmark examples, including hazard analysis of infinite-state combinational genetic circuits, over the previous STAMINA implementation. Additionally, its design allows for future customizations and optimizations to the STAMINA algorithm. 

   more » « less
2. Engineering Blockchain-Based Narrowband Internet of Things Applications for Energy Optimization

   https://doi.org/10.1007/978-3-031-87781-0_24  

   Kakar, Hafizullah; Mohan, Vamshi S; Roy, Swapnoneel; Dutta, Ayan; Kreidl, O Patrick; Bölöni, Ladislau; Sankaran, Sriram (January 2025, Springer Nature Switzerland)

   We optimize the overall energy consumption of a Narrowband Internet of Things (NB-IoT) application created using a hybrid blockchain framework. We accomplish this by engineering the underlying hash function (SHA-256) that is used in different procedures (Unique ID generation, Device Join, and Device Transaction) of the blockchain-based NB-IoT system. In order to reduce the complexity of hash verification, IoT devices in the NB-IoT application are built to save the hashes of their authorized transactions as a linear hash chain rather than the entire Merkle tree. Furthermore, base station memory is dynamically partitioned to improve memory usage efficiency and scalability. Compared with the state-of-the-art approach, our approach considerably reduces the total energy consumption of the state-of-the-art application. 

   more » « less
3. Improving Performance and Scalability of Algebraic Multigrid through a Specialized MATVEC

   Majid Rasouli, Vidhi Zala (September 2018, IEEE High Performance Extreme Computing Conference)

   Algebraic Multigrid (AMG) is an extremely popular linear system solver and/or preconditioner approach for matrices obtained from the discretization of elliptic operators. However, its performance and scalability for large systems obtained from unstructured discretizations seem less consistent than for geometric multigrid (GMG). To a large extent, this is due to loss of sparsity at the coarser grids and the resulting increased cost and poor scalability of the matrix-vector multiplication. While there have been attempts to address this concern by designing sparsification algorithms, these affect the overall convergence. In this work, we focus on designing a specialized matrix-vector multiplication (matvec) that achieves high performance and scalability for a large variation in the levels of sparsity. We evaluate distributed and shared memory implementations of our matvec operator and demonstrate the improvements to its scalability and performance in AMG hierarchy and finally, we compare it with PETSc. 

   more » « less
4. To Probe Full and Partial Activation of Human Peroxisome Proliferator-Activated Receptors by Pan-Agonist Chiglitazar Using Molecular Dynamics Simulations

   https://doi.org/10.1155/2020/5314187  

   Sullivan, Holli-Joi; Wang, Xiaoyan; Nogle, Shaina; Liao, Siyan; Wu, Chun (April 2020, PPAR Research)

   Chiglitazar is a promising new-generation insulin sensitizer with low reverse effects for the treatment of type II diabetes mellitus (T2DM) and has shown activity as a nonselective pan-agonist to the human peroxisome proliferator-activated receptors (PPARs) (i.e., full activation of PPAR γ and a partial activation of PPAR α and PPAR β / δ ). Yet, it has no high-resolution complex structure with PPARs and its detailed interactions and activation mechanism remain unclear. In this study, we docked chiglitazar into three experimentally resolved crystal structures of hPPAR subtypes, PPAR α , PPAR β / δ , and PPAR γ , followed by 3  μ s molecular dynamics simulations for each system. Our MM-GBSA binding energy calculation revealed that chiglitazar most favorably bound to hPPAR γ (-144.6 kcal/mol), followed by hPPAR α (-138.0 kcal/mol) and hPPAR β (-135.9 kcal/mol), and the order is consistent with the experimental data. Through the decomposition of the MM-GBSA binding energy by residue and the use of two-dimensional interaction diagrams, key residues involved in the binding of chiglitazar were identified and characterized for each complex system. Additionally, our detailed dynamics analyses support that the conformation and dynamics of helix 12 play a critical role in determining the activities of the different types of ligands (e.g., full agonist vs. partial agonist). Rather than being bent fully in the direction of the agonist versus antagonist conformation, a partial agonist can adopt a more linear conformation and have a lower degree of flexibility. Our finding may aid in further development of this new generation of medication. 

   more » « less
5. Blockchain-Driven Privacy-Preserving Contact-Tracing Framework in Pandemics

   https://doi.org/10.1109/TCSS.2024.3351191  

   Li, Xiao; Wu, Weili; Chen, Tiantian (June 2024, IEEE Transactions on Computational Social Systems)

   Blockchain technology, recognized for its decentralized and privacy-preserving capabilities, holds potential for enhancing privacy in contact tracing applications. Existing blockchain-based contact tracing frameworks often overlook one or more critical design details, such as the blockchain data structure, a decentralized and lightweight consensus mechanism with integrated tracing data verification, and an incentive mechanism to encourage voluntary participation in bearing blockchain costs. Moreover, the absence of framework simulations raises questions about the efficacy of these existing models. To solve above issues, this article introduces a fully third-party independent blockchain-driven contact tracing (BDCT) framework, detailed in its design. The BDCT framework features an RivestShamir-Adleman (RSA) encryption-based transaction verification method (RSA-TVM), achieving over 96% accuracy in contact case recording, even with a 60% probability of individuals failing to verify contact information. Furthermore, we propose a lightweight reputation corrected delegated proof of stake (RCDPoS) consensus mechanism, coupled with an incentive model, to ensure timely reporting of contact cases while maintaining blockchain decentralization. Additionally, a novel simulation environment for contact tracing is developed, accounting for three distinct contact scenarios with varied population density. Our results and discussions validate the effectiveness, robustness of the RSA-TVM and RC-DPoS, and the low storage demand of the BDCT framework. 

   more » « less