TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Fair testing and stubborn sets

Tutkimustuotosvertaisarvioitu

Standard

Fair testing and stubborn sets. / Valmari, Antti; Vogler, Walter.

julkaisussa: International Journal on Software Tools for Technology Transfer, 2018, s. 589-610.

Tutkimustuotosvertaisarvioitu

Harvard

Valmari, A & Vogler, W 2018, 'Fair testing and stubborn sets', International Journal on Software Tools for Technology Transfer, Sivut 589-610. https://doi.org/10.1007/s10009-017-0481-2

APA

Valmari, A., & Vogler, W. (2018). Fair testing and stubborn sets. International Journal on Software Tools for Technology Transfer, 589-610. https://doi.org/10.1007/s10009-017-0481-2

Vancouver

Valmari A, Vogler W. Fair testing and stubborn sets. International Journal on Software Tools for Technology Transfer. 2018;589-610. https://doi.org/10.1007/s10009-017-0481-2

Author

Valmari, Antti ; Vogler, Walter. / Fair testing and stubborn sets. Julkaisussa: International Journal on Software Tools for Technology Transfer. 2018 ; Sivut 589-610.

Bibtex - Lataa

@article{c6d1de6acaf84c2f909171333b7ba847,
title = "Fair testing and stubborn sets",
abstract = "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.",
keywords = "Fair testing equivalence, Fairness, Partial order methods, Progress, Stubborn sets",
author = "Antti Valmari and Walter Vogler",
year = "2018",
doi = "10.1007/s10009-017-0481-2",
language = "English",
pages = "589--610",
journal = "International Journal on Software Tools for Technology Transfer",
issn = "1433-2779",
publisher = "Springer Verlag",

}

RIS (suitable for import to EndNote) - Lataa

TY - JOUR

T1 - Fair testing and stubborn sets

AU - Valmari, Antti

AU - Vogler, Walter

PY - 2018

Y1 - 2018

N2 - 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.

AB - 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.

KW - Fair testing equivalence

KW - Fairness

KW - Partial order methods

KW - Progress

KW - Stubborn sets

U2 - 10.1007/s10009-017-0481-2

DO - 10.1007/s10009-017-0481-2

M3 - Article

SP - 589

EP - 610

JO - International Journal on Software Tools for Technology Transfer

JF - International Journal on Software Tools for Technology Transfer

SN - 1433-2779

ER -