No Cover Image

E-Thesis 231 views 72 downloads

Institution-based Semantics and Tool Support for the UML / TOBIAS ROSENBERGER

Swansea University Author: TOBIAS ROSENBERGER

  • 2023_Rosenberger_T.final.63491.pdf

    PDF | E-Thesis – open access

    Copyright: The Author, Tobias Rosenberger, 2023.

    Download (5.02MB)

DOI (Published version): 10.23889/SUthesis.63491

Abstract

Model-based techniques, in particular the Unified Modeling Language (UML), have found wideadoption in the software industry. Formal methods can produce software which is guaranteed topossess desired properties, this being of particular interest where safety or security are concerned.Formal methods h...

Full description

Published: Swansea, Wales, UK 2023
Institution: Swansea University
Degree level: Doctoral
Degree name: Ph.D
Supervisor: Roggenbach, Markus. and Bensalem, Saddek.
URI: https://cronfa.swan.ac.uk/Record/cronfa63491
Tags: Add Tag
No Tags, Be the first to tag this record!
first_indexed 2023-05-17T15:15:06Z
last_indexed 2023-05-17T15:15:06Z
id cronfa63491
recordtype RisThesis
fullrecord <?xml version="1.0" encoding="utf-8"?><rfc1807 xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema"><bib-version>v2</bib-version><id>63491</id><entry>2023-05-17</entry><title>Institution-based Semantics and Tool Support for the UML</title><swanseaauthors><author><sid>7fafc04b119dcfc9a5ad6f815ca608c0</sid><firstname>TOBIAS</firstname><surname>ROSENBERGER</surname><name>TOBIAS ROSENBERGER</name><active>true</active><ethesisStudent>false</ethesisStudent></author></swanseaauthors><date>2023-05-17</date><abstract>Model-based techniques, in particular the Unified Modeling Language (UML), have found wideadoption in the software industry. Formal methods can produce software which is guaranteed topossess desired properties, this being of particular interest where safety or security are concerned.Formal methods have been used very successfully in certain fields like the railway domain (e.g.,the verification of the fully automatic lines of the Paris metro system). However, in the widersoftware industry the adoption of formal methods has been limited. This thesis is part of an effortto ease the uptake of formal methods by enabling a fully formal use of the UML. In pursuing thisgoal, we want to follow software engineering best practices such as the don’t-repeat-yourselfprinciple and modularity.To achieve this, we use Institution Theory and the Heterogeneous Toolset (HeTS). InstitutionTheory is a principled way to relate different formalisms in a modular way. The HeterogeneousToolset is based on Institution Theory and implements tool reuse across different formalisms. Thisis the context into which we wish to integrate the UML, by providing institutional semantics andHeTS implementations for the different UML sublanguages. Translations between these UMLinstitutions then give joint semantics. Translations to other established languages implementedin HeTS allow us to borrow their tool-support.The contributions of this thesis to the effort outlined above consist in the development oflanguages for UML State Machines and Composite Structures and translations to the existinglanguage Casl. We give an account of our languages and translations in terms of InstitutionTheory, as well as a prototypical implementation in HeTS. Further, we verify properties based onspecifications in our languages to demonstrate the feasibility of our approach. The experiencesfrom our work on institutionalisation, implementation and verification moreover point to severalopportunities for future work.</abstract><type>E-Thesis</type><journal/><volume/><journalNumber/><paginationStart/><paginationEnd/><publisher/><placeOfPublication>Swansea, Wales, UK</placeOfPublication><isbnPrint/><isbnElectronic/><issnPrint/><issnElectronic/><keywords>UML, specification, verification, formal methods, institutions, modularity</keywords><publishedDay>20</publishedDay><publishedMonth>4</publishedMonth><publishedYear>2023</publishedYear><publishedDate>2023-04-20</publishedDate><doi>10.23889/SUthesis.63491</doi><url/><notes/><college>COLLEGE NANME</college><CollegeCode>COLLEGE CODE</CollegeCode><institution>Swansea University</institution><supervisor>Roggenbach, Markus. and Bensalem, Saddek.</supervisor><degreelevel>Doctoral</degreelevel><degreename>Ph.D</degreename><degreesponsorsfunders>Swansea University (College of Science scholarship), Université Grenoble Alpes (Fixed-term employment in the EU project BRAIN IoT)</degreesponsorsfunders><apcterm/><funders/><projectreference/><lastEdited>2023-09-28T15:42:29.3089426</lastEdited><Created>2023-05-17T16:12:47.3302729</Created><path><level id="1">Faculty of Science and Engineering</level><level id="2">School of Mathematics and Computer Science - Computer Science</level></path><authors><author><firstname>TOBIAS</firstname><surname>ROSENBERGER</surname><order>1</order></author></authors><documents><document><filename>63491__27501__894ecc13f5a442879387df1e61cfae59.pdf</filename><originalFilename>2023_Rosenberger_T.final.63491.pdf</originalFilename><uploaded>2023-05-17T16:16:12.5029280</uploaded><type>Output</type><contentLength>5260983</contentLength><contentType>application/pdf</contentType><version>E-Thesis – open access</version><cronfaStatus>true</cronfaStatus><documentNotes>Copyright: The Author, Tobias Rosenberger, 2023.</documentNotes><copyrightCorrect>true</copyrightCorrect><language>eng</language></document></documents><OutputDurs/></rfc1807>
spelling v2 63491 2023-05-17 Institution-based Semantics and Tool Support for the UML 7fafc04b119dcfc9a5ad6f815ca608c0 TOBIAS ROSENBERGER TOBIAS ROSENBERGER true false 2023-05-17 Model-based techniques, in particular the Unified Modeling Language (UML), have found wideadoption in the software industry. Formal methods can produce software which is guaranteed topossess desired properties, this being of particular interest where safety or security are concerned.Formal methods have been used very successfully in certain fields like the railway domain (e.g.,the verification of the fully automatic lines of the Paris metro system). However, in the widersoftware industry the adoption of formal methods has been limited. This thesis is part of an effortto ease the uptake of formal methods by enabling a fully formal use of the UML. In pursuing thisgoal, we want to follow software engineering best practices such as the don’t-repeat-yourselfprinciple and modularity.To achieve this, we use Institution Theory and the Heterogeneous Toolset (HeTS). InstitutionTheory is a principled way to relate different formalisms in a modular way. The HeterogeneousToolset is based on Institution Theory and implements tool reuse across different formalisms. Thisis the context into which we wish to integrate the UML, by providing institutional semantics andHeTS implementations for the different UML sublanguages. Translations between these UMLinstitutions then give joint semantics. Translations to other established languages implementedin HeTS allow us to borrow their tool-support.The contributions of this thesis to the effort outlined above consist in the development oflanguages for UML State Machines and Composite Structures and translations to the existinglanguage Casl. We give an account of our languages and translations in terms of InstitutionTheory, as well as a prototypical implementation in HeTS. Further, we verify properties based onspecifications in our languages to demonstrate the feasibility of our approach. The experiencesfrom our work on institutionalisation, implementation and verification moreover point to severalopportunities for future work. E-Thesis Swansea, Wales, UK UML, specification, verification, formal methods, institutions, modularity 20 4 2023 2023-04-20 10.23889/SUthesis.63491 COLLEGE NANME COLLEGE CODE Swansea University Roggenbach, Markus. and Bensalem, Saddek. Doctoral Ph.D Swansea University (College of Science scholarship), Université Grenoble Alpes (Fixed-term employment in the EU project BRAIN IoT) 2023-09-28T15:42:29.3089426 2023-05-17T16:12:47.3302729 Faculty of Science and Engineering School of Mathematics and Computer Science - Computer Science TOBIAS ROSENBERGER 1 63491__27501__894ecc13f5a442879387df1e61cfae59.pdf 2023_Rosenberger_T.final.63491.pdf 2023-05-17T16:16:12.5029280 Output 5260983 application/pdf E-Thesis – open access true Copyright: The Author, Tobias Rosenberger, 2023. true eng
title Institution-based Semantics and Tool Support for the UML
spellingShingle Institution-based Semantics and Tool Support for the UML
TOBIAS ROSENBERGER
title_short Institution-based Semantics and Tool Support for the UML
title_full Institution-based Semantics and Tool Support for the UML
title_fullStr Institution-based Semantics and Tool Support for the UML
title_full_unstemmed Institution-based Semantics and Tool Support for the UML
title_sort Institution-based Semantics and Tool Support for the UML
author_id_str_mv 7fafc04b119dcfc9a5ad6f815ca608c0
author_id_fullname_str_mv 7fafc04b119dcfc9a5ad6f815ca608c0_***_TOBIAS ROSENBERGER
author TOBIAS ROSENBERGER
author2 TOBIAS ROSENBERGER
format E-Thesis
publishDate 2023
institution Swansea University
doi_str_mv 10.23889/SUthesis.63491
college_str Faculty of Science and Engineering
hierarchytype
hierarchy_top_id facultyofscienceandengineering
hierarchy_top_title Faculty of Science and Engineering
hierarchy_parent_id facultyofscienceandengineering
hierarchy_parent_title Faculty of Science and Engineering
department_str School of Mathematics and Computer Science - Computer Science{{{_:::_}}}Faculty of Science and Engineering{{{_:::_}}}School of Mathematics and Computer Science - Computer Science
document_store_str 1
active_str 0
description Model-based techniques, in particular the Unified Modeling Language (UML), have found wideadoption in the software industry. Formal methods can produce software which is guaranteed topossess desired properties, this being of particular interest where safety or security are concerned.Formal methods have been used very successfully in certain fields like the railway domain (e.g.,the verification of the fully automatic lines of the Paris metro system). However, in the widersoftware industry the adoption of formal methods has been limited. This thesis is part of an effortto ease the uptake of formal methods by enabling a fully formal use of the UML. In pursuing thisgoal, we want to follow software engineering best practices such as the don’t-repeat-yourselfprinciple and modularity.To achieve this, we use Institution Theory and the Heterogeneous Toolset (HeTS). InstitutionTheory is a principled way to relate different formalisms in a modular way. The HeterogeneousToolset is based on Institution Theory and implements tool reuse across different formalisms. Thisis the context into which we wish to integrate the UML, by providing institutional semantics andHeTS implementations for the different UML sublanguages. Translations between these UMLinstitutions then give joint semantics. Translations to other established languages implementedin HeTS allow us to borrow their tool-support.The contributions of this thesis to the effort outlined above consist in the development oflanguages for UML State Machines and Composite Structures and translations to the existinglanguage Casl. We give an account of our languages and translations in terms of InstitutionTheory, as well as a prototypical implementation in HeTS. Further, we verify properties based onspecifications in our languages to demonstrate the feasibility of our approach. The experiencesfrom our work on institutionalisation, implementation and verification moreover point to severalopportunities for future work.
published_date 2023-04-20T15:42:30Z
_version_ 1778292779103813632
score 11.014246

Similar Items