DCMODELSWARD 2015 Abstracts

Full Papers
Paper Nr: 1

Formal Verification of Relational Model Transformations using an Intermediate Verification Language


Zheng Cheng

Abstract: Model-driven engineering has been recognised as an effective way to manage the complexity of software development. Model transformation is widely acknowledged as one of the central ingredients of Model-driven engineering. Among different paradigms of model transformations, I specifically interest in relational model transformations for their mapping-style nature. Proving the correctness of relational model transformation is my major concern. Here "correctness" means implicit assumptions about the relational model transformation. These assumptions can be made explicitly via annotations, so-called contracts. In particular, my main objective is to design a static verifier for the target relational model transformation language by applying formal methods, which allows the designed verifier to analyse annotated relational model transformation and check that the given correctness contracts are never violated. I aim at modular, reusable and reliable verifier designing. Thus, I develop the VeriMTLr framework. It assists in designing verifiers that allow automatic theorem proving of the correctness of relational model transformation. VeriMTLr draws on the Boogie intermediate verification language to systematically designing modular and reusable verifier for a target relational model transformation language. The framework encapsulates the memory model (for formalizing metamodels) and the contract libraries (which formalises OCL, SET theory and first order logic) to reduce coding costs and time of verifier construction. Furthermore, VeriMTLr encapsulates the EMFTVM bytecode formalisation, which enables automated translation validation approach (from compiler verification) to ensure the reliability of the verification result of designed verifier. Three use cases of the VeriMTLr framework are demonstrated. I also identify the limitations of VeriMTLr, and outline the future works for its development.

Paper Nr: 2

Model-driven Engineering in Support of Development, Test and Maintenance of Communication Middleware - A Preliminary Industrial Case-Study


Deniz Akdur and Vahid Garousi

Abstract: Embedded real-time software systems are widespread and can be found in many devices in our everyday life, e.g., in cars, TVs, aviation, etc. Development and testing of embedded software is usually more challenging compared to regular software systems. The scale and complexity of these systems makes it infeasible to deploy them in disconnected, standalone configurations. Therefore, communication is at the heart of all distributed systems. The latest modern distributed real-time and embedded systems have numerous components in which interfaces and middleware layers play crucial roles. Defects in those components could lead to minor issues or even life-threatening system failures. For example, message-communication-related faults such as wrong message sizes exchanged between the interfaces might be left uncovered during testing activities. Delays in integration can create huge costs and extra effort might be needed to verify all the implemented internal business logic and message interfaces. Furthermore, late defect correction in live systems after deployment for these types of software systems costs much more compared to regular software systems due to the close hardware interactions. Thus, it is very crucial to verify communication interfaces between different hardware and software modules earlier before delivery to ensure proper interoperability of these modules. Furthermore, it has been observed in several industrial contexts that when hardware, software modules and related communication interfaces evolve in those systems, synchronization of source code with other artifacts becomes a major challenge. In a specific industrial context, ASELSAN Inc., one of Turkey's leading defense companies, all the above challenges were regularly faced and thus, to address them, we design, implement and evaluate a toolset in the context of Radar & Electronic Warfare Systems (REWS) division.In this paper, we report our progress in this ongoing R&D project. The solution approach is based on the Model-Driven Engineering (MDE) which is in support of development, test and maintenance of communication middleware. The toolset has been developed using the Eclipse Modeling Framework (EMF) and is titled: Model-ComM, standing for Model-driven Communication Middleware, which automatically generates code, document and test driver for communication interfaces of each component depending on the type of protocol and the architecture of the system. This tool is currently in use by many teams in the company. The approach and the case study reported in this paper is only one component of the PhD dissertation of the first author. The thesis' overall plan is to focus on a comprehensive investigation of industrial and empirical evidence of using MDE, which has a multidisciplinary research methodology. Firstly, the thesis plans to investigate recent modeling usage and its adoption with describing and understanding the industrial experience, which is based on survey and exploratory & improving case study strategies with interviews. Secondly, to show the positive impact of MDE by addressing the lack of empirical results in the industry, this study uses an industrial evidence to ensure the cost effectiveness and benefit of MDE by realizing technology transfer via Model-ComM, which is based on Action Research.