© University of Kent - Contact | Feedback | Legal | FOI | Cookies
An Algorithm to Translate PARADIGM specifications to PLTL
Rodolfo S. Gomez, Juan C. Augusto, and Silvia T. Acua
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 kbytesBibtex Record
@inproceedings{1864, author = {Rodolfo S. Gomez and Juan C. Augusto and Silvia T. Acua}, 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}, }