CISPA
Browse
cispa_all_3819.pdf (456.42 kB)

Automatic Repair and Deadlock Detection for Parameterized Systems

Download (456.42 kB)
conference contribution
posted on 2023-11-29, 18:23 authored by Swen JacobsSwen Jacobs, Mouhammad Sakr, Marcus Völp
We present an algorithm for the repair of parameterized 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. We apply this algorithm on systems that can be represented as well-structured transition systems (WSTS), including disjunctive systems, pairwise rendezvous systems, and broadcast protocols. Moreover, we show that parameterized deadlock detection can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols.

History

Preferred Citation

Swen Jacobs, Mouhammad Sakr and Marcus Völp. Automatic Repair and Deadlock Detection for Parameterized Systems. In: Formal Methods in Computer-Aided Design (FMCAD). 2022.

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

Formal Methods in Computer-Aided Design (FMCAD)

Legacy Posted Date

2022-10-13

Open Access Type

  • Green

BibTeX

@inproceedings{cispa_all_3819, title = "Automatic Repair and Deadlock Detection for Parameterized Systems", author = "Jacobs, Swen and Sakr, Mouhammad and Völp, Marcus", booktitle="{Formal Methods in Computer-Aided Design (FMCAD)}", year="2022", }

Usage metrics

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC