E-mail senden E-Mail Adresse kopieren

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


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.

Konferenz / Medium

Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020, Proceedings postponed



Letztes Änderungsdatum

2020-12-01 10:00:31