Alex Groce
Klaus Havelund
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.
- http://mars.jpl.nasa.gov/msl.Google Scholar
- J. H. Andrews and Y. Zhang. General test result checking with log file analysis. IEEE Transactions on Software Engineering, 29(7):634--648, 2003. Google ScholarDigital Library
- 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
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- GraphViz. http://www.graphviz.org.Google Scholar
- 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. Google ScholarDigital Library
- S. Squyres. Roving Mars: Spirit, Opportunity, and the Exploration of the Red Planet. Hyperion, 2005.Google Scholar
- M. Vardi. From Church and Prior to PSL. In 25 Years of Model Checking: History, Achievements, Perspectives, 2008. Google ScholarDigital Library
Index Terms
- From scripts to specifications: the evolution of a flight software testing effort
Recommendations
Elucidation and Analysis of Specification Patterns in Aerospace System Telemetry
NASA Formal MethodsAbstractExperimental 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 VerificationIn 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 & SimulationFlight 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