(2020) Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries.
|
Text
Khosrowjerdi2020_Chapter_Spatio-TemporalModel-CheckingO.pdf Download (1MB) | Preview |
Abstract
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.
| Item Type: | Conference or Workshop Item (A Paper) (Paper) |
|---|---|
| Divisions: | Hamed Nemati (HM) |
| Conference: | TAP International Conference on Tests and Proofs |
| Depositing User: | Hamed Nemati |
| Date Deposited: | 01 Dec 2020 10:00 |
| Last Modified: | 01 Dec 2020 10:00 |
| Primary Research Area: | NRA1: Trustworthy Information Processing |
| URI: | https://publications.cispa.saarland/id/eprint/3212 |
Actions
Actions (login required)
 |
View Item |