From SysML to Model Checkers via Model Transformation
| Type of Publication: | Contribution to a conference collection |
| Publication status: | Published |
| URI (citable link): | http://nbn-resolving.de/urn:nbn:de:bsz:352-2-fcxzqisum9ld1 |
| Author: | Kölbl, Martin; Leue, Stefan; Singh, Hargurbir |
| Year of publication: | 2018 |
| Conference: | 25th International Symposium on Model Checking Software : SPIN 2018, Jun 20, 2018 - Jun 22, 2018, Malaga |
| Published in: | Model Checking Software : 25th International Symposium : SPIN 2018 : proceedings / del Mar Gallardo, María; Merino, Pedro (ed.). - Cham : Springer, 2018. - (Lecture Notes in Computer Science ; 10869). - pp. 255-274. - ISSN 0302-9743. - eISSN 1611-3349. - ISBN 978-3-319-94110-3 |
| DOI (citable link): | https://dx.doi.org/10.1007/978-3-319-94111-0_15 |
| Summary: |
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.
|
| Subject (DDC): | 004 Computer Science |
| Link to License: | In Copyright |
| Bibliography of Konstanz: | Yes |
Cite This
Files in this item
![[PDF]](/themes/Kops/images/mimes/pdf.png "PDF file"){kind=small}
KÖ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, Jun 20, 2018 - Jun 22, 2018. In: DEL MAR GALLARDO, María, ed., Pedro MERINO, ed.. Model Checking Software : 25th International Symposium : SPIN 2018 : proceedings. Cham:Springer, pp. 255-274. ISSN 0302-9743. eISSN 1611-3349. ISBN 978-3-319-94110-3. Available under: doi: 10.1007/978-3-319-94111-0_15
@inproceedings{Kolbl2018SysML-42960, title={From SysML to Model Checkers via Model Transformation}, year={2018}, doi={10.1007/978-3-319-94111-0_15}, number={10869}, isbn={978-3-319-94110-3}, issn={0302-9743}, address={Cham}, publisher={Springer}, 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 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/rdf/resource/123456789/42960"> <dc:contributor>Singh, Hargurbir</dc:contributor> <dc:rights>terms-of-use</dc:rights> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42960/1/Koelbl_2-fcxzqisum9ld1.pdf"/> <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/42960"/> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <dc:contributor>Leue, Stefan</dc:contributor> <dcterms:title>From SysML to Model Checkers via Model Transformation</dcterms:title> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>Singh, Hargurbir</dc:creator> <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/> <dc:creator>Leue, Stefan</dc:creator> <dc:contributor>Kölbl, Martin</dc:contributor> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/42960/1/Koelbl_2-fcxzqisum9ld1.pdf"/> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-08-03T11:21:50Z</dcterms:available> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dcterms:issued>2018</dcterms:issued> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2018-08-03T11:21:50Z</dc:date> <dc:creator>Kölbl, Martin</dc:creator> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/rdf/resource/123456789/36"/> <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> <dc:language>eng</dc:language> </rdf:Description> </rdf:RDF>
Downloads since Aug 3, 2018 (Information about access statistics)
| Koelbl_2-fcxzqisum9ld1.pdf | 319 |
This item appears in the following Collection(s)
Search KOPS
Browse
My Account
