GPS has long been the standard for determining position and navigation across a wide range of applications. However, as this technology cannot be relied on in many scenarios, alternative sensing modalities, such as vision, could provide viable alternatives. This work investigated the use of an event-based camera for navigation, within a mobile embedded system. Event-based cameras generate events when pixels asynchronously detect changes in light intensity, and report these changes as binary spikes. Such sensors can provide very high temporal resolution, wide dynamic range and low power consumption. A ground-based rover was developed, hosting a DAVIS346 event-based camera, to test a navigation system based on a visual-inertial odometry (VIO) approach. Processing and communications were implemented on two microcontrollers (Raspberry Pi 5 and ESP32), both communicating with a base station, which tracked the position of the rover and status of onboard sensors. The event-based processing pipeline showed improved accuracy when using frames augmented with event data, as compared to regular frames only. Due to the scarcity of modular, open source, event-based VIO systems, this work focused on how the benefits of an event-based camera could be leveraged in OpenVINS, which is a traditional VIO system designed for conventional frame-based cameras. To the best of our knowledge this is the first demonstration of a framework that can leverage the benefits of an event-based camera in a traditional VIO system of this style.

Cyber attacks on Industrial Control Systems (ICSs) are becoming increasingly sophisticated, undermining the ability of these systems to manage critical processes and compromising the availability of key public infrastructure. Detecting system anomalies is an important element in the identification of cyber attacks, allowing the rapid deployment of crucial incident-response activities. In this paper, we introduce a novel anomaly detection approach that integrates SPIN model checking into ICS environments to detect anomalies in live system data. Our approach uses the application code extracted from Programmable Logic Controllers (PLCs) to generate the dynamic system model, requiring only a small amount of test data to validate their design. We evaluate our approach by generating models using a representative physical hydroelectric dam testbed containing real PLCs. These models are used to analyse synthetic data containing potential irregularities that could occur within the dam as a result of false data injection attacks. Our approach was shown to identify anomalies and verify normal system behaviour. Our evaluation shows that the models achieved high performance while maintaining explainability and delivering metrics of 99.99% precision, 99.05% recall, a 99.52% F1-score, and 99.05% accuracy.

Fast and reliable trajectory planning is a key requirement of autonomous vehicles. In this paper we introduce a novel technique for planning the route of an autonomous vehicle on a straight, traffic-heavy rural road using the SPIN model checker. We show how we can combine SPIN's ability to identify paths violating temporal properties with sensor information from a 3D Unity simulation of an autonomous vehicle, to plan and perform consecutive overtaking manoeuvres. This involves discretising the sensory information and combining multiple sequential SPIN models with a Linear-time Temporal Logic specification to generate an error path. This path provides the autonomous vehicle with an action plan. The entire process is fast (using no precomputed data) and the action plan is tailored for individual scenarios. Our experiments demonstrate that the simulated autonomous vehicle implementing our approach can drive a median of 37 km and overtake a median of 187 vehicles before experiencing a collision - which is usually caused by inaccuracies in the sensory system. We also describe a memoisation approach which helps to mitigate one of the drawbacks of our approach - the cost of model compilation. Our novel approach demonstrates a potentially powerful future tool for efficient trajectory planning for autonomous vehicles.

Abstract We show how detailed simulation models and abstract Markov models can be developed collaboratively to generate and implement effective controllers for autonomous agent search and retrieve missions. We introduce a concrete simulation model of an Unmanned Aerial Vehicle (UAV). We then show how the probabilistic model checker PRISM is used for optimal strategy synthesis for a sequence of scenarios relevant to UAVs and potentially other autonomous agent systems. For each scenario we demonstrate how it can be modelled using PRISM, give model checking statistics and present the synthesised optimal strategies. We then show how our strategies can be returned to the controller for the simulation model and provide experimental results to demonstrate the effectiveness of one such strategy. Finally we explain how our models can be adapted, using symmetry, for use on larger search areas, and demonstrate the feasibility of this approach.