Browsing by Author "Parisaca Vargas, Abigail"

Now showing 1 - 2 of 2
  • No Thumbnail Available
    Item
    A translation from RSL to CSP
    (Scopus, 2008) Parisaca Vargas, Abigail; Tapia Tarifa, Silvia Lizeth; George, Chris
    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.
  • No Thumbnail Available
    Item
    Model checking LTL formulae in RAISE with FDR
    (Scopus, 2009) Parisaca Vargas, Abigail; Gabriela Garis, Ana; Tapia Tarifa, Silvia Lizeth; George, Chris
    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.