Mi DSpace
Please use this identifier to cite or link to this item: http://hdl.handle.net/UCSP/15906
Title: A translation from RSL to CSP
Authors: Parisaca Vargas, Abigail
Tapia Tarifa, Silvia Lizeth
George, Chris
Keywords: Computer operating procedures;Computers; Formal methods;Information theory;Linguistics;Specifications;Translation (languages);CSP;FDR;RAISE;Refinement;RSL;Model checking
Issue Date: 2008
Publisher: Scopus
metadata.dc.relation.uri: https://www.scopus.com/inward/record.uri?eid=2-s2.0-58049183882&doi=10.1109%2fSCCC.2008.20&partnerID=40&md5=c4c545b7b5e1230d7956642f657d5d68
Abstract: The Raise Specification Language (RSL) is a broad spectrum modeling language which supports a wide range of specification styles. In order to apply verification techniques based on model checking to descriptions of concurrent systems in RSL, we translate RSL specifications into the input language CSPM of the FDR model checker. FDR is a well-established model checker for the process algebra CSP. However, we need to show that the analysis performed in FDR carry over to the original RSL specifications. For this purpose, we define a syntactic and semantic translation between RSL and CSPM, and show that this translation is in fact a strong bisimulation which preserves various properties such as traces and deadlock. Finally, we have built a tool which automates the translation of RSL specifications into CSPM following this approach. © 2008 IEEE.
URI: http://repositorio.ucsp.edu.pe/handle/UCSP/15906
ISBN: urn:isbn:9780769534039
ISSN: 15224902
Appears in Collections:Artículos - Ciencia de la computación

Files in This Item:
There are no files associated with this item.

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.