Indoor localization technology has become increasingly crucial as the demand for precise and reliable positioning systems grows across various applications. Traditional methods, such as vision-based techniques, radio signal-based technologies (including UWB, WiFi, RFID, and Bluetooth), and visible light-based technologies, offer unique advantages and limitations. Among these, visible light positioning (VLP) stands out for its potential to provide high accuracy by leveraging the characteristics of light signals.

This thesis explores the integration of VLP with a balloon-enabled drone—a novel UAV setup featuring a buoyant balloon that extends flight duration. A balloon-enabled drone introduces both opportunities and challenges for VLP methods due to its size. Its large surface area can block light paths, which may impact signal reception and positioning accuracy. On the other hand, it also allows for the use of multiple receivers across the surface, potentially improving positioning reliability.

Traditional VLP systems typically utilize multiple transmitters and a single receiver; however, our approach takes advantage of the large surface area of a balloon-enabled drone by using only a single transmitter with multiple receivers strategically positioned on the balloon. This setup leverages the balloon’s curved surface to capture a diverse range of light intensities and angles, thereby improving positioning accuracy. We developed a 2D+H RSS-based VLP model specifically designed for balloon-enabled drones. This model takes into account factors like light transmission and optical channel loss. Our VLP system includes multiple receivers placed on the balloon’s surface and a single transmitter. We analyzed the optimal number and placement of these receivers to enhance positioning accuracy.

The system’s performance was tested through both static and dynamic experiments. In static tests, our configuration achieved an average positioning error of 4 cm. During dynamic tests, which involved movement and tilt, the mean error increased to 10-12 cm, largely due to difficulties in estimating height and managing tilt angles. Overall, our system shows an improvement over existing positioning methods like Crazyflie, while also maintaining low energy consumption and computational complexity. This work highlights the potential of our VLP model to improve the positioning accuracy of balloon-enabled drones for various applications.

The formal verification of concurrent programs is of particular importance, because concurrent programs are notoriously difficult to test. Because Haskell is a purely functional language, it is relatively easy to reason about the correctness of such programs and write down manual proofs. However, since these methods are still prone to error, this paper investigates how Agda2hs can be used to automate the verification process in Agda, while keeping the advantages of having our code available in Haskell. This paper shows how Agda2hs enables the partial verification of a simple Haskell concurrency model. The model is first ported to Agda, staying as close to the original code as possible, and directly compared to the Haskell translation provided by Agda2hs to showcase the readability of the code it produces. Consequently, it is shown how Agda's proof techniques can be used to provide straightforwards proofs of the presence or absence of deadlocks in simple concurrent programs written in this model. Finally, the model's limitations, in particular its deterministic nature, are discussed.