More Web Proxy on the site http://driver.im/

Article

Abstract Interpretation with Applications to Timing Validation

Authors:

Reinhard Wilhelm,

Björn WachterAuthors Info & Claims

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

Pages 22 - 36

https://doi.org/10.1007/978-3-540-70545-1_6

Published: 07 July 2008 Publication History

Abstract

Abstract interpretation is one of the main verification technologies besides model checking and deductive verification.

Abstract interpretation has a rich theory of abstraction and strong support for the construction of abstract domains. It allows to express a precise relation to the (concrete) semantics of the programming language inducing a clear relation between the results of an abstract interpretation and the properties of the analyzed program. It permits trading efficiency against precision and offers means to enforce termination where this is not guaranteed.

We explain abstract interpretation using examples from a particular application domain: the determination of bounds on the execution times of programs. These bounds are used to show reliably that hard real-time systems satisfy their timing constraints.

The application domain requires a number of static analyses and domains with different characteristics. Most domains exhibit Galois connections, a few do not. Some analyses require widening to leap infinite ascending chains and ensure termination.

References

[1]

Kildall, G.A.: A Unified Approach to Global Program Optimization. In: Proceedings of the ACM Symposium on Principles of Programming Languages, Boston, Massachusetts, pp. 194-206 (October 1973)

Digital Library

[2]

Kam, J., Ullman, J.D.: Monotone Data Flow Analysis Frameworks. Acta Informatica 7(3), 305-318 (1977)

Digital Library

[3]

Cousot, P.: Méthodes itératives de construction et d'approximation de point fixes d'opérateurs monotone sur un treilis, analyse sémantique des programmes. PhD thesis, Université de Grenoble (1978)

[4]

Lacan, J., Monfort, J.N., Ribal, V.Q., Deutsch, A., Gonthier, G.: The software reliability verification process: The Ariane 5 example. DAta Systems In Aerospace SP-422 (1998)

[5]

Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: A static analyzer for large safety-critical software. In: Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation (PLDI 2003), San Diego, California, USA, pp. 196-207. ACM Press, New York (2003)

Digital Library

[6]

Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: Reliable and precise WCET determination for a real-life processor. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469-485. Springer, Heidelberg (2001)

Digital Library

[7]

Thesing, S., Souyris, J., Heckmann, R., Randimbivololona, F., Langenbach, M., Wilhelm, R., Ferdinand, C.: An abstract interpretation-based timing validation of hard real-time avionics software systems. In: Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), pp. 625-632. IEEE Computer Society, Los Alamitos (2003)

[8]

Mathworks: Polyspace, http://www.polyspace.com.

[9]

Coverity: Coverity Prevent, http://www.coverity.com

[10]

Fasoo.com, Seoul University: Sparrow, http://spa-arrow.com:8000/index.htm

[11]

GrammaTech Inc.: Codesurfer, http://www.grammatech.com

[12]

AbsInt Angewandte Informatik: aiT Worst-Case Execution Time Analyzers

[13]

Nielson, F., Nielson, H.R., da Rosa, D.S., Priami, C.: Static analysis for systems biology. In: Proc. of workshop on Systeomatics - dynamic biological systems informatics. Computer Science Press, Trinity College Dublin (2004)

[14]

Bodei, C., Buchholtz, M., Degano, P., Nielson, F., Nielson, H.R.: Static validation of security protocols. Journal of Computer Security 13(3), 347-390 (2005)

Digital Library

[15]

Chawdhary, A., Cook, B., Gulwani, S., Sagiv, M., Yang, H.: Ranking Abstractions. In: Proceedings of the 17th European Symposium on Programming (to appear, April 2008)

Digital Library

[16]

Alt, M., Ferdinand, C., Martin, F., Wilhelm, R.: Cache Behavior Prediction by Abstract Interpretation. In: Cousot, R., Schmidt, D.A. (eds.) SAS 1996. LNCS, vol. 1145, pp. 52-66. Springer, Heidelberg (1996)

Digital Library

[17]

Ferdinand, C., Martin, F., Wilhelm, R.: Cache Behavior Prediction by Abstract Interpretation. Science of Computer Programming 35, 163-189 (1999)

Digital Library

[18]

Heckmann, R., Langenbach, M., Thesing, S., Wilhelm, R.: The influence of processor architecture on the design and the results of WCET tools. IEEE Proceedings on Real-Time Systems 91(7), 1038-1054 (2003)

[19]

Cousot, P., Cousot, R.: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238-252 (1977)

Digital Library

[20]

Cousot, P., Cousot, R.: Comparison of the Galois connection and widening/ narrowing approaches to abstract interpretation. In: JTASPEFL 1991, Bordeaux. BIGRE, vol. 74, pp. 107-110 (1991)

[21]

Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening operators for convex polyhedra. Sci. Comput. Program. 58(1-2), 28-56 (2005)

Digital Library

[22]

Miné, A.: The octagon abstract domain. Higher Order Symbol. Comput. 19(1), 31-100 (2006)

Digital Library

[23]

Wilhelm, R., Seidl, H.: Übersetzerbau: Analyse und Transformation. Springer, Heidelberg (2008)

[24]

Ferdinand, C.: Cache Behavior Prediction for Real-Time Systems. PhD Thesis, Universität des Saarlandes (September 1997)

[25]

Thesing, S.: Safe and Precise WCET Determination by Abstract Interpretation of Pipeline Models. PhD thesis, Saarland University (2004)

[26]

Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183-235 (1994)

Digital Library

[27]

Campos, S., Grumberg, O.: Selective quantitative analysis and interval model checking: Verifying different facets of a system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 257-268. Springer, Heidelberg (1996)

Digital Library

[28]

Campos, S.V.A., Clarke, E.M.: Analysis and verification of real-time systems using quantitative symbolic algorithms. International Journal on Software Tools for Technology Transfer 2(3), 260-269 (1999)

[29]

Hartonas-Garmhausen, V., Campos, S.V.A., Cimatti, A., Clarke, E.M., Giunchiglia, F.: Verification of a safety-critical railway interlocking system with real-time constraints. Sci. Comput. Program. 36(1), 53-64 (2000)

Digital Library

[30]

Schüle, T., Schneider, K.: Exact runtime analysis using automata-based symbolic simulation. In: MEMOCODE, pp. 153-162 (2003)

Digital Library

[31]

Schüle, T., Schneider, K.: Abstraction of assembler programs for symbolic worst case execution time analysis. In: DAC, pp. 107-112 (2004)

Digital Library

[32]

Logothetis, G., Schneider, K.: Exact high level WCET analysis of synchronous programs by symbolic state space exploration. In: DATE, pp. 10196-10203 (2003)

Digital Library

[33]

Metzner, A.: Why model checking can improveWCET analysis. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 334-347. Springer, Heidelberg (2004)

[34]

Ferdinand, C., Wilhelm, R.: Fast and Efficient Cache Behavior Prediction for Real-Time Systems. Real-Time Systems 17, 131-181 (1999)

Digital Library

Cited By

Wilhelm R(2022)Principles of Abstract InterpretationFormal Aspects of Computing10.1145/354695334:2(1-3)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1145/3546953
Cousot PCousot RHenzinger TMiller D(2014)Abstract interpretationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603165(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603165
Rodrigues VFlorido Mde Sousa S(2011)A functional approach to worst-case execution time analysisProceedings of the 20th international conference on Functional and constraint logic programming10.5555/2032603.2032611(86-103)Online publication date: 19-Jul-2011
https://dl.acm.org/doi/10.5555/2032603.2032611
Show More Cited By

Abstract Interpretation with Applications to Timing Validation
1. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning

Recommendations

Complementation in abstract interpretation

Reduced product of abstract domains is a rather well-known operation for domain composition in abstract interpretation. In this article, we study its inverse operation, introducing a notion of domain complementation in abstract interpretation. ...
Static contract checking with abstract interpretation
FoVeOOS'10: Proceedings of the 2010 international conference on Formal verification of object-oriented software

We present an overview of Clousot, our current tool to statically check CodeContracts. CodeContracts enable a compiler and language-independent specification of Contracts (precondition, postconditions and object invariants).

Clousot checks every method ...
Correctness Witness Validation by Abstract Interpretation
Verification, Model Checking, and Abstract Interpretation
Abstract
Witnesses record automated program analysis results and make them exchangeable. To validate correctness witnesses through abstract interpretation, we introduce a novel abstract operation unassume. This operator incorporates witness invariants into ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CAV '08: Proceedings of the 20th international conference on Computer Aided Verification

July 2008

555 pages

ISBN:9783540705437

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 07 July 2008

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Wilhelm R(2022)Principles of Abstract InterpretationFormal Aspects of Computing10.1145/354695334:2(1-3)Online publication date: 19-Sep-2022
https://dl.acm.org/doi/10.1145/3546953
Cousot PCousot RHenzinger TMiller D(2014)Abstract interpretationProceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1145/2603088.2603165(1-10)Online publication date: 14-Jul-2014
https://dl.acm.org/doi/10.1145/2603088.2603165
Rodrigues VFlorido Mde Sousa S(2011)A functional approach to worst-case execution time analysisProceedings of the 20th international conference on Functional and constraint logic programming10.5555/2032603.2032611(86-103)Online publication date: 19-Jul-2011
https://dl.acm.org/doi/10.5555/2032603.2032611
AsĂvoae MAsĂvoae ILucanu D(2011)On abstractions for timing analysis in the K frameworkProceedings of the Second international conference on Foundational and Practical Aspects of Resource Analysis10.1007/978-3-642-32495-6_6(90-107)Online publication date: 19-May-2011
https://dl.acm.org/doi/10.1007/978-3-642-32495-6_6
Gulwani SMehra KChilimbi T(2009)SPEEDACM SIGPLAN Notices10.1145/1594834.148089844:1(127-139)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1594834.1480898
Gulwani SMehra KChilimbi TShao ZPierce B(2009)SPEEDProceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages10.1145/1480881.1480898(127-139)Online publication date: 21-Jan-2009
https://dl.acm.org/doi/10.1145/1480881.1480898

View Options

View options

Media

Figures

Other

Tables

View Table of Contents