Document Type
Article
Publication Date
2023
Publication Source
2023 21st ACM-IEEE International Symposium on Formal Methods and Models for System Design, Memocode
Abstract
Hyperproperties extend trace properties to express properties of sets of traces, and they are increasingly popular in specifying various security and performance-related properties in domains such as cyber-physical systems, smart grids, and automotive. This paper introduces HyperTWTL, which extends Time Window Temporal Logic (TWTL)-a domain-specific formal specification language for robotics, by allowing explicit and simultaneous quantification over multiple execution traces. We propose two different semantics for HyperTWTL, synchronous and asynchronous, based on the alignment of the timestamps in the traces. Consequently, we demonstrate the application of HyperTWTL in formalizing important information-flow security policies and concurrency for robotics applications. Furthermore, we introduce a model checking algorithm for verifying fragments of HyperTWTL by reducing the problem to a TWTL model checking problem.
Inclusive pages
100-110
ISBN/ISSN
1936-9492
Document Version
Published Version
Publisher
ASSOC Computing Machinery
Peer Reviewed
yes
eCommons Citation
Bonnah, Ernest; Nguyen, Luan Viet; and Hoque, Khaza Anuarul, "Model Checking Time Window Temporal Logic for Hyperproperties" (2023). Computer Science Faculty Publications. 187.
https://ecommons.udayton.edu/cps_fac_pub/187
Comments
This open-access article is provided for download in compliance with the publisher’s policy on self-archiving. To view the version of record, use the DOI: https://doi.org/10.1145/3610579.3611077