School of Computing

An Algorithm to Translate PARADIGM specifications to PLTL

Rodolfo S. Gomez, Juan C. Augusto, and Silvia T. Acu�a

In Proceedings of the 3ras. Jornadas Iberoamericanas de Ingenieria de Software e Ingenieria de Conocimiento (JIISIC'03), pages 182-196, Valdivia, Chile, November 2003.

Abstract

PARADIGM has recently emerged as a new language to design cooperative object-oriented systems. To our knowledge, PARADIGM temporal aspects have not been studied before.

Here we describe a polynomial algorithm to translate PARADIGM models to Propositional Linear Temporal Logic programs. The resulting program is an executable specification of the modelled system, suitable for verifying model properties. It is also a declarative view of the model. Therefore we provide a temporal framework to understand and reason about PARADIGM models behavior, and system development in general. Finally, we believe this work provides further evidence on the benefits that PARADIGM has to offer to the Software Engineering community. We complement a previous conference paper which introduced the main concepts behind the translation process and its application to system verification.

Download publication 127 kbytes

Bibtex Record

@inproceedings{1864,
author = {Rodolfo S. Gomez and Juan C. Augusto and Silvia T. Acu�a},
title = {{A}n {A}lgorithm to {T}ranslate {PARADIGM} specifications to {PLTL}},
month = {November},
year = {2003},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2003/1864},
    publication_type = {inproceedings},
    submission_id = {25077_1080902060},
    booktitle = {Proceedings of the 3ras. Jornadas Iberoamericanas de Ingenieria de Software e Ingenieria de Conocimiento (JIISIC'03)},
    address = {Valdivia, Chile},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014