Publikation: Automated Invariant Generation for the Verification of Real-Time Systems
Lade...
Dateien
Datum
2009
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
Open Access Green
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK. 2009
Zusammenfassung
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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
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. 2009BibTex
@inproceedings{Badban2009Autom-6283,
year={2009},
title={Automated Invariant Generation for the Verification of Real-Time Systems},
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: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/6283">
<dc:contributor>Smaus, Jan-Georg</dc:contributor>
<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"/>
<dcterms:issued>2009</dcterms:issued>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/6283"/>
<dc:creator>Badban, Bahareh</dc:creator>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:11:09Z</dcterms:available>
<dc:contributor>Badban, Bahareh</dc:contributor>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<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"/>
<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>terms-of-use</dc:rights>
<dc:creator>Smaus, Jan-Georg</dc:creator>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T16:11:09Z</dc:date>
<dc:format>application/pdf</dc:format>
<dc:language>eng</dc:language>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dcterms:title>Automated Invariant Generation for the Verification of Real-Time Systems</dcterms:title>
<dc:creator>Leue, Stefan</dc:creator>
<dc:contributor>Leue, Stefan</dc:contributor>
<dcterms:bibliographicCitation>Paper for: 2nd International Workshop on Invariant Generation (WING), 2009, University of York, UK</dcterms:bibliographicCitation>
</rdf:Description>
</rdf:RDF>Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
