Simulink Design Verifier vs. SPIN : a comparative case study

Vorschaubild
Dateien
Leitner-Fischer_212922.pdf
Leitner-Fischer_212922.pdfGröße: 103.73 KBDownloads: 580
Datum
2008
Autor:innen
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
http://nbn-resolving.de/urn:nbn:de:bsz:352-212922
DOI (zitierfähiger Link)
ArXiv-ID
Internationale Patentnummer
Link zur Lizenz
Urheberrechtlich geschützt
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Sammlungen
Informatik und Informationswissenschaft
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Publikationstyp
Sonstiges, textgebunden (z.B. Gutachten, Blogbeiträge)
Publikationsstatus
Published
Erschienen in
Zusammenfassung

An increasing number of industrial strength software design tools come along with veri cation tools that o er some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Veri er and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
Rezension
undefined / . - undefined, undefined
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Datensätze
Zitieren
ISO 690LEITNER-FISCHER, Florian, Stefan LEUE, 2008. Simulink Design Verifier vs. SPIN : a comparative case study
BibTex
@misc{LeitnerFischer2008Simul-21292,
  year={2008},
  title={Simulink Design Verifier vs. SPIN : a comparative case study},
  author={Leitner-Fischer, Florian and Leue, Stefan},
  note={„Paper presented at FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems“}
}
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/21292">
    <dcterms:issued>2008</dcterms:issued>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21292"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-12T13:22:32Z</dc:date>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dc:language>eng</dc:language>
    <dcterms:abstract xml:lang="eng">An increasing number of industrial strength software design tools come along with veri cation tools that o er some property checking capabilities. On the other hand, there is a large number of general purpose model checking tools available. The question whether users of the industrial strength design tool preferably use the built-in state space exploration tool or a general purpose model checking tool arises quite naturally. Using the case study of an AUTOSAR compliant memory management module we compare the Simulink Design Veri er and the SPIN model checking tool in terms of their suitability to verify important correctness properties of this module. The comparison is both functional in that it analyzes the suitability to verify a set of basic system properties, and quantitative in comparing the computational efficiency of both tools.</dcterms:abstract>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-03-12T13:22:32Z</dcterms:available>
    <dc:rights>terms-of-use</dc:rights>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21292/1/Leitner-Fischer_212922.pdf"/>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21292/1/Leitner-Fischer_212922.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:title>Simulink Design Verifier vs. SPIN : a comparative case study</dcterms:title>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
  </rdf:Description>
</rdf:RDF>
Interner Vermerk
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Kontakt
URL der Originalveröffentl.
Prüfdatum der URL
Prüfungsdatum der Dissertation
Finanzierungsart
Kommentar zur Publikation
„Paper presented at FMICS 2008, ERCIM Working Group on Formal Methods for Industrial Critical Systems“
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen