Analysis and testing of PLEXIL plans

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.