An Algorithm to Translate PARADIGM specifications to PLTL

Gomez, R.S. and Augusto, Juan Carlos and Acuña, Silvia.T. (2003) An Algorithm to Translate PARADIGM specifications to PLTL. In: Proceedings of the 3ras. Jornadas Iberoamericanas de Ingenieria de Software e Ingenieria de Conocimiento (JIISIC'03). , Valdivia, Chile pp. 53-63. (The full text of this publication is not available from this repository)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL
http://www.cs.kent.ac.uk/pubs/2003/1864

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.

Item Type: Conference or workshop item (UNSPECIFIED)
Uncontrolled keywords: Distributed systems, Temporal Logics, Specification Languages
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Science Technology and Medical Studies > School of Computing > Theoretical Computing Group
Depositing User: Mark Wheadon
Date Deposited: 24 Nov 2008 18:00
Last Modified: 14 Apr 2014 08:47
Resource URI: http://kar.kent.ac.uk/id/eprint/13883 (The current URI for this page, for reference purposes)
  • Depositors only (login required):