Practical Verification of Lenses: Implementing Formally Verified Lenses using agda2hs

agda2hs is a tool which translates a subset of Agda to readable Haskell. Using agda2hs, programmers can implement libraries in this subset of Agda, formally verify them, and then convert them to Haskell. In this paper we present a new, verified implementation of the lens data type, which is used to access data structures in a readable yet...

Practical Verification of Concurrent Haskell Programs

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,...

Practical Verification of Infinite Structures in agda2hs

Agda allows for writing code that can be mathematically proven and verified to be correct, this type of languages is generally known as a proof assistant. The agda2hs library makes an effort to translate Agda to readable Haskell, in a way the Haskell is still consistent. In previous work it is shown that with the current agda2hs implementation,...

Constructing A Dataset For Gesture Recognition Using Ambient Light

Public technology has been shown to have a strong dependence on physical touch, which increases the transmission of diseases. Gesture recognition helps to reduce this transmission, as the dependence on physical touch is removed. Furthermore, the use of visible light for gesture recognition would reduce the power consumption of public technology,...

Characterising AI Weakness in Detecting Personal Data from Images By Crowds

This thesis looks at how to characterize weaknesses in machine learning models that are used for detecting privacy-sensitive data in images with the help of crowdsourcing. Before we can come up with a method to achieve a goal, we first need to make clear what we consider privacy-sensitive data. We took the General Data Protection Regulation ...

Reducing wireless control communication for a water irrigation system

For this thesis we have compared communication times of different control schemes on a wireless control network for a water irrigation system. Therefore a control application which can run different protocols was created. We have shown that a significant reduction of communication time can be achieved by using event-triggered control (ETC), and...

Optimizing Edge Computing in 5G Networks

Multi-access Edge Computing (MEC) is a concept brought up by ETSI and it places computing, storage, processing and network resources into MEC hosts and places these MEC hosts as close as needed to the telecom network edge in order to reduce service latency and bandwidth usage. For self-driving vehicles, streaming video and real-time gaming, the...

Adaptive Real-Time PPG Signal Qualification and Pulse Segmentation

Ever since its invention in the 1930s, photoplethysmography (PPG) is a wide-spread technique used for health-monitoring. Via illumination of the human skin with a light source and capturing the light, an estimate of important physiological properties such as the heart rate can be made. This is commonly done with dedicated medical equipment, but...

IMS in 5G: Analysis of IMS based communication services in the 5G network

The thesis focuses on investigating the role of IP Multimedia Subsystem (IMS) in 5G networks. IMS already plays a very important role in enabling a wide range of real-time multimedia communication services such as basic phone calls and messaging in the LTE network. Addition of application servers on top of the IMS core can provide enhanced...

A New Type Of Medium Access Control For Event Driven Energy Harvesting Devices

We present a new MAC protocol for networks of devices. We specifically target certain applications. To cater for this setting, we introduce a new concept. This concept is instrumental to improve performance in these network scenarios. We build a proof of concept implementation of the new mac protocol. We specifically present a protocol model and...