Electric infrastructures have been pushed forward to handle tasks they were not originally designed to perform. To improve reliability and efficiency, state-of-the-art power grids include improved security, reduced peak loads, increased integration of renewable sources, and lower operational costs. In this framework“, smart grids” are built around bidirectional communication technologies, where “smart meters” communicate with all other entities and collect data from the power grid, offering specific features to each actor playing in the energy marketplace. In this paper, to overcome some of the challenges raised by smart grids and smart meters, we propose a distributed metering infrastructure which provides bidirectional communication, self-configuration, and auto-update capabilities. Our 3-phase smart meters follow the basics Internet-of-Things principles and have the ability to run, either on-board or distributed on the network, multiple algorithms for smart grid management. These algorithms can be freely added, updated, or removed on-the-fly thanks to the auto-update feature of the system. Moreover, to reduce costs and improve scalability, we prove that it is possible to implement our smart meters using only off-the-shelf and inexpensive hardware devices. A digital real-time simulator (i.e., Opal-RT) has been used to assess the capabilities of both the infrastructure and the meter. Our experimental analysis shows that the latency introduced by the data transmission over the Internet is compliant with the limits imposed by the IEC 61850 standard. As a consequence, our architecture does not affect the operational status of the smart grid, making it a viable solution to support the deployment of novel services.

This paper presents a solution to the problem of reducing the power dissipated by a digital system containing an intellectual proprietary core processor which repeatedly executes a special-purpose program. The proposed method relies on a novel, application-dependent low-power address bus encoding scheme. The analysis of the execution traces of a given program allows an accurate computation of the correlations that may exist between blocks of bits in consecutive patterns; this information can be successfully exploited to determine an encoding which sensibly reduces the bus transition activity. Experimental results, obtained on a set of special-purpose applications, are very satisfactory; reductions of the bus activity up to 64.8% (41.8% on average) have been achieved over the original address streams. In addition, data concerning the quality and the performance of the automatically synthesized encoding/decoding circuits, as well as the results obtained for a realistic core-based design, indicate the practical usefulness of the proposed power optimization strategy.

Air quality, especially particulate matter, has recently attracted a lot of attention from governments, industry, and academia, motivating the use of denser air quality monitoring networks based on low-cost sensing strategies. However, low-cost sensors are frequently sensitive to aging, environmental conditions, and pollutant cross-sensitivities. These issues have been only partially addressed, limiting their usage. In this study, we develop a low-cost particulate matter monitoring system based on special-purpose acquisition boards, deployed for monitoring air quality on both stationary and mobile sensor platforms. We explore the influence of all model variables, the quality of different calibration strategies, the accuracy across different concentration ranges, and the usefulness of redundant sensors placed in each station. The collected sensor data amounts to about 50GB of data, gathered in six months during the winter season. Tests of statically immovable stations include an analysis of accuracy and sensors reliability made by comparing our results with more accurate and expensive standard - radiation sensors. Tests on mobile stations have been designed to analyze the reactivity of our system to unexpected and abrupt events. These experiments embrace traffic analysis, pollution investigation using different means of transport and pollution analysis during peculiar events. With respect to other approaches, our methodology has been proved to be extremely easy to calibrate, to offer a very high sample rate (one sample per second), and to be based on an open-source software architecture. Database and software are available as open source in [1].

Binary Decision Diagrams (BDDs) have been widely used for hardware verification since the beginning of the '90s, whereas Boolean Satisfiability (SAT) has been gaining ground more recently, with the introduction of Bounded Model Checking (BMC). In this paper we dovetail BDD and SAT based methods to improve the efficiency of BMC More specifically, we first exploit inexpensive symbolic approximate reachability analysis to gather information on the state space. We then use the above information to restrict and focus the overall search space of SAT based BMC. In the experimental results section we show how the information coming from a BDD tool can improve the efficiency of a SAT engine by drastically reducing the number of "variable assignments" and "variable conflicts". This results in a significant overall performance gain associated with a general, robust, and easy-to-apply methodology.