Search for: All records

Abstract Traditional piezoelectric materials, such as lead zirconate titanate (PZT), are widely used due to their superior ability to convert mechanical energy into electrical energy. However, these lead-based ceramics are highly toxic and environmentally hazardous. This report explores Rochelle salt as an eco-friendly alternative, despite its brittleness and lower piezoelectric properties compared to PZT. The study investigates methods to enhance the energy capture of Rochelle salt crystals(RS) by varying crystal volume, impact frequency, and force, as well as by incorporating the 3D-printed biomimetic structure inspired by the pomelo fruit peel, which is naturally optimized for absorbing out-of-plane crushing forces. Experimental crystals grown within this structure were compared with those grown without it, focusing on energy capture and durability. Additionally, units with a 64:36 crystal-to-resin ratio were designed to assess the impact of crystal volume on voltage output. The experiments involved varying impact frequencies (120 rpm and 250 rpm) and compression distances (0.034 and 0.068 inches) using a digital oscilloscope and a custom crank slider mechanism. The results indicate that reducing crystal thickness and increasing rpms enhance voltage capture, suggesting that biomimetic structures can significantly improve the mechanical and electrical performance of piezoelectric materials. 

Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP. 

Preaxial dominance in the mesopodium is limited to distal carpals/tarsals and facilitates digit reduction in early tetrapods. 

Fortran is widely used in computational science, engineering, and high performance computing. This paper presents an extension to the CIVL verification framework to check correctness properties of Fortran programs. Unlike previous work that translates Fortran to C, LLVM IR, or other intermediate formats before verification, our work allows CIVL to directly consume Fortran source files. We extended the parsing, translation, and analysis phases to support Fortran-specific features such as array slicing and reshaping, and to find program violations that are specific to Fortran, such as argument aliasing rule violations, invalid use of variable and function attributes, or defects due to Fortran's unspecified expression evaluation order. We demonstrate the usefulness of our tool on a verification benchmark suite and kernels extracted from a real world application. 

In many packet-switched wireless systems including cellular networks, RObust Header Compression (ROHC) plays an important role in improving payload efficiency by reducing the number of header bits in a link session. However, there are only very few research works addressing the optimized control of ROHC. Our recent studies have demonstrated the advantage of a trans-layer ROHC design that exploits lower layer link status. We have presented a unidirectional ROHC design based on a partially observable Markov decision process formulation that enables the transmitter to decide the header compression level without receiver feedback. The present work considers the physical channel dynamics in an LTE environment and how they affect header decompressor status. Our new model takes into consideration the transport block (TBs) size defined in LTE transmission according to the modulation and coding scheme (MCS). Our novel and practical model can significantly improve the efficiency of the transmission when compared to a traditional timer-based ROHC control.