Culling predicates for the Verification of Real-Time Models
- Startseite
- →
- Informatik und Informationswissenschaft
- →
- Informatik und Informationswissenschaft
- →
- Dokumentanzeige
| Publikationstyp: | Working Paper/Technical Report |
| URI (zitierfähiger Link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-opus-118458 |
| Autor/innen: | Badban, Bahareh |
| Erscheinungsjahr: | 2008 |
| Schriftenreihe: | Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-06 |
| Zusammenfassung: |
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.
|
| Fachgebiet (DDC): | 004 Informatik |
| Link zur Lizenz: | Nutzungsbedingungen |
Zitieren
Dateien zu dieser Ressource
![[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:rights rdf:resource="https://kops.uni-konstanz.de/page/termsofuse"/> <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> </rdf:Description> </rdf:RDF>
Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)
| soft_08_06.pdf | 92 |
Das Dokument erscheint in:
KOPS Suche
Stöbern
Mein Benutzerkonto
