View models are key concepts of domain-specific modeling to provide task-specific focus (e.g., power or communication architecture of a system) to the designers by highlighting only the relevant aspects of the system under design. View models can be specified by unidirectional graph queries, and automatically maintained from the underlying source model using incremental transformation techniques. However, tracing back the consequence of a modification in the abstract view to the source model is a challenging task as several valid source changes may correspond to a single change in the view. Calculating these source changes requires complex logic analysis which has to take into account both queries defining the view and the structural well-formedness constraints of the source model. In this paper we outline a systematic technique to calculate valid source candidates by iterative calls to underlying SAT solvers.
2 MTA-BME Lendület Cyber-Physical Systems Research Group
View models are key concepts of domain-specific modeling to provide task-specific focus (e.g., power or communication architecture of a system) to the designers by creating a model which highlights only the relevant aspects of the system under design and aids the detection of conceptual flaws. In [DHH+14], we proposed an approach to define view models in a highly automated way, based on unidirectional declarative graph queries [UBH+15] and using incremental transformation techniques [VB07].
However, view models created in this way are read-only representations, thus changes in the view model can not be directly propagated to a change in the source model. When a conceptual change is need to be done in a view model, the developer is forced to edit the source model, and manually check if the modified model corresponds to the expected view model. Additionally, there might be several other views which may be unintentionally changed, or structural well-formedness constraint may be violated by the manual modification on the source.
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
phone: Sensor t r irgge type s m1: Measure triggeredBy pressureDone: EventTrigger what r1 :Report where gp:Host pt:PeriodicTrigger when
dataflow(type, host) pulse: Tmyepaseures typet:ypTeype hostw:Hheorset
tr 2. Transfor- :Measurement :Report m2 :Metyapseure irsgge mation t:rEigvgeenretdTBryiggerwhat
triggeredBy 4. Change pulseDone: EventTrigger Pulse Emerg
what r2 :Rewpoherrte Pressure emerg:Host 3. View Model
Pulse «new» GP Pressure GP
5. Changed Model Data-flow models 6. Change propagation «del»
Emerg
To overcome this problem we propose a technique to automatically deduce source model variant which are consistent to a changed view model. First (i) the unaffected partition of the source model is selected to restrict the impact of a modification, (ii) transforms the modified view model to a set of logic conditions according to the specification of the view defining graph queries and (iii) calculates possible candidate solutions by dedicated SAT solvers by combining the unaffected part, the conditions and the well-formedness constraints. Hence, this technique helps the developement process by allowing the enumeration on valid design decisions for a change in the view model. An initial implementation is carried out using Alloy Analyser [all] as the back-end solver to construct several solution candidates. 2
Our change propagation approach is illustrated in the context of the healthcare case study developed for the Concerto Artemis project [con]. As source model, a health care architecture metamodel is developed which consists of Sensor instances that measure specific Type of data. The execution of a measurement can be initiated by a PeriodicTrigger while an EventTrigger captures the end of a measure and can trigger Report operation to send the measured data to a specific Host. A domain-specific language may define several well-formedness constraints (WF) to ensure the correctness of the model under developement, which tipically defined in OCL invariants [OCL06], or as graph patterns [BHR+10]. For example, in the architecture level a WF specifies that all the measurements have to be reported. As view model, a data-flow model is created which connects measurement Types to the target Host.
Example. Our approach is illustrated on a pulse and blood pressure measurement environment controlled by a smart phone, which is depicted on the left side of Fig. 1 labelled as Initial Model in Step 1. The measurement is executed by the Sensors of a mobile phone. The phone measures two types of data: pulse and blood pressure. The measurements m1 and m2 are executed periodically, triggered by the the phone timer pt. The completion event of the measurements triggers the job for processing of the sensor data: pressureDone and pulseDone. The result of the measurement is collected to Reports r1 and r2, and sent to the different hosts. In our case study, the blood pressure is sent to the general practitioner (GP) of the patient for logging, and signs of hearth failure is sent to hospitals (modelled by emerg). In order to create a focused view on what information is sent to the hosts, a view model of the data-flow is created in step Step 2. Graph pattern dataflow(type, host) is presented in the middle-top of Fig. 1, which matches to a type-host pair if the corresponding measurement is triggered and reported to the host. Therefore the data-flow model labelled as View Model is created in Step 3 : the pulse is sent to the emergency department, and the blood pressure is forwarded to the General Practitioner (GP).
Let us assume that the developer makes changes in the data-flow model depicted in Step 4 : the data-flow from Pulse to Emergency is redirected to the General Practicioner (noted by «del» and «new»), which results in Changed Model in Step 5. Two possible resolution of the source (architecture) model is proposed. In Step 7.A the pulse and blood pressure is reported in the same message. Technically, the r2 report has been removed, therefore the communication with Emergency is terminated, and a relation is added to r1. In Step 7.B the results of the measurements are sent in two separate reports. Report r2 is also removed in this case, and a new report is added to the model that sends the measurement results to the new address. In both cases, the well-formedness constraints are satisfied. = +
WF WF WF ′ = + 11 2 3 «new»
«del» trace specifies which view model element is created from which match (as described in [DHH+14]), and [m
We assume that traceability links are built and maintained during the forward propagation of changes: [t → m] collects the source model elements whose change may invalidate the match (including the binding of symbolic → s] parameters, and possible interpretation of internal variables). Upon a change from t to t0, the model can be separated into two partitions: fixed model partition tf is the part of t which remains unchanged, while old part to is changed to a new part tn (cross-references are included in to and tn). Consequently, a fixed subset of matches mf , and the changed subset mo can be calculated via the [t → m] trace. The source model is also partitioned to sf and so using the [m → s] trace where sf contains the objects whose are not associated to any objects or edges of the changing part of the view model tn. In this paper, we associate an object to a pattern match if the object is bound to a parameter or inner variable of the pattern. This information is conceptually stored in the traceability links. In the future, more sophisticated calculation can applied to select the relevant part more precisely. tn directly specifies the invalidated and newly introduced matches mn. However, the changed subset of matches mn specifies declarative structural constraints only, which have to be satisfied by the modified part.
Therefore the possible solutions sn for a change in the target model are calculated based on (1) the unchanged part of the source model sf , (2) the requirements defined by the changed matches mn, and (3) additional domainspecific well-formedness constraints WF. All these constraints are transformed into a first-order logic problem to be solved by a logic (SAT/SMT) solver. The solver provides several possible valid solutions for sn, which from the model developer may choose the most suitable one sin. Finally, the obsolete part so is replaced with sin.
In order to represent model generation tasks as logic problems, the structural constraints of the source metamodel are mapped to a set of formulae Meta. Additionally, the well-formedness constraints WF can be added to the logic problem to create valid solutions. Finally, [SBH+15] describes how graph patterns Patterns and requirements about the matches defined by the view model Matches can be translated to logic relations and assertions. Therefore, an s where s |= Meta ∧ WF ∧ Patterns ∧ Matches is a valid source model, where view defining patterns has matches as the constraint Matches specifies, so A1 Consistency and A2 Well-formedness challenges are satisfied, similarly as [MC13] describes. However, generating full models from scratch causes scalability issues (which is a common problem with logic solvers). Additionally, A3 Localization and A4 Minimal Changes assumptions are ignored, or have to be enforced by additional constraints. However, in our approach the generated source model is separated into a fix sf and changing sn part, where only the generation of the sn part is issued to the solver, similarly as [SVV16] describes incremental model generation. Hence, the well-formedness and the view definitions in sf can be excluded from the problem to simplify the problem and ensure A3 and A4 requirements, while creating problems proportional only to the size of the changing part.
Evaluation. By applying the method described in the previous section, valid health care system variations were synthesized. In the following we evaluate our solution with respect to the outlined challenges: Challenge 1: Because the query specification is explicitly mapped to constraints on the model fragment to be generated, the correspondence is ensured.
Challenge 2: The well-formedness constraints can be directly added to the logic problem, therefore only valid models will be generated.
Challenge 3: Our solution selects the largest part in the source model where the change may be synthesised.
While approach is useful for searching solutions which are hard to satisfy, or identify unsatisfiable changes, simple changes may have unnecessary side-effects in irrelevant model partitions.
Challenge 4: In the current state, our approach replaces the old partition with newly created objects, and does not takes the previous state of the modified part into account.
While challenge 1. and 2. is solved, our the current solution may underperform in aspects of 3. and 4. In the future, we plan to generate solutions in multiple steps, where the scope of the change is limited at first, and in each step extended with additional elements if the solver fails to create simple solutions. For example, in the first step the solver should try to set only attributes, then it can redirect edges, and finally create or delete objects. We expect that these steps can be used to prioritise better solutions. 4
Most of the view model synchronization techniques use bijective transformations where the rules are pairs of functions reverse of each other such in lenses [FGM+07], injective functions [MHT04], ATL [XLH+07] or relational/declarative descriptions such as in TGG [HEO+13] or QVT [Ste10]. These transformations can provide incremental backward propagation of changes. However, well-formedness constraints have to be included in all transformation pairs separately and cannot guarantee the completeness and unambiguity of the solutions.
Other approaches, such as [CDREP10], allow non-injective transformation for target model derivation such as that use logical representation to calculate the reverse direction. [MC13] reuses the declarative rule definition of QVT-R and maps it to Alloy SAT solver. [CK13] formalise the problem to Linear Programming. However, these techniques aim to find valid source models from scratch, instead of valid model parts. Moreover, well-formedness constraints are not taken into account. [Het10] defines the partial synchronization, where the changing part of the model is defined by a minimal explanation of an abductive reasoning problem. In contrast to our work, [Het10] defines an operation-based approach to search for minimal set of operations on the source model.
We believe that our contribution is unique in the context of state-based model synchronization in the sense that uni-directional and non-injective derivation rules are reversed using a SAT-solver to find well-formed models solutions, where the rules are mapped to first-order logic constraints and only relevant model parts are extended instead of the recalculation of the whole source model. 5
In this paper, we presented an approach for backward propagation of changes from view to source models by (i) selecting the impact of a modification, (ii) transforming the modified view model to logic conditions and (iii) calculating possible solution candidates by mapping the unaffected part, the conditions and well-formedness constraint to a SAT problem. Initial prototype is implemented which successfully generated design candidates for the case study using Alloy Analyzer as the back-end solver. As future work, we plan to (i) priorize the synthesized solutions and (ii) evaluate the performance of our approach on different measurement scenarios. Acknowledgement This paper is partially supported by the CONCERTO (ART-2012-333053) and the MTA-BME Lendület 2015 Research Group on Cyber-Physical Systems.
Gábor Bergmann, Ákos Horváth, István Ráth, Dániel Varró, András Balogh, Zoltan Balogh, and András Ökrös. Incremental evaluation of model queries over EMF models. In Model Driven Engineering Languages and Systems, MODELS 2010, pages 76–90, 2010. [all] [BHR+10] [DHH+14] [HEO+13] [SBH+15] [UBH+15] [VB07] [XLH+07]
Glenn Callow and Roy S Kalawsky. A satisficing bi-directional model transformation engine using mixed integer linear programming. 2013.
Csaba Debreceni, Ákos Horváth, Ábel Hegedüs, Zoltán Ujhelyi, István Ráth, and Dániel Varró. Query-driven incremental synchronization of view models. In Proceedings of the 2nd Workshop on View-Based, Aspect-Oriented and Orthographic Software Modelling, page 31. ACM, 2014. [CDREP10] Antonio Cicchetti, Davide Di Ruscio, Romina Eramo, and Alfonso Pierantonio. Jtl: a bidirectional and change propagating transformation language. In Software Language Engineering, pages 183– 202. Springer, 2010.
Frank Hermann, Hartmut Ehrig, Fernando Orejas, Krzysztof Czarnecki, Zinovy Diskin, Yingfei Xiong, Susann Gottmann, and Thomas Engel. Model synchronization based on triple graph grammars: correctness, completeness and invertibility. Software & Systems Modeling, 14(1):241–269, 2013.
Nuno Macedo and Alcino Cunha. Implementing qvt-r bidirectional model transformations using alloy. In Fundamental Approaches to Software Engineering, pages 297–311. Springer, 2013. Shin-Cheng Mu, Zhenjiang Hu, and Masato Takeichi. An injective language for reversible computation. In Mathematics of Program Construction, pages 289–313. Springer, 2004.
Object Constraint Language, v2.0, May 2006.
Oszkár Semeráth, Ágnes Barta, Ákos Horváth, Zoltán Szatmári, and Dániel Varró. Formal validation of domain-specific languages with derived features and well-formedness constraints. Software & Systems Modeling, 2015.
Perdita Stevens. Bidirectional model transformations in QVT: semantic issues and open questions. Software & Systems Modeling, 9(1):7–20, 2010.
Oszkár Semeráth, András Vörös, and Dániel Varró. Iterative and incremental model generation by logic solvers. Fundamental Approaches to Software Engineering, 19th International Conference, FASE 2016, 2016.
Zoltán Ujhelyi, Gábor Bergmann, Ábel Hegedüs, Ákos Horváth, Benedek Izsó, István Ráth, Zoltán Szatmári, and Dániel Varró. EMF-IncQuery: An integrated development environment for live model queries. Sci. Comput. Program., 98:80–99, 2015.
Dániel Varró and András Balogh. The Model Transformation Language of the VIATRA2 Framework. Science of Computer Programming, 68(3):214–234, October 2007.