Practical Partial Order Reduction for CSP
Tutkimustuotos › › vertaisarvioitu
Yksityiskohdat
| Alkuperäiskieli | Englanti |
|---|---|
| Otsikko | Nasa Formal Methods |
| Alaotsikko | 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings |
| Kustantaja | Springer International Publishing |
| Sivut | 188-203 |
| Sivumäärä | 16 |
| Vuosikerta | 9058 |
| ISBN (elektroninen) | 978-3-319-17524-9 |
| ISBN (painettu) | 978-3-319-17523-2 |
| DOI - pysyväislinkit | |
| Tila | Julkaistu - 2015 |
| OKM-julkaisutyyppi | A4 Artikkeli konferenssijulkaisussa |
| Tapahtuma | NASA Formal Methods Symposium - , Yhdysvallat Kesto: 6 huhtikuuta 2009 → … |
Julkaisusarja
| Nimi | Lecture Notes in Computer Science |
|---|---|
| Vuosikerta | 9058 |
Conference
| Conference | NASA Formal Methods Symposium |
|---|---|
| Maa | Yhdysvallat |
| Ajanjakso | 6/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.