JPL Technical Report Server

Spot: a programming language for verified flight software

Show simple item record Bocchino Jr., Robert L. Gamble, Edward Gostelow, Kim P. Some, Raphael R. 2016-04-13T17:33:15Z 2016-04-13T17:33:15Z 2014-10-18
dc.identifier.citation ACM High-Integrity Language Technology (HILT) 2014, Portland, Oregon, October 18-21, 2014 en_US
dc.identifier.clearanceno 14-3638
dc.description.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 pa- per 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 up- dates, and annotations for testing and verification. Spot also supports domain-specific annotations for managing space- craft 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. en_US
dc.description.sponsorship NASA/JPL en_US
dc.language.iso en_US en_US
dc.publisher Pasadena, CA : Jet Propulsion Laboratory, National Aeronautics and Space Administration, 2014 en_US
dc.subject avionics en_US
dc.subject concurrent real-time systems en_US
dc.subject programming languages en_US
dc.subject state en_US
dc.subject verification en_US
dc.subject validation en_US
dc.subject model checking en_US
dc.subject SPIN en_US
dc.title Spot: a programming language for verified flight software en_US
dc.type Preprint en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record



My Account