As Industry 4.0 drives the Fourth Industrial Revolution, Cyber-Physical Systems (CPSs) have become central to industrial automation. These systems integrate software with physical processes, significantly improving the efficiency and adaptability. However, this integration also expands the attack surface, exposing systems to Cyber-Physical-attacks (CP-attacks) that can target either the computational components, physical devices, or both. The impact of such attacks can be catastrophic, ranging from system disruption to physical damage. Although numerous techniques have been developed to detect and mitigate these threats, industrial standards are often not incorporated into the design of these methods. This limits their deployment within the Industry 4.0 systems, where standard compliance is critical.

Automatic detection of cardiac arrhythmia is an important tool in the fight against cardiovascular diseases and their associated human impacts. Such detection needs to be both accurate and timely, in order to allow for interventions to be administered within short time frames. Traditionally, such approaches have used black box implementations which are not explainable and hence have limited use in terms of clinical interpretability. Additionally, these implementations may either require additional training between patients, or have processing times which make them unsuitable for real-time classification. To address this, we develop a set of formal Timed Automaton-based policies that capture three common arrhythmia, Premature Ventricular Contraction, Ventricular Tachycardia, and Atrial Fibrilation, in terms of Electrocardiogram (ECG) features. We synthesise Runtime Verification monitors for each of these policies, and run them alongside existing clinical ECG databases to evaluate their efficacy. This approach shows comparable results to existing black box work with accuracies ranging from 90 % to 96 % while still being both explainable and clinically interpretable.

Unmanned aerial drones are Cyber-Physical Systems (CPSs) with increasing availability, popularity, and capability. Although other aeronautical and safety-critical industries apply stringent regulations and design approaches, smaller drones tend to have much weaker and informal design requirements. Due to the strong open-source movement in this space, there are numerous opportunities for malicious actors to find weaknesses to attack drone systems, and in parallel develop their own rogue drones. These factors present a risk of damage to people and property in addition to compromise of integrity and availability. However, a formal framework for ethical hacking that combines attacker modelling and launching of attacks is lacking in the literature. To this end, we leverage runtime enforcement, combined with the idea of suspension from synchronous programming to develop the first such formal framework. The proposed framework enables the modelling of complex attack vectors on drones. To facilitate this, we propose a bespoke policy-based runtime enforcement framework called enforcer interchange (EI). It is capable of both individual intent/target-specific attacks as well as more sophisticated combinations of attacks, which it manages by enabling and disabling attack enforcers at runtime in a context-aware manner. To demonstrate our framework, we utilise a quadcopter drone simulator and record the changes in the drone's behaviour as it executes a range of missions under different attacks. Our approach provides a framework for testing drones' resilience and defenses against malicious attacks, as well as exploring the capabilities of rogue drones.