A Formal Interactive Verification Environment for the Plan Execution Interchange Language

Abstract

The Plan Execution Interchange Language (PLEXIL) is an open source synchronous language developed by NASA for commanding and monitoring autonomous systems. This paper reports the development of the PLEXIL’s Formal Interactive Verification Environment (PLEXIL5), a graphical interface to the formal executable semantics of PLEXIL. Among its main features, PLEXIL5 provides model checking of plans with support for formula editing and visualization of counterexamples, interactive simulation of plans at different granularity levels, and random initialization of external environment variables. The formal verification capabilities of PLEXIL5 are illustrated by means of a human-automation interaction model.

El lenguaje de intercambio de ejecución de planes (PLEXIL) es un lenguaje síncrono de código abierto desarrollado por la NASA para controlar y monitorear sistemas autónomos. Este documento informa sobre el desarrollo del entorno de verificación interactivo formal de PLEXIL (PLEXIL5), una interfaz gráfica para la semántica ejecutable formal de PLEXIL. Entre sus principales características, PLEXIL5 proporciona verificación de modelos de planes con soporte para edición de fórmulas y visualización de contraejemplos, simulación interactiva de planes en diferentes niveles de granularidad e inicialización aleatoria de variables de entorno externo. Las capacidades de verificación formal de PLEXIL5 se ilustran mediante un modelo de interacción humano-automatización.