Counterexample Refinement for a Boundedness Test for CFSM Languages

Leue, Stefan; Wei, Wei

Counterexample Refinement for a Boundedness Test for CFSM Languages

Files

Counterexample_Refinement_for_a_Boundedness_Test_for_CFSM_Languages.pdf(210.29 KB)

Date

2005

Authors

Leue, Stefan

Wei, Wei

Series

Technical Report, Chair for Software Engineering, University of Konstanz; soft-05-01

Publication type

Working Paper/Technical Report

Abstract

In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive counterexamples when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples.

Subject (DDC)

004 Computer Science

Cite This

ISO 690

LEUE, Stefan, Wei WEI, 2005. Counterexample Refinement for a Boundedness Test for CFSM Languages

BibTex

@techreport{Leue2005Count-5616,
  year={2005},
  series={Technical Report, Chair for Software Engineering, University of Konstanz},
  title={Counterexample Refinement for a Boundedness Test for CFSM Languages},
  number={soft-05-01},
  author={Leue, Stefan and Wei, Wei}
}

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/5616">
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5616/1/Counterexample_Refinement_for_a_Boundedness_Test_for_CFSM_Languages.pdf"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5616"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:language>eng</dc:language>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:contributor>Wei, Wei</dc:contributor>
    <dc:rights>terms-of-use</dc:rights>
    <dc:format>application/pdf</dc:format>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5616/1/Counterexample_Refinement_for_a_Boundedness_Test_for_CFSM_Languages.pdf"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:57:13Z</dcterms:available>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:57:13Z</dc:date>
    <dcterms:title>Counterexample Refinement for a Boundedness Test for CFSM Languages</dcterms:title>
    <dcterms:abstract xml:lang="eng">In precursory work we suggested an abstraction-based highly scalable semi-test for the boundedness of Communicating Finite State Machine (CFSM) based modelling and programming languages. We illustrated its application to Promela and UML-RT models. The test is sound with respect to determining boundedness, but may return inconclusive  counterexamples  when boundedness cannot be established. In this paper we turn to the question how to effectively determine the spuriousness of these counterexamples, and how to refine the abstraction based on the analysis. We employ methods from program analysis and illustrate the application of our refinement method to a number of Promela examples.</dcterms:abstract>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:creator>Wei, Wei</dc:creator>
    <dcterms:issued>2005</dcterms:issued>
  </rdf:Description>
</rdf:RDF>

Bibliography of Konstanz

Yes