TY - JOUR
T1 - The Systematic Design of Responsibility Analysis by Abstract Interpretation
AU - Deng, Chaoqiang
AU - Cousot, Patrick
N1 - Publisher Copyright:
© 2021 Copyright held by the owner/author(s). Publication rights licensed to ACM.
PY - 2022/3
Y1 - 2022/3
N2 - Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples.However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.
AB - Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples.However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.
KW - Responsibility analysis
KW - abstract interpretation
KW - backward accessibility analysis
KW - causality
KW - cognizance
KW - dependency
KW - forward reachability analysis
KW - trace partitioning
UR - http://www.scopus.com/inward/record.url?scp=85123416988&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85123416988&partnerID=8YFLogxK
U2 - 10.1145/3484938
DO - 10.1145/3484938
M3 - Article
AN - SCOPUS:85123416988
SN - 0164-0925
VL - 44
JO - ACM Transactions on Programming Languages and Systems
JF - ACM Transactions on Programming Languages and Systems
IS - 1
M1 - 3484938
ER -