Analysis and testing of PLEXIL plans

Jason Biatek, Michael W Whalen, Mats Heimdahl, Sanjai Rayadurgam, Michael R. Lowry

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Scopus citations

Abstract

Autonomy is increasingly important in missions to remote locations (e.g., space applications and deep sea exploration) since limited bandwidth and communication delays make detailed instructions from a remote base (e.g., Earth or a land base) impractical. The planning systems used for autonomous operation are difficult to verify and validate because they must create plans for use in a specific environment and the correct behavior might not be easy to define. To explore verification and validation of planning systems, we have developed a verification framework for the PLEXIL plan execution language. The framework allows us to perform verification and test case generation using Java Symbolic PathFinder. Using this framework, we have performed verification, bounded verification and test-case generation for NASA-relevant PLEXIL plans and discovered two bugs in the PLEXIL language semantics: one in the definition of the If/Then/Else construct in the Extended PLEXIL language that could lead to plan deadlocks, and one in the semantics of the core language that could cause the PLEXIL executive to crash.

Original languageEnglish (US)
Title of host publication2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014 - Proceedings
PublisherAssociation for Computing Machinery, Inc
Pages52-58
Number of pages7
ISBN (Electronic)9781450328531
DOIs
StatePublished - Jun 3 2014
Event2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014 - Hyderabad, India
Duration: Jun 3 2014 → …

Publication series

Name2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014 - Proceedings

Other

Other2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014
CountryIndia
CityHyderabad
Period6/3/14 → …

Keywords

  • Automatic test generation
  • Java
  • Java PathFinder

Fingerprint Dive into the research topics of 'Analysis and testing of PLEXIL plans'. Together they form a unique fingerprint.

  • Cite this

    Biatek, J., Whalen, M. W., Heimdahl, M., Rayadurgam, S., & Lowry, M. R. (2014). Analysis and testing of PLEXIL plans. In 2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014 - Proceedings (pp. 52-58). (2nd FME Workshop on Formal Methods in Software Engineering, FormaliSE 2014 - Proceedings). Association for Computing Machinery, Inc. https://doi.org/10.1145/2593489.2593496