Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN
Dateien
Datum
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
Sammlungen
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
An increasing number of industrial strength software design tools come along with verification tools that offer 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 verification tool or a general purpose model checking tool arises quite naturally. In this bachelor thesis, the Simulink Design Verifier and the SPIN model checking tool are compared. The comparison is based on the case study of an AUTOSAR compliant memory management 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. In this context, it is also described how Simulink / Stateflow models can be manually translated into the input language of the model checker SPIN.
Zusammenfassung in einer weiteren Sprache
Eine steigende Anzahl von industriell eingesetzten Software Design Werkzeugen, bietet Möglichkeiten "Korrektheitseigenschaften" zu verifizieren. Andererseits, gibt es eine große Anzahl an allgemeinen Model Checking Werkzeugen. Natürlich stellt sich nun die Frage, ob der Benutzer eines industriellen Software Design Werkzeuges nun das eingebaute Verifizierungs-Werkzeug benutzen sollte, oder ob er eines der allgemeinen Model Checking Werkzeuge bevorzugen sollte. In dieser Bachelorarbeit wird der Simulink Design Verifier mit dem model checking Werkzeug SPIN verglichen. Dem Vergleich liegt die Fallstudie eines AUTOSAR kompatiblen Speicherverwaltungs-Modul zu Grunde. Der Vergleich ist sowohl funktional, da analysiert wird, inwieweit sich die Werkzeuge dazu eignen eine ausgewählte Menge an "Korrektheitseigenschaften" zu verifizieren, als auch quantitativ da die Effizienz der beiden Werkzeuge verglichen wird. Im Zusammenhang wird auch beschrieben, wie Simulink / Stateflow Modelle manuell in die Eingabesprache des Model Checker SPIN übersetzt werden können.
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
LEITNER-FISCHER, Florian, 2008. Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN [Bachelor thesis]BibTex
@mastersthesis{LeitnerFischer2008Evalu-5603,
year={2008},
title={Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN},
author={Leitner-Fischer, Florian}
}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/5603">
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:43Z</dc:date>
<dc:contributor>Leitner-Fischer, Florian</dc:contributor>
<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/5603/1/Leitner_Evaluation_of_the_Matlab_Simulink_Design_Verifier_versus_the_model_checker_SPIN.pdf"/>
<dc:creator>Leitner-Fischer, Florian</dc:creator>
<dcterms:abstract xml:lang="eng">An increasing number of industrial strength software design tools come along with verification tools that offer 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 verification tool or a general purpose model checking tool arises quite naturally. In this bachelor thesis, the Simulink Design Verifier and the SPIN model checking tool are compared. The comparison is based on the case study of an AUTOSAR compliant memory management 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. In this context, it is also described how Simulink / Stateflow models can be manually translated into the input language of the model checker SPIN.</dcterms:abstract>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5603"/>
<dcterms:title>Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN</dcterms:title>
<dc:language>eng</dc:language>
<dc:format>application/pdf</dc:format>
<dcterms:issued>2008</dcterms:issued>
<dc:rights>terms-of-use</dc:rights>
<dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5603/1/Leitner_Evaluation_of_the_Matlab_Simulink_Design_Verifier_versus_the_model_checker_SPIN.pdf"/>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:43Z</dcterms:available>
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
</rdf:Description>
</rdf:RDF>
