E-Thesis 231 views 72 downloads
Institution-based Semantics and Tool Support for the UML / TOBIAS ROSENBERGER
Swansea University Author: TOBIAS ROSENBERGER
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...
| 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!
|
| 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. |
|---|---|
| Keywords: |
UML, specification, verification, formal methods, institutions, modularity |
| College: |
Faculty of Science and Engineering |