Publikation:

Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela

Vorschaubild

Dateien

Caltais_2-36psqv39yo5y6.pdf
Caltais_2-36psqv39yo5y6.pdfGröße: 777.81 KBDownloads: 488

Datum

2020

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-2-36psqv39yo5y6
DOI (zitierfähiger Link)
https://doi.org/10.5220/0008968303600372
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: Publikationen
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

HAMMOUDI, Slimane, ed., Luis FERREIRA PIRES, ed., Bran SELIC, ed.. Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development : Volume 1: MODELSWARD. Setúbal, Portugal: SCITEPRESS, 2020, pp. 360-372. ISBN 9789897584008. Available under: doi: 10.5220/0008968303600372

Zusammenfassung

In this paper we discuss the correctness of an ATL-based model transformation from the systems engineering modelling language SysML into Promela, the input language of the SPIN model checker. More precisely, we reduce showing the correctness of the transformation to showing a notion of what we refer to as observational equivalence of the SysML and the generated Promela models, respectively. This paves the way to a proof technique that could be further exploited in order to argue the correctness of model transformations from SysML to various model checkers, based on the observable actions generated by the systems under analysis.

Zusammenfassung in einer weiteren Sprache

Fachgebiet (DDC)
004 Informatik

Schlagwörter

Model Transformation, ATL, SysML, Promela, Correctness, Observational Equivalence

Konferenz

MODELSWARD 2020 : 8th International Conference on Model-Driven Engineering and Software Development, 25. Feb. 2020 - 27. Feb. 2020, Valletta, Malta
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690CALTAIS, Georgiana, Stefan LEUE, Hargurbir SINGH, 2020. Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela. MODELSWARD 2020 : 8th International Conference on Model-Driven Engineering and Software Development. Valletta, Malta, 25. Feb. 2020 - 27. Feb. 2020. In: HAMMOUDI, Slimane, ed., Luis FERREIRA PIRES, ed., Bran SELIC, ed.. Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development : Volume 1: MODELSWARD. Setúbal, Portugal: SCITEPRESS, 2020, pp. 360-372. ISBN 9789897584008. Available under: doi: 10.5220/0008968303600372
BibTex
@inproceedings{Caltais2020Corre-53127,
  year={2020},
  doi={10.5220/0008968303600372},
  title={Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela},
  isbn={9789897584008},
  publisher={SCITEPRESS},
  address={Setúbal, Portugal},
  booktitle={Proceedings of the 8th International Conference on Model-Driven Engineering and Software Development : Volume 1: MODELSWARD},
  pages={360--372},
  editor={Hammoudi, Slimane and Ferreira Pires, Luis and Selic, Bran},
  author={Caltais, Georgiana 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/53127">
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Caltais, Georgiana</dc:contributor>
    <dc:creator>Leue, Stefan</dc:creator>
    <dcterms:abstract xml:lang="eng">In this paper we discuss the correctness of an ATL-based model transformation from the systems engineering modelling language SysML into Promela, the input language of the SPIN model checker. More precisely, we reduce showing the correctness of the transformation to showing a notion of what we refer to as observational equivalence of the SysML and the generated Promela models, respectively. This paves the way to a proof technique that could be further exploited in order to argue the correctness of model transformations from SysML to various model checkers, based on the observable actions generated by the systems under analysis.</dcterms:abstract>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-03-10T13:04:37Z</dcterms:available>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dc:language>eng</dc:language>
    <dcterms:title>Correctness of an ATL Model Transformation from SysML State Machine Diagrams to Promela</dcterms:title>
    <dc:creator>Singh, Hargurbir</dc:creator>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/53127/1/Caltais_2-36psqv39yo5y6.pdf"/>
    <dc:contributor>Singh, Hargurbir</dc:contributor>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2021-03-10T13:04:37Z</dc:date>
    <dc:rights>terms-of-use</dc:rights>
    <dcterms:issued>2020</dcterms:issued>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dc:creator>Caltais, Georgiana</dc:creator>
    <dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/53127/1/Caltais_2-36psqv39yo5y6.pdf"/>
    <bibo:uri rdf:resource="https://kops.uni-konstanz.de/handle/123456789/53127"/>
  </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