Heuristic Search for Unbounded Executions

Thumbnail Image
Files
atva09_submission_25.pdf(215.68 KB)
Date
2009
Authors
Yang, Sen
Editors
Contact
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
URI (citable link)
urn:nbn:de:bsz:352-opus-103118
DOI (citable link)
ArXiv-ID
International patent number
Link to the license
In Copyright
EU project number
Project
Open Access publication
Collections
Informatik und Informationswissenschaft
Restricted until
Title in another language
Research Projects
Organizational Units
Journal Issue
Publication type
Working Paper/Technical Report
Publication status
Published in
Abstract
We present a heuristic search based approach to finding un- bounded executions in software models that can be described using Com- municating Finite State Machines (CFSMs). This improves the unbound- edness test devised by Jeron and Jard in case certain knowledge about potential sources of unboundedness is available. Such knowledge can be obtained from a boundedness analysis that we designed in precursory work. We evaluate the effectiveness of several different heuristics and search strategies. To show the feasibility of our approach, we compare the performance of the heuristic search algorithms with that of uninformed search algorithms in detecting unbounded executions for a number of case studies. We discuss the applicability of our approach to high level modeling languages for concurrent systems such as Promela.
Summary in another language
Subject (DDC)
004 Computer Science
Keywords
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690KUNTZ, Matthias, Stefan LEUE, Christoph SCHEBEN, Wei WEI, Sen YANG, 2009. Heuristic Search for Unbounded Executions
BibTex
@techreport{Kuntz2009Heuri-6228,
  year={2009},
  title={Heuristic Search for Unbounded Executions},
  author={Kuntz, Matthias and Leue, Stefan and Scheben, Christoph and Wei, Wei and Yang, Sen}
}
RDF
<rdf:RDF
    xmlns:dcterms="http://purl.org/dc/terms/"
    xmlns:dc="http://purl.org/dc/elements/1.1/"
    xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
    xmlns:bibo="http://purl.org/ontology/bibo/"
    xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
    xmlns:foaf="http://xmlns.com/foaf/0.1/"
    xmlns:void="http://rdfs.org/ns/void#"
    xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > 
  <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/6228">
    <dc:creator>Scheben, Christoph</dc:creator>
    <dc:contributor>Wei, Wei</dc:contributor>
    <dc:language>eng</dc:language>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:contributor>Kuntz, Matthias</dc:contributor>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Scheben, Christoph</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:23Z</dc:date>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:23Z</dcterms:available>
    <dcterms:title>Heuristic Search for Unbounded Executions</dcterms:title>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:rights>terms-of-use</dc:rights>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6228"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:creator>Wei, Wei</dc:creator>
    <dc:format>application/pdf</dc:format>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6228/1/atva09_submission_25.pdf"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6228/1/atva09_submission_25.pdf"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Yang, Sen</dc:contributor>
    <dcterms:issued>2009</dcterms:issued>
    <dc:creator>Yang, Sen</dc:creator>
    <dc:creator>Kuntz, Matthias</dc:creator>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:abstract xml:lang="eng">We present a heuristic search based approach to finding un- bounded executions in software models that can be described using Com- municating Finite State Machines (CFSMs). This improves the unbound- edness test devised by Jeron and Jard in case certain knowledge about potential sources of unboundedness is available. Such knowledge can be obtained from a boundedness analysis that we designed in precursory work. We evaluate the effectiveness of several different heuristics and search strategies. To show the feasibility of our approach, we compare the performance of the heuristic search algorithms with that of uninformed search algorithms in detecting unbounded executions for a number of case studies. We discuss the applicability of our approach to high level modeling languages for concurrent systems such as Promela.</dcterms:abstract>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </rdf:Description>
</rdf:RDF>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Contact
URL of original publication
Test date of URL
Examination date of dissertation
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
Yes
Refereed