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
FullText Text:
  Availability: 0
Header DbId: egs
DbLabel: Engineering Source
An: 188354583
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: Automatic WSTS-based repair and deadlock detection of parameterized systems.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Baumeister%2C+Tom%22">Baumeister, Tom</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> tom.baumeister@cispa.de</i><br /><searchLink fieldCode="AR" term="%22Jacobs%2C+Swen%22">Jacobs, Swen</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> jacobs@cispa.de</i><br /><searchLink fieldCode="AR" term="%22Sakr%2C+Mouhammad%22">Sakr, Mouhammad</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> mouhammad.sakr@uni.lu</i><br /><searchLink fieldCode="AR" term="%22Völp%2C+Marcus%22">Völp, Marcus</searchLink><relatesTo>2</relatesTo> (AUTHOR)<i> marcus.voelp@uni.lu</i>
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Formal+Methods+in+System+Design%22">Formal Methods in System Design</searchLink>. Sep2025, Vol. 66 Issue 3, p335-375. 41p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Synchronization%22">Synchronization</searchLink><br /><searchLink fieldCode="DE" term="%22Verification+of+computer+systems%22">Verification of computer systems</searchLink><br /><searchLink fieldCode="DE" term="%22Constraint+programming%22">Constraint programming</searchLink><br /><searchLink fieldCode="DE" term="%22Safety+standards%22">Safety standards</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: 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]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>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.</i> (Copyright applies to all Abstracts.)
PLink https://search.ebscohost.com/login.aspx?direct=true&site=eds-live&db=egs&AN=188354583
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1007/s10703-025-00469-2
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 41
        StartPage: 335
    Subjects:
      – SubjectFull: Synchronization
        Type: general
      – SubjectFull: Verification of computer systems
        Type: general
      – SubjectFull: Constraint programming
        Type: general
      – SubjectFull: Safety standards
        Type: general
    Titles:
      – TitleFull: Automatic WSTS-based repair and deadlock detection of parameterized systems.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Baumeister, Tom
      – PersonEntity:
          Name:
            NameFull: Jacobs, Swen
      – PersonEntity:
          Name:
            NameFull: Sakr, Mouhammad
      – PersonEntity:
          Name:
            NameFull: Völp, Marcus
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 09
              Text: Sep2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 09259856
          Numbering:
            – Type: volume
              Value: 66
            – Type: issue
              Value: 3
          Titles:
            – TitleFull: Formal Methods in System Design
              Type: main
ResultId 1