Zero Overhead Verification of Software Programs & On Range Search in Distributed Sensor Networks

Опубликовано 6 сентября 2016, 17:20

Zero Overhead Online Verification of Software Programs The PSL-to-Verilog compiler can translate a set of assertions about a block-structured software program into a hardware design to be executed concurrently with the execution of the software program. The assertions are expressed in a subset of the IEEE standard Property Specification Language PSL. The target execution system is the eMIPS processor, a dynamically self-extensible processor realized with an FPGA. Assertions are compiled into eMIPS Extensions. They can be loaded and unloaded at runtime, and validate the correctness of the software program without altering its temporal behavior. The system is currently used to verify software properties in areas such as testing and debugging, intrusion detection, and the behavioral verification of concurrent and realtime programs. On Range Search in Distributed Sensor Networks Sensor networks have been widely deployed for data collection, in-network processing and distributed control. Sensor nodes are often small embedded devices with limited energy supply and memories, which makes it a challenging task to store and retrieve data efficiently. A range query asks for all the data items in a region of the sensor network field. This talk addresses the inherent tradeoff between the storage and retrieval cost to answer range queries. We propose an algorithm with a general retrieval cost function with optimized storage overhead, and prove that logarithm storage is asymptotically optimal to achieve linear retrieval. The result also applies to a few other problems such as distributed location service and information brokerage.