Anzeige
Erschienen in:
2012 | OriginalPaper | Buchkapitel
Model Checking Information Flow in Reactive Systems
verfasst von : Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, Helmut Seidl
Erschienen in: Verification, Model Checking, and Abstract Interpretation
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Most analysis methods for information flow properties do not consider temporal restrictions. In practice, however, such properties rarely occur statically, but have to consider constraints such as
when and under which conditions
a variable has to be kept secret. In this paper, we propose a natural integration of information flow properties into linear-time temporal logics (LTL). We add a new modal operator, the hide operator, expressing that the observable behavior of a system is independent of the valuations of a secret variable. We provide a complexity analysis for the model checking problem of the resulting logic SecLTL and we identify an expressive fragment for which this question is efficiently decidable. We also show that the path based nature of the hide operator allows for seamless integration into branching time logics.