Counterexample Refinement for a Boundedness Test for CFSM Languages
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Sammlungen
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
LEUE, Stefan, Wei WEI, 2005. Counterexample Refinement for a Boundedness Test for CFSM LanguagesBibTex
@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>