Automated planning systems (APS) are gaining acceptance for use on NASA missions as evidenced by APS flown on missions such as Earth Orbiter 1 and Deep Space 1, both of which were commanded by onboard planning systems. The planning system takes high level goals and expands them onboard into a detailed plan of action that the spacecraft executes. The system must be verified to ensure that the automatically generated plans achieve the goals as expected and do not generate actions that would harm the spacecraft or mission. These systems are typically tested using empirical methods. Formal methods, such as model checking, offer exhaustive or measurable test coverage which leads to much greater confidence in correctness. 1 2 This paper describes a formal method based on the SPIN model checker. This method guarantees that possible plans meet certain desirable properties. We express the input model in Promela, the language of SPIN [1] [2] and express the properties of desirable plans formally. The Promela model is then checked by SPIN to see if it contains violations of the properties, which are reported as errors. We have applied this approach to an APS and found a defect.


    Zugriff

    Zugriff prüfen

    Verfügbarkeit in meiner Bibliothek prüfen

    Bestellung bei Subito €


    Exportieren, teilen und zitieren



    Titel :

    Model Checking Autonomous Planners: Even the B est L aid P lans M ust be V erified


    Beteiligte:
    Smith, M.H. (Autor:in) / Holzmann, G.J. (Autor:in) / Cucullu, G.C. (Autor:in) / Smith, B.D. (Autor:in)

    Erschienen in:

    Erscheinungsdatum :

    01.01.2005


    Format / Umfang :

    1650483 byte




    Medientyp :

    Aufsatz (Konferenz)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch



    Model Checking Autonomous Planners: Even the Best Laid Plans Must be Verified

    Smith, M. H. / Cucullu, G. C. / Smith, B. D. et al. | British Library Conference Proceedings | 2005


    Model Checking Artificial Intelligence Based Planners: Even the Best Laid Plans Must Be Verified

    Smith, Margaret H. / Holzmann, Gerard J. / Cucullu, Gordon C., III et al. | NTRS | 2005


    Model checking for autonomous vehicles

    FERGUSON DAVID I / DOLGOV DMITRI A / URMSON CHRISTOPHER | Europäisches Patentamt | 2016

    Freier Zugriff

    TOOLS FOR PERFORMANCE TESTING AND/OR TRAINING AUTONOMOUS VEHICLE PLANNERS

    EIRAS FRANCISCO / HAWASLY MAJD / RAMAMOORTHY SUBRAMANIAN | Europäisches Patentamt | 2024

    Freier Zugriff

    TOOLS FOR PERFORMANCE TESTING AND/OR TRAINING AUTONOMOUS VEHICLE PLANNERS

    EIRAS FRANCISCO / HAWASLY MAJD / RAMAMOORTHY SUBRAMANIAN | Europäisches Patentamt | 2022

    Freier Zugriff