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.

Sharkey, Kiss and others developed a dynamical approach to modelling epidemic disease on a contact graph by generating systems of first-order ordinary differential equations expressing the model dynamics [1], [2], which are solved to yield exact and deterministic modelling results. However, they left algorithmic generation (and solving) of systems and runtime assessment of the approach as an open question. To address this, we give an open source implementation that takes both a compartmental model and a contact graph as input and then generates and solves a system of equations exactly describing the dynamics of the system. Our implementation uses a moment closure result on single-vertex cutsets in the contact graph to reduce the number of equations required. In runtime experiments, we find that the implementation of the dynamical approach is almost always slower than a comparable Monte Carlo simulation in finding the expected state of the modelling system at a specified time. To complement our runtime evaluations, we give results and bounds on the number of equations required to describe a system as a function of the size of the compartmental model and input graph. We show that a natural extension of the moment closure result on single-vertex cutsets to larger cutsets is only possible for restricted projections of the model states on the cutset. We conclude that the dynamical approach is unlikely to be suitable unless exact, deterministic (rather than simulated) results are essential.

Multiple choice questions are a popular means of assessment for online examinations: easy to mark, but difficult to prepare in a way that makes it hard for students to gain high marks by sharing answers between them. Here we describe a systematic approach for creating multiple choice questions that can be used to test the understanding of bookwork topics, while still being challenging and mitigating against potential cheating.

Probabilistic model checking can overcome much of the complexity inherent in balancing games. Game balancing is the careful maintenance of relationships between the ways in which a game can be played, to ensure that no single way is strictly better than all others, and that players are offered a wide variety of ways to play successfully. We introduce a novel approach toward automating game balancing using probabilistic model checking called chained strategy generation (CSG). This involves generating chains of adversarial strategies, which mimic the way players adapt their approach during repeated plays of a game. We use CSG to map out the evolving metagame. The trends identified can allow game developers to identify strategies, which will be too strong, and ways of playing the game, which a player may want to use, but are never viable for successful competitive play. We introduce a case study, a game called RPGLite, and use CSG to compare five candidate configurations for the game. We show how to determine which configurations of RPGLite lead to a more fair and interesting experience for players. We also identify unexpected trends in how the strategies evolve. Our approach introduces a new technique for improving game development and player experience.

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.

Abstract Formal verification of agents representing robot behaviour is a growing area due to the demand that autonomous systems have to be proven safe. In this paper we present an abstract definition of autonomy which can be used to model autonomous scenarios and propose the use of small-scale simulation models representing abstract actions to infer quantitative data. To demonstrate the applicability of the approach we build and verify a model of an unmanned aerial vehicle (UAV) in an exemplary autonomous scenario, utilising this approach.

Abstract As autonomous systems become more prevalent, methods for their verification will become more widely used. Model checking is a formal verification technique that can help ensure the safety of autonomous systems, but in most cases it cannot be applied by novices, or in its straight “off-the-shelf” form. In order to be more widely applicable it is crucial that more sophisticated techniques are used, and are presented in a way that is reproducible by engineers and verifiers alike. In this paper we demonstrate in detail two techniques that are used to increase the power of model checking using the model checker S pin . The first of these is the use of embedded C code within Promela specifications, in order to accurately reflect robot movement. The second is to use abstraction together with a simulation relation to allow us to verify multiple environments simultaneously. We apply these techniques to a fairly simple system in which a robot moves about a fixed circular environment and learns to avoid obstacles. The learning algorithm is inspired by the way that insects learn to avoid obstacles in response to pain signals received from their antennae. Crucially, we prove that our abstraction is sound for our example system—a step that is often omitted but is vital if formal verification is to be widely accepted as a useful and meaningful approach.

We present formal specification and verification of a robot moving in a complex network, using temporal sequence learning to avoid obstacles. Our aim is to demonstrate the benefit of using a formal approach to analyze such a system as a complementary approach to simulation. We first describe a classical closed-loop simulation of the system and compare this approach to one in which the system is analyzed using formal verification. We show that the formal verification has some advantages over classical simulation and finds deficiencies our classical simulation did not identify. Specifically we present a formal specification of the system, defined in the Promela modeling language and show how the associated model is verified using the Spin model checker. We then introduce an abstract model that is suitable for verifying the same properties for any environment with obstacles under a given set of assumptions. We outline how we can prove that our abstraction is sound: any property that holds for the abstracted model will hold in the original (unabstracted) model.

We describe verification of S-MAC, a medium access control protocol designed for wireless sensor networks, by means of the PRISM model checker. The S-MAC protocol is built on top of the IEEE 802.11 standard for wireless ad hoc networks and, as such, it uses the same randomised backoff procedure as a means to avoid collision. In order to minimise energy consumption, in S-MAC, nodes are periodically put into a sleep state. Synchronisation of the sleeping schedules is necessary for the nodes to be able to communicate. Intuitively, energy saving obtained through a periodic sleep mechanism will be at the expense of performance. In previous work on S-MAC verification, a combination of analytical techniques and simulation has been used to confirm the correctness of this intuition for a simplified (abstract) version of the protocol in which the initial schedules coordination phase is assumed correct. We show how we have used the PRISM model checker to verify the behaviour of S-MAC and compare it to that of IEEE 802.11.

Abstract. We describe how the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol is modelled in Promela and verified using SPIN. The verification of arbitrary system configurations is discussed.

The automatic verification of concurrent systems by model-checking is limited due to the inability to generalise results to systems consisting of any number of processes. We use abstraction to prove general results, by model-checking, about feature interaction analysis of a telecommunications service involving any number of processes. The key idea is to model-check a system of constant number (m) of concurrent processes, in parallel with an "abstract" process which represents the product of any number of other processes. The system, for any specified set of selected features, is generated automatically using Perl scripts.