Search NASA⌕ Search
Home/Archive/NASA NTRS

NASA NTRS · 20160005629

Spot: A Programming Language for Verified Flight Software

Bocchino, Robert L., Jr.·Gamble, Edward·Gostelow, Kim P.·Some, Raphael R.
View original source ↗Export metadata ↓

Abstract

The 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.

Explore related subjects

validationSPINmodel checkingverificationprogramming languagesconcurrent real-time systemsstateavionics

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Bocchino, Robert L., Jr., Gamble, Edward, Gostelow, Kim P., Some, Raphael R.. 2014-10-18. Spot: A Programming Language for Verified Flight Software. https://ntrs.nasa.gov/citations/20160005629

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related reports

NASA NTRS2018

LaSRC (Land Surface Reflectance Code): Overview, Application and Validation Using MODIS, VIIRS, LANDSAT and Sentinel 2 Data's

This paper presents a generic approach developed to derive surface reflectance over land from a variety of sensors. This technique builds on the extensive dataset acquired by the Terra platform by combining MODIS and MISR to derivean explicit and dynamic map of band ratio's between blue and red channels and is a refinement of the operational approach used for MODIS and LANDSAT over the past 15 years. We will present the generic approach and the application to MODIS VIIRS, LANDSAT and Sentinel 2 data's and its validation using the AERONET data.

validation↗
NASA NTRS2018

A Generic Approach for Inversion of Surface Reflectance over Land: Overview, Application and Validation Using MODIS and LANDSAT8 Data

This paper presents a generic approach developed to derive surface reflectance over land from a variety of sensors. This technique builds on the extensive dataset acquired by the Terra platform by combining MODIS and MISR to derive an explicit and dynamic map of band ratio's between blue and red channels and is a refinement of the operational approach used for MODIS and LANDSAT over the past 15 years. We will present the generic approach and the application to MODIS and LANDSAT data and its validation using the AERONET data.

validation↗
NASA NTRS2018

Comparison of the Integrated Medical Model Predictions to Real World ISS and STS Observations

The Human Research Program funded the development of the integrated medical model (IMM) to quantify the medical component of overall mission risk. The IMM uses Monte Carlo methodology to integrate space flight and ground medical data to assess the probability of mission medical outcomes and resource utilization. To determine the credibility of IMM output the IMM project team completed two validation studies that compare IMM output to observed medical events from a selection of Shuttle Transportation System (STS) and International Space Station (ISS) missions.

validation↗