File Download
  Links for fulltext
     (May Require Subscription)
Supplementary

Article: An enhanced flow analysis technique for detecting unreachability faults in concurrent systems

TitleAn enhanced flow analysis technique for detecting unreachability faults in concurrent systems
Authors
KeywordsConcurrency
Distributed systems
Reachability analysis
Static analysis
Issue Date2012
PublisherElsevier Inc. The Journal's web site is located at http://www.elsevier.com/locate/ins
Citation
Information Sciences, 2012, v. 194, p. 254-269 How to Cite?
AbstractWe present a flow analysis technique for detecting unreachable states and actions in concurrent systems. It is an enhancement of the approach by Cheung and Kramer. Each process of a concurrent system is modeled as a finite state machine, whose states represent process execution states and whose transitions are labeled by actions. We construct dependency sets incrementally and eliminate spurious paths by checking the execution sequences of actions. We prove mathematically that our algorithm can detect more unreachability faults than the well-known Reif/Smolka and Cheung/Kramer algorithms. The algorithm is easy to manage and its complexity is still polynomial to the system size. Case studies on two commonly used communication protocols show that the technique is effective. © 2012 Elsevier Inc. All rights reserved.
Persistent Identifierhttp://hdl.handle.net/10722/144724
ISSN
2015 Impact Factor: 3.364
2015 SCImago Journal Rankings: 2.513
ISI Accession Number ID
Funding AgencyGrant Number
Australian Research Council
Research Grants Council of Hong Kong717308
Funding Information:

This research is supported in part by a grant of the Australian Research Council and a grant of the Research Grants Council of Hong Kong (Project No. 717308).

References

 

DC FieldValueLanguage
dc.contributor.authorChen, TYen_HK
dc.contributor.authorHu, Pen_HK
dc.contributor.authorLi, Hen_HK
dc.contributor.authorTse, THen_HK
dc.date.accessioned2012-02-03T06:19:49Z-
dc.date.available2012-02-03T06:19:49Z-
dc.date.issued2012en_HK
dc.identifier.citationInformation Sciences, 2012, v. 194, p. 254-269en_HK
dc.identifier.issn0020-0255en_HK
dc.identifier.urihttp://hdl.handle.net/10722/144724-
dc.description.abstractWe present a flow analysis technique for detecting unreachable states and actions in concurrent systems. It is an enhancement of the approach by Cheung and Kramer. Each process of a concurrent system is modeled as a finite state machine, whose states represent process execution states and whose transitions are labeled by actions. We construct dependency sets incrementally and eliminate spurious paths by checking the execution sequences of actions. We prove mathematically that our algorithm can detect more unreachability faults than the well-known Reif/Smolka and Cheung/Kramer algorithms. The algorithm is easy to manage and its complexity is still polynomial to the system size. Case studies on two commonly used communication protocols show that the technique is effective. © 2012 Elsevier Inc. All rights reserved.en_HK
dc.languageengen_US
dc.publisherElsevier Inc. The Journal's web site is located at http://www.elsevier.com/locate/insen_HK
dc.relation.ispartofInformation Sciencesen_HK
dc.rightsNOTICE: this is the author’s version of a work that was accepted for publication in <Information Sciences>. Changes resulting from the publishing process, such as peer review, editing, corrections, structural formatting, and other quality control mechanisms may not be reflected in this document. Changes may have been made to this work since it was submitted for publication. A definitive version was subsequently published in PUBLICATION, [VOL194, (2012)] DOI 10.1016/j.ins.2011.11.034]-
dc.rightsCreative Commons: Attribution 3.0 Hong Kong License-
dc.subjectConcurrencyen_HK
dc.subjectDistributed systemsen_HK
dc.subjectReachability analysisen_HK
dc.subjectStatic analysisen_HK
dc.titleAn enhanced flow analysis technique for detecting unreachability faults in concurrent systemsen_HK
dc.typeArticleen_HK
dc.identifier.emailTse, TH: thtse@cs.hku.hken_HK
dc.identifier.authorityTse, TH=rp00546en_HK
dc.description.naturepostprint-
dc.identifier.doi10.1016/j.ins.2011.11.034en_HK
dc.identifier.scopuseid_2-s2.0-84862828555en_HK
dc.identifier.hkuros199194en_US
dc.relation.referenceshttp://www.scopus.com/mlt/select.url?eid=2-s2.0-84862828555&selection=ref&src=s&origin=recordpageen_HK
dc.identifier.volume194en_HK
dc.identifier.spage254en_HK
dc.identifier.epage269en_HK
dc.identifier.eissn1872-6291-
dc.identifier.isiWOS:000303092700015-
dc.publisher.placeUnited Statesen_HK
dc.identifier.scopusauthoridChen, TY=35247605500en_HK
dc.identifier.scopusauthoridHu, P=7201989692en_HK
dc.identifier.scopusauthoridLi, H=55261726500en_HK
dc.identifier.scopusauthoridTse, TH=7005496974en_HK
dc.identifier.citeulike10165430-

Export via OAI-PMH Interface in XML Formats


OR


Export to Other Non-XML Formats