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: | 9780769534039 |
| ISSN: | 15224902 |
| Appears in Collections: | Artículos de investigació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.