NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Back to Results
Spot: A Programming Language for Verified Flight SoftwareThe C programming language is widely used for programming space flight software and other safety-critical real time systems. C, however, is far from ideal for this purpose: as is well known, it is both low-level and unsafe. This paper describes Spot, a language derived from C for programming space flight systems. Spot aims to maintain compatibility with existing C code while improving the language and supporting verification with the SPIN model checker. The major features of Spot include actor-based concurrency, distributed state with message passing and transactional updates, and annotations for testing and verification. Spot also supports domain-specific annotations for managing spacecraft state, e.g., communicating telemetry information to the ground. We describe the motivation and design rationale for Spot, give an overview of the design, provide examples of Spot's capabilities, and discuss the current status of the implementation.
Document ID
20160005629
Acquisition Source
Jet Propulsion Laboratory
Document Type
Conference Paper
External Source(s)
Authors
Bocchino, Robert L., Jr.
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Gamble, Edward
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Gostelow, Kim P.
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Some, Raphael R.
(Jet Propulsion Lab., California Inst. of Tech. Pasadena, CA, United States)
Date Acquired
May 2, 2016
Publication Date
October 18, 2014
Subject Category
Computer Programming And Software
Meeting Information
Meeting: ACM High-Integrity Language Technology (HILT) 2014
Location: Portland, OR
Country: United States
Start Date: October 18, 2014
End Date: October 21, 2014
Sponsors: Association for Computing Machinery
Distribution Limits
Public
Copyright
Other
Keywords
validation
SPIN
model checking
verification
programming languages
concurrent real-time systems
state
avionics

Available Downloads

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