TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Practical Partial Order Reduction for CSP

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoNasa Formal Methods
Alaotsikko7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
KustantajaSpringer International Publishing
Sivut188-203
Sivumäärä16
Vuosikerta9058
ISBN (elektroninen)978-3-319-17524-9
ISBN (painettu)978-3-319-17523-2
DOI - pysyväislinkit
TilaJulkaistu - 2015
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisussa
TapahtumaNASA Formal Methods Symposium - , Yhdysvallat
Kesto: 6 huhtikuuta 2009 → …

Julkaisusarja

NimiLecture Notes in Computer Science
Vuosikerta9058

Conference

ConferenceNASA Formal Methods Symposium
MaaYhdysvallat
Ajanjakso6/04/09 → …

Tiivistelmä

FDR is an explicit-state refinement checker for the process algebra CSP and, as such, is vulnerable to the state-explosion problem. In this paper, we show how a form of partial-order reduction, an automatic state reduction mechanism, can be utilised to soundly reduce the number of states that must be visited. In particular, we develop a compositional method for partial-order reduction that takes advantage of FDR’s internal, compositional, process representation. Further, we develop novel methods of preserving the traces of a process which allow partial-order reduction to be applied to arbitrary FDR refinement checks. We also provide details on how to efficiently implement the algorithms required for partial-order reduction.

Julkaisufoorumi-taso

Tilastokeskuksen tieteenalat