Search

We present work in progress on, verified, transformation of a modeling language based on communicating concurrent state machines, SLCO, to Java. Some concurrency related challenges, related to atomicity and non-standard fairness issues, are pointed out. We discuss solutions based on Java synchronization concepts.

In this paper we describe our experience in applying the Event-B formalism for specifying the dynamic semantics of a real-life industrial DSL. The main objective of this work is to enable the industrial use of the broad spectrum of specification analysis tools that support Event-B. To leverage the usage of Event-B and its analysis techniques we developed model transformations, that allowed for automatic generation of Event-B specifications of the DSL programs. The model transformations implement a modular approach for specifying the semantics of the DSL and, therefore, improve scalability of the specifications and the reuse of their verification. Keywords: domain specific language, Event-B, model transformations, verification and validation, reuse, scalability

Model transformations play a pivotal role in model-driven engineering. Since they are in many ways similar to traditional software artifacts, they have to be treated similarly. Therefore, it is necessary to assess their quality. We propose to use metrics to assess various quality attributes of model transformations In this paper, we focus on model transformations created using ATL, which ATL is currently one of the most widely used model transformation formalisms. We have collected metrics data from a heterogeneous collection of seven model transformations. The quality of the same transformations has been evaluated manually by nineteen ATL experts. We assess whether the metrics are appropriate predictors for the quality attributes by correlating the metrics data with the expert data. To support or refute the correlations, we also acquired qualitative statements from the ATL experts. Although the study was intended as a first exploration of the relation between metrics and quality attributes, some significant correlations were found that are supported by statements of the participants.