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


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

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


    Beteiligte:

    Erschienen in:

    Erscheinungsdatum :

    2016-03-01


    Format / Umfang :

    727744 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Progress towards flight software hybrid controllers from formal specifications

    Haesaert, S. / Reder, L.J. / Murray, R.M. | IEEE | 2018



    Software interfacing of flight data

    Phillips, M. R. | NTRS | 1971


    Automated statechart model checking

    Mikk, E. / Pingree, P. J. | NTRS | 2002


    Generation of Object-Oriented Formal Software Specifications

    Karagias, T. / Hartrum, T. / IEEE | British Library Conference Proceedings | 1997