Mi DSpace
Please use this identifier to cite or link to this item: http://hdl.handle.net/UCSP/15901
Title: Model checking LTL formulae in RAISE with FDR
Authors: Parisaca Vargas, Abigail
Gabriela Garis, Ana
Tapia Tarifa, Silvia Lizeth
George, Chris
Keywords: CSP;FDR;LTL;RAISE;Refinement;RSL;Computer operating procedures;Formal methods;Specifications;Temporal logic;Model checking
Issue Date: 2009
Publisher: Scopus
metadata.dc.relation.uri: https://www.scopus.com/inward/record.uri?eid=2-s2.0-67650508575&doi=10.1007%2f978-3-642-00255-7-16&partnerID=40&md5=93151dfd98a4b410f2b6d4c49f757df6
Abstract: TheRaise SpecificationLanguage (RSL) is a modeling languagewhich supports various specification styles. To apply model checking to RSL concurrent descriptions, we translate RSL specifications into the input language CSPM of FDR. FDR is the model checker for the process algebra CSP. First, we define a syntactic and semantic translation from the concurrent applicative subset of RSL to CSPM, and show that this translation is a strong bisimulation which preserves properties such as traces and deadlock. Consequently, results obtained by refinement checks in FDR are sound for the original RSL descriptions. Second, RSL uses Linear Temporal Logic (LTL) to specify desired properties, but FDR does not support LTL. LTL formulas may be translated to CSP test processes in order to check them with FDR.We build a tool which automates the translation of RSL specifications into CSPMand translates LTL formulas to CSP processes, enabling the model checking of LTL formulas over RSL descriptions with FDR. © Springer-Verlag Berlin Heidelberg 2009.
URI: http://repositorio.ucsp.edu.pe/handle/UCSP/15901
ISBN: urn:isbn:9783642002540
ISSN: 3029743
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.