An Innovative Heuristic to Detect Special States in Concurrent Software Systems.

Saved in:
Bibliographic Details
Title: An Innovative Heuristic to Detect Special States in Concurrent Software Systems.
Authors: Pira, Einollah1 (AUTHOR) pira@azaruniv.ac.ir, Rouhi, Alireza1 (AUTHOR)
Source: Quality & Reliability Engineering International. Dec2025, Vol. 41 Issue 8, p3686-3697. 12p.
Subjects: Heuristic, Verification of computer systems, Software development tools, Computer performance, State-space methods, Software validation, Parallel programs (Computer programs)
Abstract: Model checking is a formal verification technique used to verify whether a model of a given concurrent software system will meet some special states such as reachability (so‐called goal) ones, in the future. Although useful, this heuristic cannot be a suitable way in large models of given systems due to the high time of finding the similarity amount. In this paper, we present a rule‐based heuristic that uses the erase/addition of components by the rules to obtain the interdependence of rules. After acquiring these interdependences, they are employed to explore the state space efficiently. To validate the efficiency of the presented heuristic, it is applied on the concurrent software systems specified through graph transformation language, and implemented in GROOVE, an open‐source toolset for designing and model checking graph transformation systems. Experimental results show that the presented heuristic outperforms the existing algorithms in terms of running time, the number of exploration states, and the length of generated witnesses. [ABSTRACT FROM AUTHOR]
Copyright of Quality & Reliability Engineering International is the property of Wiley-Blackwell 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: 189330178
AccessLevel: 6
PubType: Academic Journal
PubTypeId: academicJournal
PreciseRelevancyScore: 0
IllustrationInfo
Items – Name: Title
  Label: Title
  Group: Ti
  Data: An Innovative Heuristic to Detect Special States in Concurrent Software Systems.
– Name: Author
  Label: Authors
  Group: Au
  Data: <searchLink fieldCode="AR" term="%22Pira%2C+Einollah%22">Pira, Einollah</searchLink><relatesTo>1</relatesTo> (AUTHOR)<i> pira@azaruniv.ac.ir</i><br /><searchLink fieldCode="AR" term="%22Rouhi%2C+Alireza%22">Rouhi, Alireza</searchLink><relatesTo>1</relatesTo> (AUTHOR)
– Name: TitleSource
  Label: Source
  Group: Src
  Data: <searchLink fieldCode="JN" term="%22Quality+%26+Reliability+Engineering+International%22">Quality & Reliability Engineering International</searchLink>. Dec2025, Vol. 41 Issue 8, p3686-3697. 12p.
– Name: Subject
  Label: Subjects
  Group: Su
  Data: <searchLink fieldCode="DE" term="%22Heuristic%22">Heuristic</searchLink><br /><searchLink fieldCode="DE" term="%22Verification+of+computer+systems%22">Verification of computer systems</searchLink><br /><searchLink fieldCode="DE" term="%22Software+development+tools%22">Software development tools</searchLink><br /><searchLink fieldCode="DE" term="%22Computer+performance%22">Computer performance</searchLink><br /><searchLink fieldCode="DE" term="%22State-space+methods%22">State-space methods</searchLink><br /><searchLink fieldCode="DE" term="%22Software+validation%22">Software validation</searchLink><br /><searchLink fieldCode="DE" term="%22Parallel+programs+%28Computer+programs%29%22">Parallel programs (Computer programs)</searchLink>
– Name: Abstract
  Label: Abstract
  Group: Ab
  Data: Model checking is a formal verification technique used to verify whether a model of a given concurrent software system will meet some special states such as reachability (so‐called goal) ones, in the future. Although useful, this heuristic cannot be a suitable way in large models of given systems due to the high time of finding the similarity amount. In this paper, we present a rule‐based heuristic that uses the erase/addition of components by the rules to obtain the interdependence of rules. After acquiring these interdependences, they are employed to explore the state space efficiently. To validate the efficiency of the presented heuristic, it is applied on the concurrent software systems specified through graph transformation language, and implemented in GROOVE, an open‐source toolset for designing and model checking graph transformation systems. Experimental results show that the presented heuristic outperforms the existing algorithms in terms of running time, the number of exploration states, and the length of generated witnesses. [ABSTRACT FROM AUTHOR]
– Name: AbstractSuppliedCopyright
  Label:
  Group: Ab
  Data: <i>Copyright of Quality & Reliability Engineering International is the property of Wiley-Blackwell 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=189330178
RecordInfo BibRecord:
  BibEntity:
    Identifiers:
      – Type: doi
        Value: 10.1002/qre.70052
    Languages:
      – Code: eng
        Text: English
    PhysicalDescription:
      Pagination:
        PageCount: 12
        StartPage: 3686
    Subjects:
      – SubjectFull: Heuristic
        Type: general
      – SubjectFull: Verification of computer systems
        Type: general
      – SubjectFull: Software development tools
        Type: general
      – SubjectFull: Computer performance
        Type: general
      – SubjectFull: State-space methods
        Type: general
      – SubjectFull: Software validation
        Type: general
      – SubjectFull: Parallel programs (Computer programs)
        Type: general
    Titles:
      – TitleFull: An Innovative Heuristic to Detect Special States in Concurrent Software Systems.
        Type: main
  BibRelationships:
    HasContributorRelationships:
      – PersonEntity:
          Name:
            NameFull: Pira, Einollah
      – PersonEntity:
          Name:
            NameFull: Rouhi, Alireza
    IsPartOfRelationships:
      – BibEntity:
          Dates:
            – D: 01
              M: 12
              Text: Dec2025
              Type: published
              Y: 2025
          Identifiers:
            – Type: issn-print
              Value: 07488017
          Numbering:
            – Type: volume
              Value: 41
            – Type: issue
              Value: 8
          Titles:
            – TitleFull: Quality & Reliability Engineering International
              Type: main
ResultId 1