Model checking LTL formulae in RAISE with FDR

Simple item page
dc.contributor.authorParisaca Vargas, Abigail
dc.contributor.authorGabriela Garis, Ana
dc.contributor.authorTapia Tarifa, Silvia Lizeth
dc.contributor.authorGeorge, Chris
dc.date.accessioned2019-01-29T22:19:56Z
dc.date.available2019-01-29T22:19:56Z
dc.date.issued2009
dc.description.abstractTheRaise 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.es_PE
dc.description.uriTrabajo académicoes_PE
dc.identifier.doihttps://doi.org/10.1007/978-3-642-00255-7-16es_PE
dc.identifier.isbnurn:isbn:9783642002540es_PE
dc.identifier.issn3029743es_PE
dc.identifier.urihttps://hdl.handle.net/20.500.12590/15901
dc.language.isoenges_PE
dc.publisherScopuses_PE
dc.relation.urihttps://www.scopus.com/inward/record.uri?eid=2-s2.0-67650508575&doi=10.1007%2f978-3-642-00255-7-16&partnerID=40&md5=93151dfd98a4b410f2b6d4c49f757df6es_PE
dc.rightsinfo:eu-repo/semantics/restrictedAccesses_PE
dc.sourceRepositorio Institucional - UCSPes_PE
dc.sourceUniversidad Católica San Pabloes_PE
dc.sourceScopuses_PE
dc.subjectCSPes_PE
dc.subjectFDRes_PE
dc.subjectLTLes_PE
dc.subjectRAISEes_PE
dc.subjectRefinementes_PE
dc.subjectRSLes_PE
dc.subjectComputer operating procedureses_PE
dc.subjectFormal methodses_PE
dc.subjectSpecificationses_PE
dc.subjectTemporal logices_PE
dc.subjectModel checkinges_PE
dc.subject.ocdehttps://purl.org/pe-repo/ocde/ford#1.02.00es_PE
dc.titleModel checking LTL formulae in RAISE with FDRes_PE
dc.typeinfo:eu-repo/semantics/article
Files
Collections
Artículos - Ciencias de la Computación