Vis enkel innførsel

dc.contributor.authorWang, Xiaoliang
dc.date.accessioned2016-07-29T09:52:47Z
dc.date.available2016-07-29T09:52:47Z
dc.date.issued2016-06-14
dc.identifier.urihttps://hdl.handle.net/1956/12352
dc.description.abstractModel-driven engineering (MDE) is a model-centric software development methodology. It promotes models as first-class entities in software de- velopment. Models are used to represent software along software devel- opment process and to finally generate software automatically by model transformations. Thus, the quality of software is highly dependent on models and model transformations. This thesis devotes to construct cor- rect models and model transformations in Diagram Predicate Framework (DPF), which provides a formal diagrammatic approach to (meta)modelling and model transformation based on category theory. The thesis presents the DPF Model Editor, a graphical (meta)modelling editor for DPF which supports diagrammatic (meta)modelling. In addi- tion, we propose bounded verification approaches of models and model transformations respectively by using Alloy. Alloy consists of a model- ling language and the Alloy Analyzer to examine Alloy specifications. The verification approaches proposed in the thesis translate models and model transformations into Alloy specifications, which are passed to the Alloy Analyzer to verify whether the models and model transformations satisfy some desired properties. Because of the inherent limitation of Alloy, the verification approaches also encounter a scalability problem: it may take quite long time or be- come intractable to verify larger models or complex model transforma- tions. To tackle the problem, the thesis also presents several techniques to optimize the approaches. The first technique splits models into submod- els and reduces the verification of the models into the verification of some submodels. The other two techniques are proposed for the verification of model transformations: one technique uses a modelling approach to sim- plify model transformations; while the other one optimizes the translation of model transformation rules. Experim at these tech-niques alleviate the scalability problem.en_US
dc.language.isoengeng
dc.publisherThe University of Bergenen_US
dc.relation.haspartPaper I: Yngve Lamo, XiaoliangWang, Florian Mantz,Wendy MacCaull, and Adrian Rutle. DPF Workbench: A Diagrammatic Multi-Layer Domain Specific (Meta-)Modelling Environment. In Computer and Information Science, volume 429 of SCI, pages 37–52. Springer, 2012 This article is not available in BORA. The published version is available at: <a href="http://dx.doi.org/ 10.1007/978-3-642-30454-5_3"target="blank">10.1007/978-3-642-30454-5_3</a>en_US
dc.relation.haspartPaper II: Xiaoliang Wang, Adrian Rutle, and Yngve Lamo. Towards User- Friendly and Efficient Analysis with Alloy. volume 1514 of CEUR Workshop Proceedings, pages 28–37, 2015 This article is not available in BORA. </a>en_US
dc.relation.haspartPaper III: Xiaoliang Wang, Fabian Büttner, and Yngve Lamo. Verification of Graph-based Model Transformations Using Alloy. ECEASST, 67, 2014 This article is not available in BORA. The published version is available at: <a href="http://dx.doi.org/10.14279/tuj.eceasst.67.943"target="blank">10.14279/tuj.eceasst.67.943</a>en_US
dc.relation.haspartPaper IV: Xiaoliang Wang, Adrian Rutle, and Yngve Lamo. Scalable Verification of Model Transformations. In Proceedings of the 11th Workshop on Model-Driven Engineering, Verification and Validation co-located with and Systems, volume 1235 of CEUR Workshop Proceedings, pages 29– 38. CEUR-WS.org, 2014 This article is not available in BORA. </a>en_US
dc.relation.haspartPaper V: XiaoliangWang andAdrianRutle. Model Checking Healthcare Workflows Using Alloy. InMMHS, volume 37 of Procedia Computer Science, pages 481–488. Elsevier, 2014 The article is available in BORA at: <a href="http://hdl.handle.net/1956/12351" target="blank">http://hdl.handle.net/1956/12351</a>en_US
dc.titleTowards Correct Modelling and Model Transformation in DPFen_US
dc.typeDoctoral thesis
dc.rights.holderCopyright the author. All rights reserved.en_US
dc.identifier.cristin1372384
dc.subject.nsiVDP::Matematikk og Naturvitenskap: 400en_US


Tilhørende fil(er)

Thumbnail

Denne innførselen finnes i følgende samling(er)

Vis enkel innførsel