NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Verification of Plan Models Using UPPAALThis paper describes work on the verification of HSTS, the planner and scheduler of the Remote Agent autonomous control system deployed in Deep Space 1 (DS1). The verification is done using UPPAAL, a real time model checking tool. We start by motivating our work in the introduction. Then we give a brief description of HSTS and UPPAAL. After that, we give a mapping of HSTS models into UPPAAL and we present samples of plan model properties one may want to verify. Finally, we conclude with a summary.
Document ID
20010081322
Acquisition Source
Ames Research Center
Document Type
Preprint (Draft being sent to journal)
Authors
Khatib, Lina
(QSS Group, Inc. Brook Park, OH United States)
Muscettola, Nicola
(NASA Ames Research Center Moffett Field, CA United States)
Haveland, Klaus
(RECOM Technologies, Inc. Moffett Field, CA United States)
Lau, Sonic
Date Acquired
September 7, 2013
Publication Date
January 15, 2001
Subject Category
Computer Programming And Software
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.
No Preview Available