TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Stop It, and Be Stubborn!

Tutkimustuotosvertaisarvioitu

Yksityiskohdat

AlkuperäiskieliEnglanti
OtsikkoApplication of Concurrency to System Design (ACSD)
Alaotsikko2015 15th International Conference on
ToimittajatStefan Haar, Roland Meyer
KustantajaIEEE Computer Society
Sivut10-19
Sivumäärä10
ISBN (elektroninen)978-1-4673-7882-6
DOI - pysyväislinkit
TilaJulkaistu - 21 kesäkuuta 2015
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisussa
TapahtumaAPPLICATION OF CONCURRENCY TO SYSTEM DESIGN -
Kesto: 1 tammikuuta 1900 → …

Conference

ConferenceAPPLICATION OF CONCURRENCY TO SYSTEM DESIGN
Ajanjakso1/01/00 → …

Tiivistelmä

A system is always may-terminating, if and only if from every reachable state, a terminal state is reachable. This publication argues that it is beneficial for both catching non-progress errors and stubborn, ample, and persistent set state space reduction to try to make verification models always may-terminating. An incorrect mutual exclusion algorithm is used as an example. The error does not manifest itself, unless the first action of the customers is modelled differently from other actions. An appropriate method is to add an alternative first action that models the customer stopping for good. This method typically makes the model always may-terminating. If the model is always may-terminating, then the basic strong stubborn set method preserves safety and some progress properties without any additional condition for solving the ignoring problem. Furthermore, whether the model is always may-terminating can be checked efficiently from the reduced state space.

!!ASJC Scopus subject areas

Tutkimusalat

Julkaisufoorumi-taso

Latausten tilastot

Ei tietoja saatavilla