Culling predicates for the Verification of Real-Time Models
| Type of Publication: | Working Paper/Technical Report |
| URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-118458 |
| Author: | Badban, Bahareh |
| Year of publication: | 2008 |
| Series: | Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-06 |
| Summary: |
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.
|
| Subject (DDC): | 004 Computer Science |
| Link to License: | In Copyright |
Cite This
Files in this item
![[PDF]](/themes/Kops/images/mimes/pdf.png "PDF file"){kind=small}
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
