KIT | KIT-Bibliothek | Impressum | Datenschutz

On Temporal Path Conditions in Dependence Graphs

Lochbihler, Andreas 1; Snelting, Gregor 1
1 Karlsruher Institut für Technologie (KIT)

Abstract:

Program dependence graphs are a well-established device to represent possible information flow in a program. Path conditions in dependence graphs have been proposed to express more detailed circumstances of a particular flow; they provide precise necessary conditions for information flow along a path or chop in a dependence graph. Ordinary boolean path conditions, however, cannot express temporal properties, e.g. that for a specific flow it is necessary that some condition holds, and later another specific condition holds.
In this contribution, we introduce temporal path conditions, which extend ordinary path conditions by temporal operators in order to express temporal dependencies between conditions for a flow. We present motivating examples, generation and simplification rules, application of model checking to generate witnesses for a specific flow, and a case study. We prove the following soundness property: if a temporal path condition for a path is satisfiable, then the ordinary boolean
path condition for the path is satisfiable. The converse does not hold, indicating that temporal path conditions are more precise.


Scopus
Zitationen: 3
Web of Science
Zitationen: 2
Zugehörige Institution(en) am KIT Institut für Programmstrukturen und Datenorganisation (IPD)
Kompetenzzentrum für angewandte Sicherheitstechnologie (KASTEL)
Publikationstyp Zeitschriftenaufsatz
Publikationsjahr 2009
Sprache Englisch
Identifikator ISSN: 0928-8910
KITopen-ID: 1000017642
Erschienen in Automated Software Engineering
Verlag Springer
Band 16
Heft 2
Seiten 263 - 290
Projektinformation KASTEL I (BMBF, 01BY1172 / 16BY1172)
Nachgewiesen in Scopus
Web of Science
KIT – Die Forschungsuniversität in der Helmholtz-Gemeinschaft
KITopen Landing Page