<?xml version="1.0" encoding="UTF-8"?><xml><records><record><source-app name="Biblio" version="6.x">Drupal-Biblio</source-app><ref-type>5</ref-type><contributors><authors><author><style face="normal" font="default" size="100%">Parisaca Vargas, Abigail</style></author><author><style face="normal" font="default" size="100%">Ana Garis</style></author><author><style face="normal" font="default" size="100%">Tarifa, S.LizethTapia</style></author><author><style face="normal" font="default" size="100%">George, Chris</style></author></authors><secondary-authors><author><style face="normal" font="default" size="100%">Leuschel, Michael</style></author><author><style face="normal" font="default" size="100%">Wehrheim, Heike</style></author></secondary-authors></contributors><titles><title><style face="normal" font="default" size="100%">Model Checking LTL Formulae in RAISE with FDR</style></title><secondary-title><style face="normal" font="default" size="100%">Integrated Formal Methods</style></secondary-title><tertiary-title><style face="normal" font="default" size="100%">Lecture Notes in Computer Science</style></tertiary-title></titles><keywords><keyword><style  face="normal" font="default" size="100%">CSP</style></keyword><keyword><style  face="normal" font="default" size="100%">FDR</style></keyword><keyword><style  face="normal" font="default" size="100%">formal methods</style></keyword><keyword><style  face="normal" font="default" size="100%">LTL</style></keyword><keyword><style  face="normal" font="default" size="100%">model checking</style></keyword><keyword><style  face="normal" font="default" size="100%">RAISE</style></keyword><keyword><style  face="normal" font="default" size="100%">refinement</style></keyword><keyword><style  face="normal" font="default" size="100%">RSL</style></keyword><keyword><style  face="normal" font="default" size="100%">tools</style></keyword></keywords><dates><year><style  face="normal" font="default" size="100%">2009</style></year></dates><urls><related-urls><url><style face="normal" font="default" size="100%">https://haslab.uminho.pt/sites/default/files/agaris/files/ifm09.pdf</style></url></related-urls></urls><publisher><style face="normal" font="default" size="100%">Springer Berlin Heidelberg</style></publisher><pub-location><style face="normal" font="default" size="100%">Düsseldorf, Germany</style></pub-location><volume><style face="normal" font="default" size="100%">5423</style></volume><pages><style face="normal" font="default" size="100%">231-245</style></pages><isbn><style face="normal" font="default" size="100%">978-3-642-00254-0</style></isbn><language><style face="normal" font="default" size="100%">eng</style></language><abstract><style face="normal" font="default" size="100%">&lt;p&gt;The Raise Specification Language (RSL) is a modeling language which 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 CSPM and translates LTL formulas to CSP processes, enabling the model checking of LTL formulas over RSL descriptions with FDR.&lt;/p&gt;
</style></abstract></record></records></xml>