Browse wiki

From MurrayWiki
Jump to: navigation, search
Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications
Abstract This paper describes the implementation of …
This paper describes the implementation of an in- terface 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-certified2 implementation code. The functionality of the interface is demonstrated through three example systems of varying com- plexity 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.
of the composition may still be required.  +
Authors Sumanth Dathathri, Scott C. Livingston, Leonard J. Reder, and Richard M. Murray  +
Funding JPL SR&D15 +
ID 2015m  +
Source IEEE Aerospace Conference, 2016  +
Tag dlrm16-ieeeaero  +
Title Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications +
Type Conference paper  +
Categories Papers
Modification date
This property is a special property in this wiki.
19 May 2016 12:54:18  +
URL
This property is a special property in this wiki.
http://resolver.caltech.edu/CaltechCDSTR:2016.001  +
hide properties that link here 
Interfacing TuLiP with the JPL Statechart Autocoder: Initial progress toward synthesis of flight software from formal specifications + Title
 

 

Enter the name of the page to start browsing from.