Stop It, and Be Stubborn!
Tutkimustuotos › › vertaisarvioitu
Yksityiskohdat
| Alkuperäiskieli | Englanti |
|---|---|
| Otsikko | Application of Concurrency to System Design (ACSD) |
| Alaotsikko | 2015 15th International Conference on |
| Toimittajat | Stefan Haar, Roland Meyer |
| Kustantaja | IEEE Computer Society |
| Sivut | 10-19 |
| Sivumäärä | 10 |
| ISBN (elektroninen) | 978-1-4673-7882-6 |
| DOI - pysyväislinkit | |
| Tila | Julkaistu - 21 kesäkuuta 2015 |
| OKM-julkaisutyyppi | A4 Artikkeli konferenssijulkaisussa |
| Tapahtuma | APPLICATION OF CONCURRENCY TO SYSTEM DESIGN - Kesto: 1 tammikuuta 1900 → … |
Conference
| Conference | APPLICATION OF CONCURRENCY TO SYSTEM DESIGN |
|---|---|
| Ajanjakso | 1/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
Tilastokeskuksen tieteenalat
Latausten tilastot
Ei tietoja saatavilla