Stop It, and Be Stubborn!
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
|Title of host publication||Application of Concurrency to System Design (ACSD)|
|Subtitle of host publication||2015 15th International Conference on |
|Editors||Stefan Haar, Roland Meyer|
|Publisher||IEEE Computer Society|
|Number of pages||10|
|ISBN (Electronic)||978-1-4673-7882-6 |
|Publication status||Published - 21 Jun 2015|
|Publication type||A4 Article in a conference publication|
|Event||Application of Concurrency to System Design - |
Duration: 1 Jan 1900 → …
|Conference||Application of Concurrency to System Design|
|Period||1/01/00 → …|
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.
- model checking; stubborn set / partial order methods; safety; progress