Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries

Khosrowjerdi, Hojat and Nemati, Hamed and Meinke, Karl
(2020) Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries.
In: Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings postponed.
Conference: TAP International Conference on Tests and Proofs


Download (1MB) | Preview
Official URL:\_4


We explore the application of graph database technology to spatio-temporal model checking of cooperating cyber-physical systems-of-systems such as vehicle platoons. We present a translation of spatio-temporal automata (STA) and the spatio-temporal logic STAL to semantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem to graph database query solving. The practicability and efficiency of this approach is evaluated by introducing NeoMC, a prototype implementation of our explicit model checking approach based on Neo4j. To evaluate NeoMC we consider case studies of verifying vehicle platooning models. Our evaluation demonstrates the effectiveness of our approach in terms of execution time and counterexample detection.


Actions (login required)

View Item View Item