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

research-article

Combining unit-level symbolic execution and system-level concrete execution for testing nasa software

Authors:

Corina S. Pǎsǎreanu,

Peter C. Mehlitz,

David H. Bushnell,

Karen Gundy-Burlet,

Suzette Person,

Mark PapeAuthors Info & Claims

ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis

Pages 15 - 26

https://doi.org/10.1145/1390630.1390635

Published: 20 July 2008 Publication History

Abstract

We describe an approach to testing complex safety critical software that combines unit-level symbolic execution and system-level concrete execution for generating test cases that satisfy user-specified testing criteria. We have developed Symbolic Java PathFinder, a symbolic execution framework that implements a non-standard bytecode interpreter on top of the Java PathFinder model checking tool. The framework propagates the symbolic information via attributes associated with the program data. Furthermore, we use two techniques that leverage system-level concrete program executions to gather information about a unit's input to improve the precision of the unit-level test case generation. We applied our approach to testing a prototype NASA flight software component. Our analysis helped discover a serious bug that resulted in design changes to the software. Although we give our presentation in the context of a NASA project, we believe that our work is relevant for other critical systems that require thorough testing.

References

[1]

A. Acevedo, J. Arnold, and W. Othon. ANTARES: Spacecraft simulation for multiple user communities and facilities. In AIAA Modeling and Simulation Technologies Conference and Exhibit, 2007.

[2]

P. Ammann, P. E. Black, and W. Majurski. Using model checking to generate tests from specifications. In Proc. of the 2nd IEEE International Conference on Formal Engineering Methods, 1998.

Digital Library

[3]

M. d'Amorim, C. Pacheco, T. Xie, D. Marinov, and M. D. Ernst. An Empirical Comparison of Automated Generation and Classification. In Proc. of the 21st ASE, 2006.

Digital Library

[4]

S. Anand, A. Orso, and M. J. Harrold. Type-dependence analysis and program transformation for symbolic execution. In Proc. of the 13th International TACAS Conference, 2007.

Digital Library

[5]

S. Anand, C. S. Pǎsǎreanu, and W. Visser. JPF-SE: A symbolic execution extension to Java PathFinder. In Proc. of the 13th International TACAS Conference, 2007.

Digital Library

[6]

T. Ball. A theory of predicate-complete test coverage and generation, 2004. Microsoft Research Technical Report MSR-TR-2004-28.

[7]

T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. 29th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 1--3, 2002.

Digital Library

[8]

D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. Generating tests from counterexamples. In Proc. of the 26th International Conference on Software Engineering (ICSE), 2004.

Digital Library

[9]

C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: automatically generating inputs of death. In Proc. ACM Conference on Computer and Communications Security, 2006.

Digital Library

[10]

The Choco Constraint Solver. http://choco.sourceforge.net/

[11]

L. A. Clarke. A system to generate test data and symbolically execute programs. IEEE Trans. Software Eng, 2(3):215--222, 1976.

Digital Library

[12]

The Daikon invariant detector. http://groups.csail.mit.edu/pag/daikon//

[13]

D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Compaq Systems Research Center, 1998.

[14]

S. G. Elbaum, H. N. Chin, M. B. Dwyer, and J. Dokulil. Carving differential unit test cases from system test cases. In Proc. of SIGSOFT FSE, 2006.

Digital Library

[15]

E. Gamma, R. Helm, R. Johnson, and J. M. Vlissides. Design Patterns: Elements of Reusable Object--Oriented Software. Addison--Wesley, 1994.

Digital Library

[16]

A. Gargantini and C. Heitmeyer. Using model checking to generate tests from requirements specifications. In Proc. of the 7th European Software Engineering Conference, Held Jointly with the 7th ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE), 1999.

Digital Library

[17]

P. Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th Annual ACM Symposium on the Principles of Programming Languages (POPL), pages 174--186, Paris, France, Jan. 1997.

Digital Library

[18]

P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In Proc. PLDI, 2005.

Digital Library

[19]

B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori, and S. K. Rajamani. SYNERGY: a new algorithm for property checking. In Proc. of SIGSOFT FSE, 2006.

Digital Library

[20]

M. P. E. Heimdahl, S. Rayadurgam, W. Visser, D. George, and J. Gao. Auto-generating test sequences using model checkers: A case study. In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES), Montreal, Canada, Oct. 2003.

[21]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with blast. In Proceedings of the Tenth International Workshop on Model Checking of Software, volume 2648 of Lecture Notes in Computer Science, 2003.

Digital Library

[22]

G. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison--Wesley, 2003.

Digital Library

[23]

H. S. Hong, I. Lee, O. Sokolsky, and H. Ural. A temporal logic based theory of test coverage and generation. In Proc. 8th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), Grenoble, France, April 2002.

Digital Library

[24]

IASolver. http://www.cs.brandeis.edu/~tim/Applets/IAsolver.html

[25]

Java PathFinder. http://javapathfinder.sourceforge.net

[26]

S. Khurshid, C. S. Pǎsǎreanu, and W. Visser. Generalized symbolic execution for model checking and testing. In Proc. of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2003.

Digital Library

[27]

J. C. King. Symbolic execution and program testing. Communications of the ACM, 19(7):385--394, 1976.

Digital Library

[28]

T. Lev-Ami and M. Sagiv. TVLA: A system for implementing static analyses. In Proc. Static Analysis Symposium, Santa Barbara, CA, June 2000.

Digital Library

[29]

T. Lindholm and F. Yellin. Java(™) Virtual Machine Specification. Prentice Hall, 1999.

Digital Library

[30]

T. Menzies and Y. Hu. Data mining for very busy people. Computer, 36(11):22--29, 2003.

Digital Library

[31]

K. Sen, D. Marinov, and G. Agha. CUTE: a concolic unit testing engine for C. In Proc. ESEC/SIGSOFT FSE, 2005.

Digital Library

[32]

W. Visser, C. S. Pǎsǎreanu, and R. Pelanek. Test input generation for java containers using state matching. In Proc. ISSTA, 2006.

Digital Library

[33]

T. Xie, D. Marinov, W. Schulte, and D. Notkin. Symstra: A framework for generating object-oriented unit tests using symbolic execution. In Proc. of the 11th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), 2005.

Digital Library

[34]

G. Yorsh, T. Ball, and M. Sagiv. Testing, abstraction, theorem proving: better together! In Proc. ISSTA, 2006.

Digital Library

Cited By

Shuai ZChen ZMa KLiu KZhang YSun JWang J(2024)Partial Solution Based Constraint Solving Cache in Symbolic ExecutionProceedings of the ACM on Software Engineering10.1145/36608171:FSE(2493-2514)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660817
Coppa EIzzillo A(2024)Testing concolic execution through consistency checksJournal of Systems and Software10.1016/j.jss.2024.112001211:COnline publication date: 2-Jul-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.112001
Brain MPolgreen E(2024)A Pyramid Of (Formal) Software VerificationFormal Methods10.1007/978-3-031-71177-0_24(393-419)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_24
Show More Cited By

Index Terms

Combining unit-level symbolic execution and system-level concrete execution for testing nasa software

Recommendations

Symbolic execution and program testing

This paper describes the symbolic execution of programs. Instead of supplying the normal inputs to a program (e.g. numbers) one supplies symbols representing arbitrary values. The execution proceeds as in a normal execution except that values may be ...
Symbolic execution techniques for refinement testing
TAP'07: Proceedings of the 1st international conference on Tests and proofs

We propose an approach to test whether an abstract specification is refined or not by a more concrete one. The specifications are input/output symbolic transition systems (IOSTS). The refinement relation requires that all traces of the abstract system ...
Combined Symbolic and Concrete Execution of TTCN-3 for Automated Testing
ISISE '08: Proceedings of the 2008 International Symposium on Information Science and Engieering - Volume 01

Testing procedure can be described by the Testing and Test Control Notation-version 3(TTCN-3). The automatic execution of TTCN-3 test scripts is transformed to automatic testing of system under test (SUT). We propose a framework, which uses combined ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis

July 2008

324 pages

ISBN:9781605580500

DOI:10.1145/1390630

General Chair:
Barbara G. Ryder
Virginia Tech, USA
,
Program Chair:
Andreas Zeller
Saarland University, Germany

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 20 July 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ISSTA '08

Sponsor:

ISSTA '08: International Symposium on Software Testing and Analysis

July 20 - 24, 2008

WA, Seattle, USA

Acceptance Rates

Overall Acceptance Rate 58 of 213 submissions, 27%

Upcoming Conference

ISSTA '25

Sponsor:
sigsoft

34th ACM SIGSOFT International Symposium on Software Testing and Analysis

June 25 - 28, 2025

Trondheim , Norway

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

191
Total Citations
View Citations
1,322
Total Downloads

Downloads (Last 12 months)50
Downloads (Last 6 weeks)9

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Shuai ZChen ZMa KLiu KZhang YSun JWang J(2024)Partial Solution Based Constraint Solving Cache in Symbolic ExecutionProceedings of the ACM on Software Engineering10.1145/36608171:FSE(2493-2514)Online publication date: 12-Jul-2024
https://dl.acm.org/doi/10.1145/3660817
Coppa EIzzillo A(2024)Testing concolic execution through consistency checksJournal of Systems and Software10.1016/j.jss.2024.112001211:COnline publication date: 2-Jul-2024
https://dl.acm.org/doi/10.1016/j.jss.2024.112001
Brain MPolgreen E(2024)A Pyramid Of (Formal) Software VerificationFormal Methods10.1007/978-3-031-71177-0_24(393-419)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_24
Bousy IBarr EClark D(2023)PopArt: Ranked Testing EfficiencyIEEE Transactions on Software Engineering10.1109/TSE.2022.321479649:4(2221-2238)Online publication date: 1-Apr-2023
https://doi.org/10.1109/TSE.2022.3214796
Muylaert WHärtel JDe Roover C(2023)Symbolic Execution to Detect Semantic Merge Conflicts2023 IEEE 23rd International Working Conference on Source Code Analysis and Manipulation (SCAM)10.1109/SCAM59687.2023.00028(186-197)Online publication date: 2-Oct-2023
https://doi.org/10.1109/SCAM59687.2023.00028
Su RZhang ZZhou YYao Y(2023)Test Generation for Mutation Testing by Symbolic Execution2023 IEEE 23rd International Conference on Software Quality, Reliability, and Security Companion (QRS-C)10.1109/QRS-C60940.2023.00098(55-61)Online publication date: 22-Oct-2023
https://doi.org/10.1109/QRS-C60940.2023.00098
Baradaran SHeidari MKamali AMouzarani M(2023)A unit-based symbolic execution method for detecting memory corruption vulnerabilities in executable codesInternational Journal of Information Security10.1007/s10207-023-00691-122:5(1277-1290)Online publication date: 7-May-2023
https://doi.org/10.1007/s10207-023-00691-1
Abbasi RSchiffl JDarulova EUlbrich MAhrendt W(2023)Combining rule- and SMT-based reasoning for verifying floating-point Java programs in KeYInternational Journal on Software Tools for Technology Transfer10.1007/s10009-022-00691-x25:2(185-204)Online publication date: 8-Mar-2023
https://doi.org/10.1007/s10009-022-00691-x
Ghosal SJonsson BRümmer P(2023)An Active Learning Approach to Synthesizing Program ContractsSoftware Engineering and Formal Methods10.1007/978-3-031-47115-5_8(126-144)Online publication date: 31-Oct-2023
https://doi.org/10.1007/978-3-031-47115-5_8
Tiraboschi IRezk TRival X(2023)Sound Symbolic Execution via Abstract Interpretation and Its Application to SecurityVerification, Model Checking, and Abstract Interpretation10.1007/978-3-031-24950-1_13(267-295)Online publication date: 17-Jan-2023
https://doi.org/10.1007/978-3-031-24950-1_13
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents