Culling predicates for the Verification of Real-Time Models

Cite This

Files in this item

Checksum: MD5:a73fb21db16c6289e0c3fae430437ece

BADBAN, Bahareh, 2008. Culling predicates for the Verification of Real-Time Models

@techreport{Badban2008Culli-6239, series={Technical Report, Chair for Software Engineering, University of Konstanz}, title={Culling predicates for the Verification of Real-Time Models}, year={2008}, number={soft-08-06}, author={Badban, Bahareh} }

<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/rdf/resource/123456789/6239"> <dc:rights>terms-of-use</dc:rights> <dcterms:issued>2008</dcterms:issued> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:format>application/pdf</dc:format> <dc:language>eng</dc:language> <dc:creator>Badban, Bahareh</dc:creator> <dcterms:title>Culling predicates for the Verification of Real-Time Models</dcterms:title> <dc:contributor>Badban, Bahareh</dc:contributor> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6239/1/soft_08_06.pdf"/> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:26Z</dcterms:available> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6239"/> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6239/1/soft_08_06.pdf"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:10:26Z</dc:date> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dcterms:abstract xml:lang="eng">We present an algorithm that generates invariants for real-time models. The algorithm, further, prunes the model by first detecting, and then removing idle discrete transitions (transitions which can never be traversed). We next demonstrate how the generated invariants can be used to create a finite-state abstraction for the original model. To this end, we enhance the idea of predicate abstraction through fully incorporating locations of the concrete timed automata model in the abstraction phase.</dcterms:abstract> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> </rdf:Description> </rdf:RDF>

Downloads since Oct 1, 2014 (Information about access statistics)

soft_08_06.pdf 143

This item appears in the following Collection(s)

Search KOPS


Browse

My Account