Automated Invariant Generation for the Verification of Real-Time Systems

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:0f0d5e06adb4602987a51c87aff5b28f

BADBAN, Bahareh, Stefan LEUE, Jan-Georg SMAUS, 2009. Automated Invariant Generation for the Verification of Real-Time Systems. 2nd International Workshop on Invariant Generation (WING). University of York, UK, 2009. In: 2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK. 2nd International Workshop on Invariant Generation (WING). University of York, UK, 2009

@inproceedings{Badban2009Autom-6283, title={Automated Invariant Generation for the Verification of Real-Time Systems}, year={2009}, booktitle={2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK}, author={Badban, Bahareh and Leue, Stefan and Smaus, Jan-Georg} }

<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/6283"> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:rights rdf:resource="http://nbn-resolving.org/urn:nbn:de:bsz:352-20140905103416863-3868037-7"/> <dc:creator>Badban, Bahareh</dc:creator> <dcterms:issued>2009</dcterms:issued> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6283/1/Automated_Invariant_Generation_for_the_Verification_of_Real_Time_Systems_2009_KOPS10601.pdf"/> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:11:09Z</dc:date> <dc:format>application/pdf</dc:format> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/6283/1/Automated_Invariant_Generation_for_the_Verification_of_Real_Time_Systems_2009_KOPS10601.pdf"/> <dc:contributor>Badban, Bahareh</dc:contributor> <dcterms:abstract xml:lang="eng">We present a technique designed to automatically compute predicate abstractions for dense real-timed models represented as networks of timed automata. We first introduce the CIPM algorithm which computes new invariants for timed automata control locations taking their originally defined invariants as well as the constraints imposed by incoming state transitions into account. CIPM also prunes transitions that can never be taken from the automaton. We then compute a predicate abstraction taking information regarding control locations and their newly computed invariants into account. We finally discuss a prototype implementation of our technique.</dcterms:abstract> <dc:rights>deposit-license</dc:rights> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:11:09Z</dcterms:available> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Leue, Stefan</dc:creator> <dc:language>eng</dc:language> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dcterms:bibliographicCitation>Paper for: 2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK</dcterms:bibliographicCitation> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6283"/> <dc:creator>Smaus, Jan-Georg</dc:creator> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:title>Automated Invariant Generation for the Verification of Real-Time Systems</dcterms:title> <dc:contributor>Smaus, Jan-Georg</dc:contributor> </rdf:Description> </rdf:RDF>

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Automated_Invariant_Generation_for_the_Verification_of_Real_Time_Systems_2009_KOPS10601.pdf 88

Das Dokument erscheint in:

KOPS Suche


Stöbern

Mein Benutzerkonto