Tampere University of Technology

TUTCRIS Research Portal

Fair testing and stubborn sets

Research output: Contribution to journalArticleScientificpeer-review

Details

Original languageEnglish
Pages (from-to)589-610
Number of pages22
JournalInternational Journal on Software Tools for Technology Transfer
Early online date11 Dec 2017
DOIs
Publication statusPublished - 2018
Publication typeA1 Journal article-refereed

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.

ASJC Scopus subject areas

Keywords

  • Fair testing equivalence, Fairness, Partial order methods, Progress, Stubborn sets

Publication forum classification

Field of science, Statistics Finland