Tampere University of Technology

TUTCRIS Research Portal

Stop It, and Be Stubborn!

Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

Details

Original languageEnglish
Title of host publicationApplication of Concurrency to System Design (ACSD)
Subtitle of host publication2015 15th International Conference on
EditorsStefan Haar, Roland Meyer
PublisherIEEE Computer Society
Pages10-19
Number of pages10
ISBN (Electronic)978-1-4673-7882-6
DOIs
Publication statusPublished - 21 Jun 2015
Publication typeA4 Article in a conference publication
EventApplication of Concurrency to System Design -
Duration: 1 Jan 1900 → …

Conference

ConferenceApplication of Concurrency to System Design
Period1/01/00 → …

Abstract

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

Keywords

  • model checking; stubborn set / partial order methods; safety; progress

Publication forum classification

Field of science, Statistics Finland

Downloads statistics

No data available