View in EDS

Automatic WSTS-based repair and deadlock detection of parameterized systems.

Saved in:
Bibliographic Details
Title: Automatic WSTS-based repair and deadlock detection of parameterized systems.
Authors: Baumeister, Tom1 (AUTHOR) tom.baumeister@cispa.de, Jacobs, Swen1 (AUTHOR) jacobs@cispa.de, Sakr, Mouhammad2 (AUTHOR) mouhammad.sakr@uni.lu, Völp, Marcus2 (AUTHOR) marcus.voelp@uni.lu
Source: Formal Methods in System Design. Sep2025, Vol. 66 Issue 3, p335-375. 41p.
Subjects: Synchronization, Verification of computer systems, Constraint programming, Safety standards
Abstract: We present an algorithm for the repair of parameterized systems that can be represented as well-structured transition systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule out candidates. Parameterized systems that fall into our class include disjunctive systems, pairwise rendezvous systems, broadcast protocols, and certain global synchronization protocols. Moreover, we show that parameterized deadlock detection and similar global properties can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols. [ABSTRACT FROM AUTHOR]
Copyright of Formal Methods in System Design is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)
Database: Engineering Source
Description
Abstract:We present an algorithm for the repair of parameterized systems that can be represented as well-structured transition systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule out candidates. Parameterized systems that fall into our class include disjunctive systems, pairwise rendezvous systems, broadcast protocols, and certain global synchronization protocols. Moreover, we show that parameterized deadlock detection and similar global properties can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols. [ABSTRACT FROM AUTHOR]
ISSN:09259856
DOI:10.1007/s10703-025-00469-2