kth.sePublications KTH
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Spatio-Temporal Model-Checking of Cyber-Physical Systems Using Graph Queries
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0001-9615-5389
Helmholtz Center for Information Security (CISPA), Saarbrücken, Germany.ORCID iD: 0000-0001-9251-3679
KTH, School of Electrical Engineering and Computer Science (EECS), Computer Science, Theoretical Computer Science, TCS.ORCID iD: 0000-0002-9706-5008
2020 (English)In: Tests and Proofs / [ed] Wolfgang Ahrendt and Heike Wehrheim, New York: Springer Nature, 2020, Vol. 12165, p. 59-79Conference paper, Published paper (Refereed)
Abstract [en]

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 se-mantically equivalent property graphs and graph queries respectively. We prove a sound reduction of the spatio-temporal verification problem tograph database query solving. The practicability and efficiency of thisapproach 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.

Place, publisher, year, edition, pages
New York: Springer Nature, 2020. Vol. 12165, p. 59-79
Series
Lecture Notes in Computer Science, ISSN 0302-9743, E-ISSN 1611-3349 ; 12165
National Category
Computer Sciences
Research subject
Computer Science
Identifiers
URN: urn:nbn:se:kth:diva-282827DOI: 10.1007/978-3-030-50995-8_4ISI: 000908023800004Scopus ID: 2-s2.0-85087280755OAI: oai:DiVA.org:kth-282827DiVA, id: diva2:1472072
Conference
Tests and Proofs - 14th International Conference, TAP@STAF 2020, Bergen, Norway, June 22-23, 2020
Note

QC 20201007

Available from: 2020-09-30 Created: 2020-09-30 Last updated: 2023-09-21Bibliographically approved

Open Access in DiVA

No full text in DiVA

Other links

Publisher's full textScopus

Authority records

Khosrowjerdi, HojatNemati, HamedMeinke, Karl

Search in DiVA

By author/editor
Khosrowjerdi, HojatNemati, HamedMeinke, Karl
By organisation
Theoretical Computer Science, TCS
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

doi
urn-nbn

Altmetric score

doi
urn-nbn
Total: 128 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf