TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Fair testing and stubborn sets

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

AlkuperäiskieliEnglanti
Sivut589-610
Sivumäärä22
JulkaisuInternational Journal on Software Tools for Technology Transfer
Varhainen verkossa julkaisun päivämäärä11 joulukuuta 2017
DOI - pysyväislinkit
TilaJulkaistu - 2018
OKM-julkaisutyyppiA1 Alkuperäisartikkeli

Tiivistelmä

Partial order methods alleviate state explosion by considering only a subset of actions in each constructed state. The choice of the subset depends on the properties that the method promises to preserve. Many methods have been developed ranging from deadlock-preserving to CTL(Formula presented.)-preserving and divergence-sensitive branching bisimilarity preserving. The less the method preserves, the smaller state spaces it constructs. Fair testing equivalence unifies deadlocks with livelocks that cannot be exited and ignores the other livelocks. It is the weakest congruence that preserves whether or not the system may enter a livelock that it cannot leave. We prove that a method that was designed for trace equivalence also preserves fair testing equivalence. We demonstrate its effectiveness on a protocol with a connection and data transfer phase. This is the first practical partial order method that deals with a practical fairness assumption.

!!ASJC Scopus subject areas

Tutkimusalat

Julkaisufoorumi-taso