CaltechAUTHORS
  A Caltech Library Service

Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications

Dathathri, Sumanth and Livingston, Scott C. and Reder, Leonard J. and Murray, Richard M. (2016) Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications. California Institute of Technology , Pasadena, CA. http://resolver.caltech.edu/CaltechCDSTR:2016.001

[img] PDF - Accepted Version
See Usage Policy.

3403Kb

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCDSTR:2016.001

Abstract

This paper describes the implementation of an interface connecting the two tools : the JPL SCA (Statechart Autocoder) and TuLiP (Temporal Logic Planning Toolbox) to enable the automatic synthesis of low level implementation code directly from formal specifications. With system dynamics, bounds on uncertainty and formal specifications as inputs, TuLiP synthesizes Mealy machines that are correct-by-construction. An interface is built that automatically translates these Mealy machines into UML statecharts. The SCA accepts the UML statecharts (as XML files) to synthesize flight-certified implementation code. The functionality of the interface is demonstrated through three example systems of varying complexity a) a simple thermostat b) a simple speed controller for an autonomous vehicle and c) a more complex speed controller for an autonomous vehicle with a map-element. In the thermostat controller, there is a specification regarding the desired temperature range that has to be met despite disturbance from the environment. Similarly, in the speed-controllers there are specifications about safe driving speeds depending on sensor health (sensors fail unpredictably) and the map-location. The significance of these demonstrations is the potential circumventing of some of the manual design of statecharts for flight software/controllers. As a result, we expect that less testing and validation will be necessary. In applications where the products of synthesis are used alongside manually designed components, extensive testing or new certificates of correctness of the composition may still be required.


Item Type:Report or Paper (Technical Report)
Related URLs:
URLURL TypeDescription
http://dx.doi.org/http://dx.doi.org/10.1109/AERO.2016.7500557DOIConference Paper
ORCID:
AuthorORCID
Murray, Richard M.0000-0002-5785-7481
Additional Information:This work is funded by the NASA, Jet Propulsion Laboratory, Technology Program Office through a Spontaneous Research and Development award to demonstrate the feasibility of utilizing TuLiP and SCA for creating flight-like controllers from formal specification.
Group:Control and Dynamical Systems Technical Reports
Funders:
Funding AgencyGrant Number
NASA/JPLUNSPECIFIED
JPL Research and Technology Development FundUNSPECIFIED
Record Number:CaltechCDSTR:2016.001
Persistent URL:http://resolver.caltech.edu/CaltechCDSTR:2016.001
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:65663
Collection:CaltechCDSTR
Deposited By: Sumanth Dathathri
Deposited On:30 Mar 2016 22:41
Last Modified:27 Jul 2017 21:35

Repository Staff Only: item control page