NASA Jet Propulsion Laboratory California Institute of Technology Follow this link to skip to the main content

BEACON eSpace at Jet Propulsion Laboratory >
JPL Technical Report Server >
JPL TRS 1992+ >

Please use this identifier to cite or link to this item:

Title: SPIN or LURCH : a comparative assessment of model cheching and stochastic search for temporal properties in procedural code.
Authors: Powell, John D.
Owens, David
Menzies, Tim
Keywords: stochastic search
model checking
Issue Date: Sep-2004
Publisher: Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2004.
Citation: IEEE Workshop on Intelligent Technologies for Software Engineering, Linz, Austria, September 2004.
Abstract: The difficulty of how to test large systems, such as the one on board a NASA robotic remote explorer (RRE) vehicle, is fundamentally a search issue: the global state space representing all possible has yet to be solved, even after many decades of work. Randomized algorithms have been known to outperform their deterministic counterparts for search problems representing a wide range of applications. In the case study presented here, the LURCH randomized algorithm proved to be adequate to the task of testing a NASA RRE vehicle. LURCH found all the errors found by an earlier analysis of a more complete method (SPIN). Our empirical results are that LURCH can scale to much larger models than standard model checkers like SMV and SPIN. Further, the LURCH analysis was simpler than the SPIN analysis. The simplicity and scalability of LURCH are two compelling reasons for experimenting further with this tool.
Appears in Collections:JPL TRS 1992+

Files in This Item:

File Description SizeFormat
04-2278A.pdf2.14 MBAdobe PDFView/Open

Items in DSpace are protected by copyright, but are furnished with U.S. government purpose use rights.


Privacy/Copyright Image Policy Beacon Home Contact Us
NASA Home Page + Div 27
+ JPL Space
Site last updated on December 5, 2014.
If you have any comments or suggestions for this web site, please e-mail Robert Powers.