[en] 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.
Disciplines :
Computer science
Author, co-author :
Baumeister, Tom; Helmholtz Center for Information Security
Jacobs, Swen; Helmholtz Center for Information Security
SAKR, Mouhammad ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX
VÖLP, Marcus ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX
External co-authors :
yes
Language :
English
Title :
Automatic WSTS-based Repair and Deadlock Detection of Parameterized Systems
