NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
SPIN or LURCH : a Comparative Assessment of Model Checking and Stochastic Search for Temporal Properties in Procedural CodeThe 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.
Document ID
20110015996
Acquisition Source
Jet Propulsion Laboratory
Document Type
Conference Paper
External Source(s)
Authors
Powell, John D.
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Owens, David
Menzies, Tim
(Portland State Univ. OR, United States)
Date Acquired
August 25, 2013
Publication Date
September 1, 2004
Subject Category
Cybernetics, Artificial Intelligence And Robotics
Meeting Information
Meeting: IEEE Workshop on Intelligent Technologies for Software Engineering
Location: Linz
Country: Austria
Start Date: September 1, 2004
Sponsors: Institute of Electrical and Electronics Engineers
Distribution Limits
Public
Copyright
Other
Keywords
verification
stochastic search
model checking

Available Downloads

There are no available downloads for this record.
No Preview Available