To incentivize solar panel adaptation, a multitude of solutions are actively being researched. Among these solutions are colored solar cells, using coatings or filters to open the door for more architectural expression. In order to help architects explore these possibilities, it is necessary to enable flexible, fast, and realistic visualization. This work explores the modeling of color-coated photovoltaic cells using a physically based bidirectional reflectance distribution function (BRDF), with a focus on the pyramidically textured structures embedded inside many of these cells. The BRDF is analytically derived, modeling light interactions as recursively specular multiple-scattering. The model is parametric, characterizing the surface using its pyramid density and pyramid slant angle, making it generally applicable to homogeneous pyramidic surfaces with uniform pyramid heights. Evaluation indicates the model closely approximates the behavior of generated references at steep viewing angles. Clear avenues of improvement, including corrections at shallow angles, are discussed within the context of future work.

Previous literature had accentuated the importance of close ground infrastructure (Ground Stations and Points of presence) on the network performance of Starlink. In order to further investigate this relation, a new method was defined, based on IPv4traceroute, to identify the PoP associated with a Starlink user. This method has been evaluated for 95 RIPE Atlas probes connected to the Starlink network and the results have been mapped in an interactive web-tool. Using this data, a strong correlation between latency and proximity to ground infrastructure was verified.

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.