Regression Test-Driven Extension of PLEXIL5: Support for Arrays

Abstract

[EN] This project describes the extension effort of PLEXIL5, a PLEXIL formal interpreter specified in the rewriting logic engine Maude, to achieve higher degrees of correctness and completeness with respect to the PLEXIL Executive, the official PLEXIL interpreter. PLEXIL5 is based on a former version of PLEXIL and has become deprecated. This project aims to introduce support for arrays into PLEXIL5. The strategy followed consists of leveraging the official regression tests of the PLEXIL Executive. The automatic comparison between the executions of the official tests running on the Executive and in PLEXIL5 is a measure of the formal interpreter correctness and completeness with respect to the reference implementation.

[ES] Este proyecto describe el esfuerzo de extensión de PLEXIL5, un intérprete formal de PLEXIL especificado en el motor lógico de reescritura Maude, para lograr mayores grados de corrección e integridad con respecto a PLEXIL Executive, el intérprete oficial de PLEXIL. PLEXIL5 está basado en una versión anterior de PLEXIL y ha quedado obsoleto. Este proyecto tiene como objetivo introducir soporte para arreglos en PLEXIL5. La estrategia seguida consiste en aprovechar las pruebas de regresión oficiales del Ejecutivo de PLEXIL. La comparación automática entre las ejecuciones de las pruebas oficiales que se ejecutan en Executive y en PLEXIL5 es una medida de la corrección e integridad del intérprete formal con respecto a la implementación de referencia.

[CA] Aquest projecte descriu l'esforç d'extensió de PLEXIL5, un intèrpret formal de PLEXIL especificat en el llenguatge de reescritura Maude, per aconseguir majors graus de correcció i completitud respecte al PLEXIL Executive, l'intèrpret oficial. PLEXIL és un llenguatge creat per a la representació d'esquemes d'automatització utilitzats principalment en robòtica i vehicles autònoms. PLEXIL5 es basa en una versió anterior de PLEXIL i ha quedat obsolet. Aquest projecte pretén introduir en PLEXIL5 el suport per a matrius. L'estratègia seguida consisteix a aprofitar les proves de regressió oficials del PLEXIL Executive. La comparació automàtica entre les ejecucions de les proves oficials executades en l'executiu i en PLEXIL5 és una mesura de la correcció i la completitud de l'interpretació formal respecte a la implementació de referència.