Towards Correct Modelling and Model Transformation in DPF
Not peer reviewed
MetadataShow full item record
Model-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.
Paper 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: 10.1007/978-3-642-30454-5_3
Paper 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.
Paper 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: 10.14279/tuj.eceasst.67.943
Paper 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.
Paper 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: http://hdl.handle.net/1956/12351