Conference Paper/Proceeding/Abstract 148 views 28 downloads
Effective Candidate Invariant Generation Using GPGPUs and Optimisations
,
Phillip James ,
Liam O'Reilly ,
Mike Edwards
2024 Twelfth International Symposium on Computing and Networking (CANDAR), Pages: 77 - 86
Swansea University Authors:
Ben Lloyd-Roberts, Filippos Pantekis , Phillip James , Liam O'Reilly , Mike Edwards
-
PDF | Accepted Manuscript
Author accepted manuscript document released under the terms of a Creative Commons CC-BY licence using the Swansea University Research Publications Policy (rights retention).
Download (696.1KB)
DOI (Published version): 10.1109/candar64496.2024.00017
Abstract
The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states whe...
| Published in: | 2024 Twelfth International Symposium on Computing and Networking (CANDAR) |
|---|---|
| ISBN: | 979-8-3315-2837-9 979-8-3315-2836-2 |
| ISSN: | 2379-1888 2379-1896 |
| Published: |
IEEE
2024
|
| Online Access: |
Check full text
|
| URI: | https://cronfa.swan.ac.uk/Record/cronfa68671 |
| Abstract: |
The formal verification of railway control systems can ensure the safety of complex scheme plans through techniques such as induction-based model checking. While inductive verification performs well in complex settings, it often produces false positives due to its inclusion of unreachable states where safety conditions are violated by transitions from unreachable safe states to unsafe states. Invariants that reduce the state space to an over-approximation of reachable states, excluding transitions from safe to unsafe states, remove these false positives. However, such invariants are difficult to deduce automatically. This paper advances existing work on using reinforcement learning (RL) and correlation measures to generate candidate invariants. This entails mapping programs to an RL environment, incentivising agents to explore state spaces and analysing observations for invariant patterns. We observe certain complications surrounding the computation of these correlation coefficients when processing large industrial programs. This paper presents our approach using General Purpose Graphics Processing Units (GPGPUs) to overcome these challenges. We detail the steps taken to optimise our GPU kernel and present results on tested devices and inputs. We achieve runtime performance orders of magnitude higher than multi- and single-threaded CPU-side implementations, with speedups ranging from ≈21× to ≈318× when generating correlation coefficients for producing candidate invariants. |
|---|---|
| Keywords: |
Correlation coefficient, Performance evaluation, Runtime, Graphics processing units, Reinforcement learning, Model checking, Rail transportation, Safety, Space Space exploration, Optimization, formal verification, invariant finding, massively parallel, kernel optimisations |
| College: |
Faculty of Science and Engineering |
| Funders: |
Ben Lloyd-Roberts is funded by the EPSRC Centre for Doctoral Training in Enhancing Human Interactions and Collaborations with Data and Intelligence Driven Systems (EP/S021892/1) and Siemens Mobility UK. |
| Start Page: |
77 |
| End Page: |
86 |