• DocumentCode
    3515963
  • Title

    Verification of Plans and Procedures

  • Author

    Brat, G. ; Gheorghiu, M. ; Giannakopoulou, D. ; Pasareanu, C.

  • Author_Institution
    USRA/RIACS, NASA Ames Res. Center, Moffett Field, CA
  • fYear
    2008
  • fDate
    1-8 March 2008
  • Firstpage
    1
  • Lastpage
    8
  • Abstract
    Procedures and plans are used across NASA missions. For example, astronaut activities on the International Space Station are regulated by procedures which are uploaded from the ground. It is critical that these procedures are verified and validated before being executed by astronauts. This paper describes how we are applying advanced formal verification techniques, such as model checking, to plans and procedures expressed in semantically well-defined languages such as PRL and PLEXIL.
  • Keywords
    aerospace computing; formal verification; NASA missions; PLEXIL; PRL; astronaut activities; formal verification techniques; Automata; Control systems; Government; Humans; International Space Station; NASA; Power system modeling; Safety; Space shuttles; Space technology;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Aerospace Conference, 2008 IEEE
  • Conference_Location
    Big Sky, MT
  • ISSN
    1095-323X
  • Print_ISBN
    978-1-4244-1487-1
  • Electronic_ISBN
    1095-323X
  • Type

    conf

  • DOI
    10.1109/AERO.2008.4526574
  • Filename
    4526574
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=3515963