Formal Interactive Verification Environment for the Plan Execution Interchange Language (PLEXIL5)(LAR-19339-1)

The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. PLEXIL Formal Interactive Verification Environment (PLEXIL5) is a tool that implements a formal executable semantics of PLEXIL. PLEXIL5 includes a graphical interface that enable access to formal verification techniques such as model-checking, symbolic execution, theorem proving, and static analysis of plans. The graphical environment supports formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables.