Localization systems play a major role in many applications for Vehicular Ad Hoc Networks (VANETs). One of the most interesting problems to be solved in vehicular networks is how to provide anywhere and anytime highly accurate and reliable localization information. Unique characteristics of VANETs such as mobility constraints, driver’s behavior and the high-speed displacement nature of vehicles cause rapid and constant changes in network topology, leading to dissemination of outdated localization information. To circumvent this problem, an alternative is the use of predicted future locations of vehicles. The main idea of this approach is to use the localization prediction as an extension of a data fusion localization system. In such an approach, a future position of a vehicle is predicted for a given future time and used to take advantage of a future time-space window of a vectorial trajectory rather than a static localization point. In this paper, we discuss this subject by studying and analyzing the use of localization prediction as natural way to improve VANET applications. We survey proposed approaches for localization, target tracking and time series prediction techniques that can be used to estimate the future position of a vehicle. We also highlight their advantages and disadvantages through an analytical discussion visualizing its potential application scenarios in VANETs. We present a set of experiments that show the results of such techniques when applied to a realistic VANET scenario.

This work proposes a new indoor positioning system, named KLIP, that uses the ${K}$ -means clustering algorithm to split the environment into different sets of log-distance propagation models in order to better characterize the indoor environment and further improve the position estimation using Bayesian inference. Our proposed method is validated in a large-scale, real-world scenario composed of Bluetooth Low Energy (BLE)-based devices. We demonstrate, throughout the paper, that the addition of location information of training points to the received signal strength indicator (RSSI) as an attribute for the clustering step improves the positioning accuracy. Moreover, the obtained results show that our solution outperforms the naive Bayesian estimation up to 12% – regarding the positioning accuracy – and the broadly deployed ${k}$ NN for reduced training dataset size – regarding both accuracy and online processing time. In this sense, KLIP proves to be an efficient and scalable alternative when both site-survey effort and energy consumption constraints must be taken into account.

Indoor positioning systems (IPSs) allow the location and tracking of mobile devices in indoor environments where the global positioning system (GPS) does not provide satisfactory results. In model-based IPSs, it is common to use signal propagation models to estimate distances between anchor nodes and mobile devices using the received signal strength indicator (RSSI). However, using fixed parameters in the path loss model to characterize the signal in large-scale scenarios results in the degradation of the positioning accuracy. In this article, we propose the adaptive model (ADAM) positioning system, a model-based IPS that chooses the best anchor nodes to benefit the positioning computation and uses different parameters for the log-distance model to represent the signal in different regions and conditions of the scenario. Then, we estimate a single, more precise position using a data fusion technique. Our proposal does not require training nor prior knowledge of the best parameters for each region. We evaluated the performance of our proposed system in a real-world, large-scale environment using Bluetooth-based mobile devices. Our results clearly show that ADAM can locate mobile devices with an average error of 2.93 m in relation to the real position, which is 23% better than literature-based models using fixed parameters for the entire environment.

Indoor Positioning Systems (IPSs) have emerged as a research topic in mobile computing, enabling the tracking and location of mobile devices within indoor environments. In model-based IPSs, the Received Signal Strength Indicator (RSSI) is used to estimate the distance between wireless signal receivers and transmitters using signal propagation models. However, the indoor environment presents challenges that make distance estimation using RSSI difficult. In this paper, we propose a new indoor positioning system that combines Particle Swarm Optimization (PSO) with signal propagation models to improve the accuracy of mobile device positioning. The PSO algorithm is used to optimize the position estimation process by generating different particles in the map, while the signal propagation model is used to model the attenuation and reflection of wireless signals in each particle. Our MIPS-PSO system does not require any prior training nor any knowledge of the best parameters of the signal propagation model. We evaluated the performance of our system using data collected in a real indoor environment with Bluetooth-Low-Energy (BLE) devices. Our results show that the MIPS-PSO achieves an average error of 2.57 m, an improvement of 40% when compared to a traditional trilateration, model-based IPS.

We present a proof by induction algorithm, which combines k-induction with invariants to model check embedded C software with bounded and unbounded loops. The k-induction algorithm consists of three cases: in the base case, we aim to find a counterexample with up to k loop unwindings, in the forward condition, we check whether loops have been fully unrolled and that the safety property ø holds in all states reachable within k unwindings, and in the inductive step, we check that whenever ø holds for k unwindings, it also holds after the next unwinding of the system. For each step of the k-induction algorithm, we infer invariants using affine constraints (i.e., polyhedral) to specify pre-and post-conditions. Experimental results show that our approach can handle a wide variety of safety properties in typical embedded software applications from telecommunications, control systems, and medical devices, we demonstrate an improvement of the induction algorithm effectiveness if compared to other approaches.