research-article

From scripts to specifications: the evolution of a flight software testing effort

Authors:

Alex Groce,

Klaus Havelund,

Margaret SmithAuthors Info & Claims

ICSE '10: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2

Pages 129 - 138

https://doi.org/10.1145/1810295.1810314

Published: 01 May 2010 Publication History

Get Access

Abstract

This paper describes the evolution of a software testing effort during a critical period for the flagship Mars Science Laboratory rover project at the Jet Propulsion Laboratory. Formal specification for post-run analysis of log files, using a domain-specific language, LogScope, replaced scripted real-time analysis. Log analysis addresses the key problems of on-the-fly approaches and cleanly separates specification and execution. Mining the test repository suggested the inadequacy of the scripted approach, and encouraged a partly engineer-driven development. LogScope development should hold insights for others facing the tight deadlines and reactionary nature of testing for critical projects. LogScope received a JPL Mariner Award for "improving productivity and quality of the MSL Flight Software" and has been discussed as an approach for other flight missions. We note LogScope features that most contributed to ease of adoption and effectiveness. LogScope is general and can be applied to any software producing logs.

References

[1]

http://mars.jpl.nasa.gov/msl.

Google Scholar

[2]

J. H. Andrews and Y. Zhang. General test result checking with log file analysis. IEEE Transactions on Software Engineering, 29(7):634--648, 2003.

Digital Library

Google Scholar

[3]

H. Barringer, A. Groce, K. Havelund, and M. Smith. Formal analysis of log files. AIAA Journal of Aerospace Computing, Information and Communications, 2010. To appear.

Google Scholar

[4]

H. Barringer, K. Havelund, D. Rydeheard, and A. Groce. Rule systems for runtime verification: A short tutorial. In S. Bensalem and D. Peled, editors, Proc. of the 9th International Workshop on Runtime Verification (RV'09), volume 5779 of LNCS, pages 1--24. Springer, 2009.

Digital Library

Google Scholar

[5]

H. Barringer, D. Rydeheard, and K. Havelund. Rule Systems for Run-Time Monitoring: from Eagle to RuleR. In Proc. of the 7th International Workshop on Runtime Verification (RV'07), volume 4839 of LNCS, pages 111--125, Vancouver, Canada, 2007. Springer.

Digital Library

Google Scholar

[6]

H. Barringer, D. Rydeheard, and K. Havelund. Rule systems for run-time monitoring: from Eagle to RuleR. Journal of Logic and Computation, doi: 10.1093/logcom/exn076, 2008.

Digital Library

Google Scholar

[7]

M. Bennett, R. Borgen, K. Havelund, M. Ingham, and D. Wagner. Development of a prototype domain-specific language for monitor and control systems. In IEEE Aerospace Conference, Big Sky, Montana, March 2008.

Crossref

Google Scholar

[8]

A. Coen-Porisini, G. Denaro, C. Ghezzi, and M. Pezze. Using symbolic execution for verifying safety-critical systems. In European Software Engineering Conference/Foundations of Software Engineering, pages 142--151, 2001.

Digital Library

Google Scholar

[9]

L. Dillon, G. Kutty, L. Moser, P. M. Melliar-Smith, and Y. S. RamaKrishna. A graphical interval logic for specifying concurrent systems. 3(2):131--165, 1994.

Digital Library

Google Scholar

[10]

GraphViz. http://www.graphviz.org.

Google Scholar

[11]

R. Mateescu and D. Thivolle. A model checking language for concurrent value-passing systems. In The 15th international symposium on Formal Methods (FM 2008), volume 5014 of LNCS. Springer, May 2008. Turku, Finland.

Digital Library

Google Scholar

[12]

S. Squyres. Roving Mars: Spirit, Opportunity, and the Exploration of the Red Planet. Hyperion, 2005.

Google Scholar

[13]

M. Vardi. From Church and Prior to PSL. In 25 Years of Model Checking: History, Achievements, Perspectives, 2008.

Digital Library

Google Scholar

Cited By

View all

Falcone YKrstić SReger GTraytel D(2021)A taxonomy for classifying runtime verification toolsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-021-00609-zOnline publication date: 18-May-2021
https://doi.org/10.1007/s10009-021-00609-z
Kim JSavchenko VShin KSorokin KJeon HPankratenko GMarkov SKim CRothermel GBae D(2020)Automatic abnormal log detection by analyzing log history for providing debugging insightProceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice10.1145/3377813.3381371(71-80)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377813.3381371
Holmes JGroce A(2020)Using mutants to help developers distinguish and debug (compiler) faultsSoftware Testing, Verification and Reliability10.1002/stvr.172730:2Online publication date: 13-Jan-2020
https://doi.org/10.1002/stvr.1727
Show More Cited By

Index Terms

From scripts to specifications: the evolution of a flight software testing effort
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Requirements analysis
    2. Software verification and validation
      1. Software defect analysis
        Software testing and debugging

Recommendations

Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry
NASA Formal Methods
Abstract
Experimental aerospace projects often require flight vehicle platforms for testing, such as high-altitude balloons, sounding rockets, unmanned aerial systems (UAS), and CubeSats. The system telemetry transmitted by these vehicles is crucial to ...
Rule Systems for Runtime Verification: A Short Tutorial
Runtime Verification

In this tutorial, we introduce two rule-based systems for on and off-line trace analysis, RuleR and LogScope . RuleR is a conditional rule-based system, which has a simple and easily implemented algorithm for effective runtime verification, and ...
Challenges in testing and validating operational spacecraft simulators
GCMS '10: Proceedings of the 2010 Conference on Grand Challenges in Modeling & Simulation

Flight Control Teams (FCT) at the European Space Operations Centre (ESOC) of the European Space Agency (ESA), start flight operations training and preparation on a specific Spacecraft (S/C), about 3 years prior to launch through, mainly, the preparation ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '10: Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - Volume 2

May 2010

554 pages

ISBN:9781605587196

DOI:10.1145/1810295

General Chairs:
Jeff Kramer
Imperial College, London, UK
,
Judith Bishop
Microsoft Research, Redmond
,
Program Chairs:
Prem Devanbu
University of California at Davis
,
Sebastian Uchitel
University of Buenos Aires, Argentina and Imperial College London, UK

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]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 May 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE '10

Sponsor:

SIGSOFT

ICSE '10: 32nd International Conference on Software Engineering

May 1 - 8, 2010

Cape Town, South Africa

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
368
Total Downloads

Downloads (Last 12 months)8
Downloads (Last 6 weeks)1

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Falcone YKrstić SReger GTraytel D(2021)A taxonomy for classifying runtime verification toolsInternational Journal on Software Tools for Technology Transfer10.1007/s10009-021-00609-zOnline publication date: 18-May-2021
https://doi.org/10.1007/s10009-021-00609-z
Kim JSavchenko VShin KSorokin KJeon HPankratenko GMarkov SKim CRothermel GBae D(2020)Automatic abnormal log detection by analyzing log history for providing debugging insightProceedings of the ACM/IEEE 42nd International Conference on Software Engineering: Software Engineering in Practice10.1145/3377813.3381371(71-80)Online publication date: 27-Jun-2020
https://dl.acm.org/doi/10.1145/3377813.3381371
Holmes JGroce A(2020)Using mutants to help developers distinguish and debug (compiler) faultsSoftware Testing, Verification and Reliability10.1002/stvr.172730:2Online publication date: 13-Jan-2020
https://doi.org/10.1002/stvr.1727
Chaves LBessa IIsmail Hdos Santos Frutuoso ACordeiro Lde Lima Filho E(2018)DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial VehiclesIEEE Transactions on Reliability10.1109/TR.2018.287326067:4(1420-1441)Online publication date: Dec-2018
https://doi.org/10.1109/TR.2018.2873260
Holmes JGroce A(2018)Causal Distance-Metric-Based Assistance for Debugging after Compiler Fuzzing2018 IEEE 29th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE.2018.00027(166-177)Online publication date: Oct-2018
https://doi.org/10.1109/ISSRE.2018.00027
Holmes JGroce APinto JMittal PAzimi PKellar KO'brien J(2018)TSTLInternational Journal on Software Tools for Technology Transfer (STTT)10.1007/s10009-016-0445-y20:1(57-78)Online publication date: 1-Feb-2018
https://dl.acm.org/doi/10.1007/s10009-016-0445-y
Heikkinen EHamalainen T(2016)Behavior Mining Language for mining expected behavior from log filesIECON 2016 - 42nd Annual Conference of the IEEE Industrial Electronics Society10.1109/IECON.2016.7793774(4613-4618)Online publication date: Oct-2016
https://doi.org/10.1109/IECON.2016.7793774
Basin DCaronni GEreth SHarvan MKlaedtke FMantel H(2016)Scalable offline monitoring of temporal specificationsFormal Methods in System Design10.1007/s10703-016-0242-y49:1-2(75-108)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10703-016-0242-y
Hallé SKhoury R(2016)Runtime Monitoring of Stream Logic FormulaeFoundations and Practice of Security10.1007/978-3-319-30303-1_15(251-258)Online publication date: 25-Feb-2016
https://doi.org/10.1007/978-3-319-30303-1_15
Groce APinto JAzimi PMittal PYoung MXie T(2015)TSTL: a language and tool for testing (demo)Proceedings of the 2015 International Symposium on Software Testing and Analysis10.1145/2771783.2784769(414-417)Online publication date: 13-Jul-2015
https://dl.acm.org/doi/10.1145/2771783.2784769
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.

Cited By

Index Terms

Recommendations

Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry

Rule Systems for Runtime Verification: A Short Tutorial

Challenges in testing and validating operational spacecraft simulators