From SysML to Model Checkers via Model Transformation

Lade...
Vorschaubild
Dateien
Koelbl_2-fcxzqisum9ld1.pdf
Koelbl_2-fcxzqisum9ld1.pdfGröße: 253.44 KBDownloads: 815
Datum
2018
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
ArXiv-ID
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz
Gesperrt bis
Titel in einer weiteren Sprache
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published
Erschienen in
DEL MAR GALLARDO, María, ed., Pedro MERINO, ed.. Model Checking Software : 25th International Symposium : SPIN 2018 : proceedings. Cham: Springer, 2018, pp. 255-274. Lecture Notes in Computer Science. 10869. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-94110-3. Available under: doi: 10.1007/978-3-319-94111-0_15
Zusammenfassung

In this paper we present an automated translation from the systems engineering modeling language SysML into the input languages of the NuSMV, Prism and Spin model checkers. A special focus of this work is the semantics of the communication mechanisms used in a syntactic fragment of SysML, in particular synchronous and asynchronous, broadcast and buffered communication. In order to achieve generality of our approach, which supports establishing the consistency of the translation as well as enabling easy adaption between different source and target languages, we use a model based transformation approach. In particular, we use the ATLAS Transformation Language (ATL) framework that is nicely integrated in the Eclipse Modeling Framework (EMF) and in the Meta-Object Facility. We illustrate the application of this model transformation approach using an airbag system as a case study.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Konferenz
25th International Symposium on Model Checking Software : SPIN 2018, 20. Juni 2018 - 22. Juni 2018, Malaga
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690KÖLBL, Martin, Stefan LEUE, Hargurbir SINGH, 2018. From SysML to Model Checkers via Model Transformation. 25th International Symposium on Model Checking Software : SPIN 2018. Malaga, 20. Juni 2018 - 22. Juni 2018. In: DEL MAR GALLARDO, María, ed., Pedro MERINO, ed.. Model Checking Software : 25th International Symposium : SPIN 2018 : proceedings. Cham: Springer, 2018, pp. 255-274. Lecture Notes in Computer Science. 10869. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-94110-3. Available under: doi: 10.1007/978-3-319-94111-0_15
BibTex
@inproceedings{Kolbl2018SysML-42960,
  year={2018},
  doi={10.1007/978-3-319-94111-0_15},
  title={From SysML to Model Checkers via Model Transformation},
  number={10869},
  isbn={978-3-319-94110-3},
  issn={0302-9743},
  publisher={Springer},
  address={Cham},
  series={Lecture Notes in Computer Science},
  booktitle={Model Checking Software : 25th International Symposium : SPIN 2018 : proceedings},
  pages={255--274},
  editor={del Mar Gallardo, María and Merino, Pedro},
  author={Kölbl, Martin and Leue, Stefan and Singh, Hargurbir}
}
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/42960">
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42960/1/Koelbl_2-fcxzqisum9ld1.pdf"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42960/1/Koelbl_2-fcxzqisum9ld1.pdf"/>
    <dc:contributor>Singh, Hargurbir</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-08-03T11:21:50Z</dc:date>
    <dc:rights>terms-of-use</dc:rights>
    <dc:creator>Kölbl, Martin</dc:creator>
    <dc:creator>Singh, Hargurbir</dc:creator>
    <dcterms:title>From SysML to Model Checkers via Model Transformation</dcterms:title>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dc:language>eng</dc:language>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:issued>2018</dcterms:issued>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:abstract xml:lang="eng">In this paper we present an automated translation from the systems engineering modeling language SysML into the input languages of the NuSMV, Prism and Spin model checkers. A special focus of this work is the semantics of the communication mechanisms used in a syntactic fragment of SysML, in particular synchronous and asynchronous, broadcast and buffered communication. In order to achieve generality of our approach, which supports establishing the consistency of the translation as well as enabling easy adaption between different source and target languages, we use a model based transformation approach. In particular, we use the ATLAS Transformation Language (ATL) framework that is nicely integrated in the Eclipse Modeling Framework (EMF) and in the Meta-Object Facility. We illustrate the application of this model transformation approach using an airbag system as a case study.</dcterms:abstract>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/42960"/>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-08-03T11:21:50Z</dcterms:available>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:contributor>Kölbl, Martin</dc:contributor>
  </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
Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Ja
Begutachtet
Diese Publikation teilen