A Formal Interactive Verification Environment for the Plan Execution Interchange Language

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.

• Autores: Cadavid Rengifo, Hector Fabio; Rocha, Camilo; Muñoz, Cesar
• Tipo de recurso: Part of book
• Fecha de publicación: 2012
• Institución: Escuela Colombiana de Ingeniería Julio Garavito
• Repositorio: Repositorio Institucional ECI
• Idioma: eng
• OAI Identifier: oai:repositorio.escuelaing.edu.co:001/1838
• Acceso en línea: https://repositorio.escuelaing.edu.co/handle/001/1838
• Palabra clave: Comprobación del modelo; Lógica Temporal Lineal; Proposición atómica; Lenguaje síncrono; Estructura Kripke; Model Check; Linear Temporal Logic; Atomic Proposition; Plan Execution; Kripke Structure
• Rights: closedAccess
• License: © Springer Nature Switzerland AG 2018