chapter

Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software

Authors:

Xavier RivalAuthors Info & Claims

The essence of computation: complexity, analysis, transformation

January 2002

Pages 85 - 108

Published: 01 January 2002 Publication History

Abstract

We report on a successful preliminary experience in the design and implementation of a special-purpose Abstract Interpretation based static program analyzer for the verification of safety critical embedded real-time software. The analyzer is both precise (zero false alarm in the considered experiment) and efficient (less than one minute of analysis for 10,000 lines of code). Even if it is based on a simple interval analysis, many features have been added to obtain the desired precision: expansion of small arrays, widening with several thresholds, loop unrolling, trace partitioning, relations between loop counters and other variables. The efficiency of the tool mainly comes from a clever representation of abstract environments based on balanced binary search trees.

References

[1]

1. J.-R. Abrial. On B. In D. Bert, editor, Proc. 2nd Int. B Conf., B'98: Recent Advances in the Development and Use of the B Method, Montpellier, FR, LNCS 1393, pages 1-8. Springer-Verlag, 22-24 Apr. 1998.]]

Digital Library

Google Scholar

[2]

2. American National Standards Institute, Inc. IEEE standard for binary floating-point arithmetic. Technical Report 754-1985, ANSI/IEEE, 1985. http://grouper. ieee.org/groups/754/.]]

Google Scholar

[3]

3. P. R. Bevington and D. K. Robinson. Data Reduction and Error Analysis for the Physical Sciences. McGraw-Hill, 1992.]]

Google Scholar

[4]

4. P. Cousot. The Marktoberdorf'98 generic abstract interpreter, http://www.di. ens.fr/~cousot/Marktoberdorf98.shtml, Nov. 1998.]]

Google Scholar

[5]

5. P. Cousot. Abstract interpretation based formal methods and future challenges, invited paper. In R. Wilhelm, editor, «Informatics -- 10 Years Back, 10 Years-- Ahead», volume 2000 of LNCS, pages 138-156. Springer-Verlag, 2000.]]

Digital Library

Google Scholar

[6]

6. P. Cousot. Partial completeness of abstract fixpoint checking, invited paper. In B.Y. Choueiry and T: Walsh, editors, Proc. 4 th Int. Symp. SARA '2000, Horseshoe Bay, TX, US, LNAI 1864, pages 1-25. Springer-Verlag, 26-29 Jul. 2000.]]

Digital Library

Google Scholar

[7]

7. P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proc. 2 nd Int. Symp. on Programming, pages 106-130. Dunod, 1976.]]

Google Scholar

[8]

8. P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, In 4th POPL, pages 238-252, Los Angeles, CA, 1977. ACM Press.]]

Digital Library

Google Scholar

[9]

9. P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In 6 th POPL, pages 269-282, San Antonio, TX, 1979. ACM Press.]]

Digital Library

Google Scholar

[10]

10. D. Goldberg. What every computer scientist should know about floating-point arithmetic. ACM Comput. Surv., 23(1):5-48, Mar. 1991.]]

Digital Library

Google Scholar

[11]

11. M. Handjieva and S. Tzolovski. Refining static analyses by trace-based partitioning using control flow. In G. Levi, editor, Proc. 5 th Int. Symp. SAS '98, Pisa, IT, 14-16 Sep. 1998, LNCS 1503, pages 200-214. Springer-Verlag, 1998.]]

Google Scholar

[12]

12. G.J. Holzmann. Software analysis and model checking. In E. Brinksma and K.G. Larsen, editors, Proc. 14 th Int. Conf. CAV'2002, Copenhagen, DK, LNCS 2404, pages 1-16. Springer-Verlag, 27-31 Jul. 2002.]]

Digital Library

Google Scholar

[13]

13. N. Jones, C.K. Gomard, and P. Sestoft. Partial Evaluation and Automatic Program Generation. Int. Series in Computer Science. Prentice-Hall, June 1993.]]

Digital Library

Google Scholar

[14]

14. JTC 1/SC 22. Programming languages -- C. Technical report, ISO/IEC 9899:1999, 16 Dec. 1999.]]

Google Scholar

[15]

15. X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The Objective Caml system, documentation and user's manual (release 3.04). Technical report, INRIA, Rocquencourt, FR., 10 Dec. 2001. http://caml.inria.fr/ocaml/.]]

Google Scholar

[16]

16. A. Miné. A new numerical abstract domain based on difference-bound matrices. In O. Danvy and A. Filinski, editors, Proc. 2 nd Symp. PADO '2001, Århus, DK, 21-23 May 2001, LNCS 2053, pages 155-172. Springer-Verlag, 2001. http://www di. ens. fr/~mine/publi/article-mine-padoII.pdf.]]

Digital Library

Google Scholar

[17]

17. S. Owre, N. Shankar, and D.W.J. Stringer-Calvert. PVS: An experience report. In D. Hutter, W. Stephan, P. Traverso, and M. Ullmann, editors, PROC Applied Formal Methods - FM-Trends'98, International Workshop on Current Trends in Applied Formal Method, Boppard, DE, LNCS 1641, pages 338-345. Springer-Verlag, 7-9 Oct. 1999.]]

Digital Library

Google Scholar

Cited By

View all

Pailoor SWang XShacham HDillig I(2020)Automated policy synthesis for system call sandboxingProceedings of the ACM on Programming Languages10.1145/34282034:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428203
Hähnle RWasser NBubel R(2016)Array Abstraction with Symbolic PivotsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_9(104-121)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-319-30734-3_9
Chatty SMagnaudet MPrun DZiegler JNebeling MNigay L(2015)Verification of properties of interactive components from their executable codeProceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems10.1145/2774225.2774848(276-285)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2774225.2774848
Show More Cited By

Index Terms

Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software

Recommendations

A static analyzer for large safety-critical software
PLDI '03: Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation

We show that abstract interpretation-based static program analysis can be made efficient and precise enough to formally verify a class of properties for a family of large programs with few or no false alarms. This is achieved by refinement of a general ...
An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer
VMCAI 2015: Proceedings of the 16th International Conference on Verification, Model Checking, and Abstract Interpretation - Volume 8931

Many practical static analyzers are not completely sound by design. Their designers trade soundness to increase automation, improve performance, and reduce the number of false positives or the annotation overhead. However, the impact of such design ...
Static program analysis of embedded executable assembly code
CASES '04: Proceedings of the 2004 international conference on Compilers, architecture, and synthesis for embedded systems

We consider the problem of automatically checking if coding standards have been followed in the development of embedded applications. The problem arises from practical considerations because DSP chip manufacturers (in our case Texas Instruments) want ...

Reviews

Reviewer: Michael Zastre

This is a welcome addition to the literature on abstract interpretation, as it describes a non-trivial analysis in a subset of the C programming language. For many years most papers have applied such interpretation on functional language programs, and papers describing application to programs written in imperative style languages were few and far between. This book chapter does assume some familiarity with the technique, but a reader need not be an expert. The adjective "special-purpose" in the title is the focus of the chapter, in that it reduces the runtime of an analysis through reducing the analyzer's complexity. Instead of creating a general-purpose analyzer for the ANSI C language, particular concrete semantics for some C implementation are used, in this case that for a real-time system consisting of some 10,000 lines of code. Some of the restrictions may seem a bit unrealistic (such as no recursive functions), but others are very reasonable (as in the case of no gotos). Sections 6 and 7 are the most valuable. The former describes a set of useful mappings into abstract environments, and the latter is a list of dead ends, describing approaches resulting in expensive analyzers. The chapter is well written, and a motivated reader will be well rewarded for reading it. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

The essence of computation: complexity, analysis, transformation

January 2002

500 pages

ISBN:3540003266

Editors:
Torben Æ Mogensen
University of Copenhagen, DIKU, Universitetsparken 1, 2100 Copenhagen, Denmark
,
David A. Schmidt
Kansas State University, Department of Computing and Information Sciences, 234 Nichols Hall, Manhattan, KS
,
I. Hal Sudborough
University of Texas at Dallas, Department of Computer Science, P.O. Box 830688, Richardson, TX

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 01 January 2002

Qualifiers

Chapter

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

57
Total Citations
View Citations
0
Total Downloads

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

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Pailoor SWang XShacham HDillig I(2020)Automated policy synthesis for system call sandboxingProceedings of the ACM on Programming Languages10.1145/34282034:OOPSLA(1-26)Online publication date: 13-Nov-2020
https://dl.acm.org/doi/10.1145/3428203
Hähnle RWasser NBubel R(2016)Array Abstraction with Symbolic PivotsEssays Dedicated to Frank de Boer on Theory and Practice of Formal Methods - Volume 966010.1007/978-3-319-30734-3_9(104-121)Online publication date: 1-Jan-2016
https://dl.acm.org/doi/10.1007/978-3-319-30734-3_9
Chatty SMagnaudet MPrun DZiegler JNebeling MNigay L(2015)Verification of properties of interactive components from their executable codeProceedings of the 7th ACM SIGCHI Symposium on Engineering Interactive Computing Systems10.1145/2774225.2774848(276-285)Online publication date: 23-Jun-2015
https://dl.acm.org/doi/10.1145/2774225.2774848
Frechtling MLeong P(2015)MCALIBACM Transactions on Programming Languages and Systems10.1145/266507337:2(1-25)Online publication date: 16-Apr-2015
https://dl.acm.org/doi/10.1145/2665073
Gange GNavas JSchachte PSøndergaard HStuckey P(2015)Interval Analysis and Machine ArithmeticACM Transactions on Programming Languages and Systems10.1145/265136037:1(1-35)Online publication date: 20-Jan-2015
https://dl.acm.org/doi/10.1145/2651360
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
Cox ASankaranarayanan SChang B(2014)A bit too precise? Verification of quantized digital filtersInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-013-0279-916:2(175-190)Online publication date: 1-Apr-2014
https://dl.acm.org/doi/10.1007/s10009-013-0279-9
Kapur DZhang ZHorbach MZhao HLu QNguyen T(2013)Geometric quantifier elimination heuristics for automatically generating octagonal and max-plus invariantsAutomated Reasoning and Mathematics10.5555/2554473.2554484(189-228)Online publication date: 1-Jan-2013
https://dl.acm.org/doi/10.5555/2554473.2554484
Hatcliff JLeavens GLeino KMüller PParkinson M(2012)Behavioral interface specification languagesACM Computing Surveys10.1145/2187671.218767844:3(1-58)Online publication date: 14-Jun-2012
https://dl.acm.org/doi/10.1145/2187671.2187678
Choudhury ABhattacharjee AAggarwal SPrabhakar TVarma VPadmanabhuni S(2012)REDProceedings of the 5th India Software Engineering Conference10.1145/2134254.2134260(37-40)Online publication date: 22-Feb-2012
https://dl.acm.org/doi/10.1145/2134254.2134260
Show More Cited By

Abstract

References

Cited By

Index Terms

Recommendations

A static analyzer for large safety-critical software

An Experimental Evaluation of Deliberate Unsoundness in a Static Program Analyzer

Static program analysis of embedded executable assembly code

Reviews

Access critical reviews of Computing literature here

Comments

Information

Published In

Publisher

Publication History

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations