Regression Test-Driven Extension of PLEXIL5: Support for Update Nodes

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 PLEXIL Update Nodes 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 y completitud en comparación con el 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 e para los nodos Update de PLEXIL en PLEXIL5. La estrategia seguida consiste en aprovechar las pruebas de regresión oficiales del PLEXIL Executive. La comparación automática entre las ejecuciones de las pruebas oficiales que se ejecutan en el PLEXIL Executive y en PLEXIL5 es una medida de la corrección e integridad del intérprete formal respecto a la implementación de referencia.

[CA] Aquest projecte descriu l’esforç d’extensió de PLEXIL5, un intèrpret formal de PLEXIL especicat en el motor de lògica de reescriptura Maude, per aconseguir majors graus de correcció i completitud en comparació amb el PLEXIL Executive, l’intèrpret ocial de PLEXIL. PLEXIL5 està basat en una versió anterior de PLEXIL i ha quedat obsoleta. Aquest projecte pretén introduir suport per als nodes Update de PLEXIL en PLEXIL5. L’estratègia seguida consistix en aprotar les proves de regressió ocials del PLEXIL Executive. La comparació automàtica entre les execucions de les proves ocials en el PLEXIL Executive i en PLEXIL5 és una mesura de la correcció i completitud de l’intèrpret formal respecte a la implementació de referència.