Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN

Loading...
Thumbnail Image
Date
2008
Editors
Contact
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-05
URI (citable link)
DOI (citable link)
ArXiv-ID
International patent number
Link to the license
EU project number
Project
Open Access publication
Restricted until
Title in another language
Research Projects
Organizational Units
Journal Issue
Publication type
Working Paper/Technical Report
Publication status
Published in
Abstract
An increasing number of industrial strength software design tools come along with verification 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 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.
Summary in another language
Subject (DDC)
004 Computer Science
Keywords
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
ISO 690LEITNER-FISCHER, Florian, 2008. Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN
BibTex
@techreport{LeitnerFischer2008Evalu-21293,
  year={2008},
  series={Technical Report, Chair for Software Engineering, University of Konstanz ; soft-08-05},
  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/21293">
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:abstract xml:lang="eng">An increasing number of industrial strength software design tools come along with verification 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 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>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2008</dcterms:issued>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21293/1/Leitner_212939.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-01-30T09:58:44Z</dc:date>
    <dcterms:title>Evaluation of the Matlab Simulink Design Verifier versus the model checker SPIN</dcterms:title>
    <dc:creator>Leitner-Fischer, Florian</dc:creator>
    <dc:language>eng</dc:language>
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/21293"/>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/21293/1/Leitner_212939.pdf"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2013-01-30T09:58:44Z</dcterms:available>
    <dc:contributor>Leitner-Fischer, Florian</dc:contributor>
  </rdf:Description>
</rdf:RDF>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Contact
URL of original publication
Test date of URL
Examination date of dissertation
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
No
Refereed