@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
    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>