Model Checking Time Window Temporal Logic for Hyperproperties

要約

ハイパープロパティは、トレースのセットのプロパティを表現するためにトレース プロパティを拡張し、サイバーフィジカル システム、スマート グリッド、自動車などのドメインでさまざまなセキュリティおよびパフォーマンス関連のプロパティを指定する際にますます一般的になっています。
この論文では、新しい形式主義のモデル チェック アルゴリズムである HyperTWTL を紹介します。これは、複数の実行トレースにわたる明示的かつ同時の定量化を可能にすることで、ロボット工学向けのドメイン固有の形式的仕様言語であるタイム ウィンドウ テンポラル ロジック (TWTL) を拡張します。
トレース内のタイムスタンプの位置合わせに基づいて、\emph{synchronous} セマンティクスと \emph{asynchronous} セマンティクスの両方を備えた HyperTWTL を示します。
その結果、ロボット工学アプリケーションの重要な情報フロー セキュリティ ポリシーと同時実行性を形式化する際の HyperTWTL のアプリケーションを実証します。
最後に、問題を TWTL モデル チェック問題に還元することにより、HyperTWTL のフラグメントを検証するためのモデル チェック アルゴリズムを提案します。

要約(オリジナル)

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 a model checking algorithm for a new formalism, 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 present HyperTWTL with both \emph{synchronous} and \emph{asynchronous} semantics, 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. Finally, we propose a model checking algorithm for verifying fragments of HyperTWTL by reducing the problem to a TWTL model checking problem.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google