=Paper=
{{Paper
|id=Vol-2019/gemoc_1
|storemode=property
|title=Bridging Engineering and Formal Modeling: WebGME and Formula Integration
|pdfUrl=https://ceur-ws.org/Vol-2019/gemoc_1.pdf
|volume=Vol-2019
|authors=Tamas Kecskes,Qishen Zhang,Janos Sztipanovits
|dblpUrl=https://dblp.org/rec/conf/models/KecskesZS17
}}
==Bridging Engineering and Formal Modeling: WebGME and Formula Integration==
https://ceur-ws.org/Vol-2019/gemoc_1.pdf
Bridging Engineering and Formal Modeling: WebGME and Formula Integration
Tamas Kecskes Qishen Zhang Janos Sztipanovits
Department of EECS, Vanderbilt University, Nashville, TN
{tamas.kecskes, qishen.zhang, janos.sztipanovits}@vanderbilt.edu
Abstract—Emergence of heterogeneous engineering domains are restricted to modeling language constructs limited to
that cross disciplinary boundaries lead to design flows that modeling the interactions among different and changing
span multiple Domain Specific Modeling Languages (DSML). modeling domains. The cost of introducing easy-to-evolve
Analyzing system level behavior and pursuing cross-domain model integration languages - that are themselves DSMLs -
trade-offs requires the semantic integration of modeling do- is the requirement for explicit representation of their formal
mains. Driven by the specific needs of and our experience semantics, which is necessary to preserve the semantic
with design automation tool suites for Cyber-Physical Systems integrity of design flows [2].
(CPS), this paper focuses on using model integration languages In our previous work, developing the OpenMETA de-
as a flexible way for modeling cross-domain interactions. The sign automation tool suite for DARPA’s Adaptive Vehicle
primary challenge in specifying and supporting model inte- Make program [3], we addressed these needs by pursuing
gration languages is that both rapid evolvability and semantic and coordinating two parallel paths in model integration.
precision are required. This challenge is mapped into a meta- As a first step, we specified and continuously evolved the
level model integration problem, the integration of a meta- CyPhyML model integration language focusing on the in-
modeling language used for specifying DSMLs and configuring tegrated OpenMETA design flow targeting ground vehicle
the underlying meta-programmable modeling tool WebGME, design [3]. Since the OpenMETA design flow extended
and a formal framework that uses algebraic data types and to multiple physical and cyber domains, CyPhyML itself
Constraint Logic Programming - Formula - devoted to formally
proved to be a complex DSML requiring the use of our
meta-programmable modeling tool, WebGME[4]. To satisfy
specifying the semantics of DSMLs and model transformations.
the need for representing and evolving the formal seman-
The primary contribution of the paper is the deep semantic in-
tics of CyPhyML, we developed the OpenMETA Semantic
tegration of WebGME and Formula that keep the engineering
Backplane[2]. It provided a formal representation of the
view of an evolving model integration language and its formal
interacting physical and cyber domains. Although the two-
representation tightly synchronized.
pronged approach satisfied the basic needs, the challenge
Index Terms—WebGME, Formula, DSML, Model Transforma- of synchronizing the CyPhyML and Formula models, and
tion, Constraint Programming. meta-models decreased the benefits of the Semantic Back-
plane.
In this paper we discuss our recent work on establish-
1. Introduction ing a deep integration of WebGME and Formula. Deep
integration means keeping the two representations - the
Modeling tools are key enablers of model-driven engi- CyPhyML meta-models and models in WebGME and their
neering. They are responsible for offering intuitive engineer- FORMULA equivalent - fully synchronized and providing
ing interface (usually graphical) for model developers and seamless access to complementary services of the tools.
they provide a range of services supporting safe model en- WebGME services include [4]:
gineering practices including composing/decomposing, vi-
• meta-programmability with prototypal inheritance
sualizing, modifying, checking well-formedness, version-
that allows smooth language integration and evolu-
ing, and storing large models. Adaption of model-driven
tion,
methods in new cross-disciplinary fields such as Cyber-
• graphical concrete syntax that is highly customiz-
Physical Systems (CPS) challenges modeling tool develop-
able,
ers with heterogeneity: design flows require the integration
• multiple, well defined APIs for model interpretation
of multi-physics, multi-abstraction and multi-fidelity mod-
and tool integration,
els expressed in a rich set of domain-specific modeling
• version control with branch support to allow mod-
languages (DSML). Since design flows and the tools in-
eling in large, and
volved in their implementation change, the suite of relevant
• collaborative, distributed modeling via web-
modeling languages is not static; they evolve continuously.
interface.
Our approach to manage model heterogeneity has been
the introduction of model integration languages [1] that
FORMULA services include: state-of-the-art satisfiability modulo theories (SMT) solver
Z3 [14].
• formal representation of structural semantics of In summary, the Formula tool complements WebGME
modeling languages [5] as strongly-typed, open- with a range of essential services: verifying if domain con-
World logic programs (OLP) [6] offering specifi- straints are consistent (the domain is not empty), completing
cations that are highly declarative and executable, partially defined models that are part of the domain, check-
they can express static, dynamic, and transformation ing well-formedness of models, formally specifying (and
semantics of DSMLs, executing) model transformations, and formally composing
• program synthesis and automated reasoning enabled domains.
by the symbolic execution of logic programs into
quantifier-free sub-problems, which are dispatched
to the state-of-the-art SMT solver Z3 [7],
4. Integration Architecture
• modular reuse of DSMLs via the composition of To provide a seamless and tight integration that com-
OLPs in a strong category theoretic sense [8]. bines the modeling power of WebGME with the reasoning
The primary contribution of this paper is the semantic engine of Formula, we have created an integration archi-
integration between the tools, detailing the relationship be- tecture presented in Figure 1. As it is shown, the WebGME
tween WebGME meta-models and Formula domain spec- client interface has a single communication channel towards
ifications. The following sections presents the integrated the server, that helps in providing a unified platform where
use of WebGME and Formula services using constraint the user is able to harness the capabilities of both tools.
specification as example. To keep the WebGME project and its Formula represen-
tation synchronized, the system uses the webhook feature of
WebGME. It generates a notification towards a configured
2. Modeling in WebGME machine - in our case the Formula machine - at every event
of interest. For every new commit in the WebGME model
WebGME[4] is the next generation of Vanderbilt’s store, the Formula machine will receive a request to make
Generic Modeling Environment(GME) [9] providing many the model translation and constraint evaluation. After finish-
newly designed features such as web-based deployment, ing, it will store the results in a separate database so they
version control, real-time collaborative editing and prototyp- can be queried later as well. With the help of an additional
ical inheritance to add more scalability and extensibility for middleware, the Formula editor is capable of continuously
large, real world applications. WebGME is a response to the querying the results from the server and provide it to the
limitations of GME uncovered by the widespread application user - whether it is the evaluation of constraints or some
of our model-integrated computing (MIC) tools. syntax error.
Although the WebGME advanced the modeling capa- Another aspect of the
bilities of GME and provided a highly customizable and integration is that the We-
meta-programmable framework; it still lacks an expressive bGME meta-model repre-
and easy-to-use platform for well-formedness checking. In sented as a Formula do-
WebGME, the models could be checked with script defined main is always available
in JavaScript language, but for model-developers and engi- in a synchronous man-
neers its use is cumbersome and lacks expressiveness which ner. Modifications to the
makes it hard to maintain. Elimination of this gap was one meta-model are immedi-
of the key motivations for the deeper integration between ately reflected as Formula
WebGME and Formula. domain specifications and
Figure 1: Integration Archi-
tecture view of the WebGME can be extended with For-
3. Formal Specification of Modeling Lan- Formula integration mula constraints without
guages in Formula interaction with server.
However, the constraint evaluation and syntax checking
Microsoft Formula[10] is a constraint logic program- requires server interaction with reasoning in Formula engine.
ming tool developed by Jackson at Vanderbilt and later
at Microsoft Research [5]. Formula is based on algebraic 5. Semantic Integration Between WebGME
data types and first-order logic with fixed-point semantics. and Formula
It has found many application in Model-Based Engineering
such as reasoning about meta-modeling [11] or finding The cornerstone of WebGME and Formula integration
specification errors by constraints [12]. is the transformation of WebGME metamodels and models
The theoretical foundation for Formula reasoning is into Formula domain and instance representations. We ex-
based on Non-recursive Horn Domain (a well-known de- plain this translation in two steps. First, we discuss a simple
cidable subset of first-order logic) to reason about meta- example to demonstrate the two alternative representations,
model as mentioned in a previous paper[13]. Formula is also and second we provide a simplified version of the model
capable of generating automatic proofs by the help of the transformation rules.
(a) FSM Meta-model in WebGME (b) Up-Down Counter model in WebGME
model M of FiniteStateMachines {
TenMachine_attr is Attr__FSMDiagram("TenMachine").
TenMachine_ptr is Ptr__FSMDiagram(NULL).
TenMachine is FSMDiagram("TenMachine",
NULL, TenMachine_attr, TenMachine_ptr).
Initial_attr is Attr_Initial("Initial").
Initial_ptr is Ptr__Initial(NULL).
Initial is Initial("Initial",
TenMachine, Initial_attr, Initial_ptr).
End_attr is Attr_End("End").
domain FiniteStateMachines { End_ptr is Ptr__End(NULL).
Transition ::= new (id: String, End is End("End", TenMachine, End_attr, End_ptr).
parent: any FSMDiagramTYPE + {NULL}, State_One_attr is Attr__State("State One").
attributes: any Attr__Transition, State_One_ptr is Ptr__State(NULL).
pointers: any Ptr__Transition). State_One is State("State One",
Attr__Transition ::= new (guard: String, TenMachine, State_One_attr, State_One_ptr).
name: String, State_Two_attr is Attr__State("State Two").
operation: String). State_Two_ptr is Ptr__State(NULL).
Ptr__Transition ::= new (base: any FCOTYPE + {NULL}, State_Two is State("State Two",
dst: any StateBaseTYPE + {NULL}, TenMachine, State_Two_attr, State_Two_ptr).
src: any StateBaseTYPE + {NULL}). Tr_I_to_E_attr is
Attr__Transition("x=10", "Transition", "").
Initial ::= new (id: String, Tr_I_to_E_ptr is Ptr__Transition(NULL, Initial, End).
parent: any FSMDiagramTYPE + {NULL}, Tr_I_to_E is Transition("Tr_I_to_E",
attributes: any Attr__Initial, TenMachine, Tr_I_to_E_attr, Tr_I_to_E_ptr).
pointers: any Ptr__Initial). Tr_I_to_1_attr is
Attr__Initial ::= new (name: String). Attr__Transition("x>10", "Transition", "x:=x-1").
Ptr__Initial ::= new (base: any FCOTYPE + {NULL}). Tr_I_to_1_ptr is Ptr__Transition(NULL, Initial, Sate_One).
Tr_I_to_1 is Transition("Tr_I_to_1",
StateBase ::= new (id: String, TenMachine, Tr_I_to_1_attr, Tr_I_to_1_ptr).
parent: any FSMDiagramTYPE + {NULL},
attributes: any Attr__StateBase, Tr_I_to_2_attr is
pointers: any Ptr__StateBase). Attr__Transition("x<10", "Transition", "x:=x+1").
Attr__StateBase ::= new (name: String). Tr_I_to_2_ptr is Ptr__Transition(NULL, Initial, Sate_Two).
Ptr__StateBase ::= new (base: any FCOTYPE + {NULL}). Tr_I_to_2 is Transition("Tr_I_to_2",
TenMachine, Tr_I_to_2_attr, Tr_I_to_2_ptr).
State ::= new (id: String,
parent: any FSMDiagramTYPE + {NULL}, Tr_1_to_1_attr is
attributes: any Attr__State, Attr__Transition("x>10", "Transition", "x:=x-1").
pointers: any Ptr__State). Tr_1_to_1_ptr is Ptr__Transition(NULL, State_One, Sate_One).
Attr__State ::= new (name: String). Tr_1_to_1 is Transition("Tr_1_to_1",
Ptr__State ::= new (base: any FCOTYPE + {NULL}). TenMachine, Tr_1_to_1_attr, Tr_1_to_1_ptr).
End ::= new (id: String, Tr_1_to_E_attr is Attr__Transition("x=10", "Transition", "").
parent: any FSMDiagramTYPE + {NULL}, Tr_1_to_E_ptr is Ptr__Transition(NULL, State_One, End).
attributes: any Attr__End, Tr_1_to_E is Transition("Tr_1_to_E",
pointers: any Ptr__End). TenMachine, Tr_1_to_E_attr, Tr_1_to_E_ptr).
Attr__End ::= new (name: String).
Ptr__End ::= new (base: any FCOTYPE + {NULL}). Tr_2_to_2_attr is
Attr__Transition("x<10", "Transition", "x:=x+1").
FSMDiagram ::= new (id: String, Tr_2_to_2_ptr is Ptr__Transition(NULL, State_Two, Sate_Two).
parent: any {NULL}, Tr_2_to_2 is Transition("Tr_2_to_2",
attributes: any Attr__FSMDiagram, TenMachine, Tr_2_to_2_attr, Tr_2_to_2_ptr).
pointers: any Ptr__FSMDiagram).
Attr__FSMDiagram ::= new (name: String). Tr_2_to_E_attr is Attr__Transition("x=10", "Transition", "").
Ptr__FSMDiagram ::= Tr_2_to_E_ptr is Ptr__Transition(NULL, State_Two, End).
new (base: any FCOTYPE + {NULL}). Tr_2_to_E is Transition("Tr_2_to_E",
} TenMachine, Tr_2_to_E_attr, Tr_2_to_E_ptr).
}
(c) Domain in Formula (d) Model in Formula
Figure 2: Meta-Model and Model representation in WebGME and Formula
WebGME
Concept
(Meta) Formula translation
description
representation
FSMDiagram ::= new (id: String, parent: any {NULL},
attributes: any Attr__FSMDiagram,
Component pointers: any Ptr__FSMDiagram).
StateBase ::= new (...parent: any FSMDiagramTYPE + {NULL},...).
Containment
Transition ::= new (...attributes: any Attr__Transition...).
Attr__Transition ::= new (guard: String, name: String,
Attribute operation: String).
Transition ::= new (...pointers: any Ptr__Transition).
Pointer Ptr__Transition ::= new (...dst: any StateBaseTYPE + {NULL},
(one to one src: any StateBaseTYPE + {NULL}).
association)
StateBase ::= new (...).
End ::= new (...).
Inheritance StateBaseTYPE ::= StateBase + ... + End.
Figure 3: Subset of translation rules of WebGME Meta concepts into Formula domain constructs
5.1. Modeling Example discussion the formal specification of behavioral semantics.
Formula supports this by its constructs for specifying model
Finite State Machine (FSM) is used to demonstrate how transformations. The various ways to use Formula for speci-
WebGME meta-models are represented as Formula domains. fying behavioral semantics in operational or denotation style
The FSM modeling language defined as WebGME meta- is discussed in [2].
model is shown in Figure 2a. The meta-modeling language
(WebGME META) adopts a UML-like concrete syntax,
which is detailed in [4]. A specific FSM instance using 5.2. Generation of Formula Domains and Models
WebGME graphical interface is shown in Figure 2b. The
concrete syntax is configurable as expected from meta- A WebGME plugin, GenFORMULA makes the trans-
programmable modeling tools. The example shows a simple lation by using the Core API functions of WebGME. It
up-down counter that - given any x integer input value and creates a Formula domain by traversing the meta-concepts
an initial state - will check the value of input, if its value of the project. By following the rules presented in Figure 3,
is equal to ten, a transition is triggered to move from initial every Class definition is translated into three constructors
state to end state denoting the goal is reached, otherwise in Formula. Attr__Class is a tuple for the available at-
it will jump to either State One or State Two and tributes, Ptr__Class couples the pointer definitions, and
keep incrementing or decrementing x until it reaches ten and Class(id,parent,attributes,pointers) tuple
transfer to end state. The equivalent Formula representation combines the other two and adds the containment rep-
are shown in Figures 2c and 2d. resentation with the parent field. The plugin also de-
The definition on Figure 2a, still allows the creation of fines ClassTYPE set, that captures the inheritance among
malformed models. To avoid it, we need to introduce domain meta-concepts of WebGME. Inheritance among models
constraints - so the user can evade flaws like having states and model elements are kept in the base pointer defini-
with the same name or not having an initial state at all. tion. Finally, it specifies some helper constructs GMENode,
From tool design point of view, Formula has its clear advan- GMEContainment and GMEInheritance to represent
tages by allowing consistency check, model synthesis, and all nodes, their containment relation and inheritance relation.
well-formedness checking. The seamless use of Formula’s The user defined constraints are then added without modifi-
constraint language is enabled by the tight integration of the cation. This step finalizes the Formula domain. Finally the
two tools and will be described in Section 6. procedure traverses the whole containment hierarchy in the
It is important to note that we leave out from this WebGME project. For every node, it gathers the necessary
values with the help of the Core API, and translate them noSourceTr ::= new(t:TransitionTYPE).
into instances in Formula. noSourceTr(t) :- t is TransitionTYPE,k = t.parent,
k is FSMDiagramTYPE, t.pointers.src = NULL.
The resulting formula file is then processed with the help noDestinationTr ::= new(t:TransitionTYPE).
of the Formula engine to get the constraint evaluations and noDestinationTr(t) :- t is TransitionTYPE,k = t.parent,
k is FSMDiagramTYPE, t.pointers.dst = NULL.
syntax check. Being automated, the result is available after danglingTr ::= new(t:TransitionTYPE).
every change, so the user will be notified at the place of danglingTr(t) :- noSourceTr(t) ; noDestinationTr(t).
error. HasDangling :- t is TransitionTYPE, danglingTr(t).
NoDangling :- no HasDangling.
NotExactlyOneInitState :- p is FSMDiagramTYPE,
6. Constraints t is FSMDiagramTYPE, p.pointers.base = t,
count({s | s is Initial, s.parent = p}) != 1.
ExactlyOneInitState :- no NotExactlyOneInitState.
The constraints play important role in specifying the NotAtLeastOneEndState :- p is FSMDiagram,
p.parent = NULL,
structural semantics of modeling languages. They restrict k = count({s | s is End, s.parent = p}), k = 0.
structural characteristics, properties and relations in models AtLeastOneEndState :- no NotAtLeastOneEndState.
ExistsDuplicateName :- s1 is StateBaseTYPE,
such that all instances of a modeling domain are seman- s2 is StateBaseTYPE,
tically well-formed. However, the built-in constraints in s1 != s2, s1.parent = s2.parent,
WebGME’s meta-modeling language are quite limited and s1.attributes.name = s2.attributes.name.
UniqueName :- no ExistsDuplicateName.
do not support the specification and enforcement of complex reachable ::= new(x: StateBaseTYPE, y: StateBaseTYPE).
constraints. The only available solution is the traversal of reachable(x,y) :- x is StateBaseTYPE, y is StateBaseTYPE,
t is TransitionTYPE, x.parent = y.parent,
models using JavaScript plugin and check if they satisfy x.parent = t.parent,
the constraints. This method is error-prone, do not provide t.pointers.src = x, t.pointers.dst = y.
declarative representation for the constraints to reason about reachable(x,y) :- reachable(y,x).
reachable(x,z) :- reachable(x,y), reachable(y,z).
their properties (e.g. consistency) and make the use of ad- DisjointDiagram :- f is FSMDiagramTYPE,
vanced service such as model synthesis impossible. Integra- x is StateBaseTYPE,
y is StateBaseTYPE, x.parent = f, y.parent = f,
tion of WebGME with Formula eliminates these drawbacks. x != y, no reachable(x,y).
NoDisjointDiagram :- no DisjointDiagram.
6.1. Constraint Example for FSM Domain
Figure 4: Formula Constraint Example
In our examples shown in Figure 4, we collected a
few important constraints regarding the FSM domain. These
well-formedness rules are complex and cannot be expressed be cumbersome to specify large complex set of constraints
with the graphical suite of meta-modeling of WebGME. with visual blocks. Formula stands in the middle of these
For example, it is required in any FSM, that all transi- two categories of constraint specification methods by using
tions should have valid states as endpoints. The pointer con- declarative constraint specification style, but also providing
cept of WebGME doesn’t specify strict requirement regard- a reasoning engine to automatically derive the result by
ing the target so it can be NULL - as in many applications repeatedly applying rules to a set of initial constants.
that would be perfectly fine. To eliminate this gap, we define
the noSourceTr(t) and noDestinationTr(t) rules
for every transition. Then we combine them to get the
danglingTr(t) rule which can be used to finally get 6.3. Constraint Editor in WebGME Visualizer
global NoDangling constraint. Overall, many complicated
constraints can be easily written in logic programming style
Formula Language and evaluated in Formula engine. In WebGME environment, a visualizer for code editing
is implemented for users to write constraints in Formula
6.2. Benefits of Using Formula Constraints in We- syntax. The embedded constraint editor is also used to
bGME render evaluation results directly in the code by changing
the background color of the head of the constraint based on
Similar works can be found that enable adding visual the result as shown in Figure 5.
or textual constraints to general modeling. For example, Furthermore, the editor also provides syntax highlight-
the Object Constraint Language (OCL) [15], Semantics Of ing and syntax check to help users come up with correct
Business Vocabulary And Rules (SBVR) and Extensible constraints. Whenever there is a syntax error in the text, an
Visual Constraint Language (EVCL) [16] is widely used exclamation mark - left of the faulty line - will be shown and
in the UML context. Constraint Languages like OCL have by hovering over it the user can see the source of the error.
the expressiveness to describe complex constraints but they Also, the user can turn on the Formula view, that will result
lack model transformation and model completion features in a split view shown in Figure 5, where the upper portion
that are integral to our needs. Other tools like EVCL [16] with white background shows the Formula translation of
generate actual JavaScript code to check visually defined the Language domain to help the user as those definitions
constraints. Consequently, it’s not flexible enough and can should make the foundation of the constraints.
[2] G. Simko, T. Levendovszky, S. Neema, E. K. Jackson, T. bapty, P. Joe,
and J. Sztipanovits, “Foundation for model integration: Semantic
backplane,” in Proceedings of the ASME 2012 IDETC/CIE 2012.
ASME, 2012, pp. 1–8.
[3] J. Sztipanovits, T. Bapty, S. Neema, L. Howard, and E. Jackson,
OpenMETA: A Model- and Component-Based Design Tool Chain
for Cyber Physical Systems. Berlin, Heidelberg: Springer
Berlin Heidelberg, 2014, pp. 235–248. [Online]. Available:
https://doi.org/10.1007/978-3-642-54848-2 16
[4] M. Maróti, T. Kecskés, R. Kereskényi, B. Broll, P. Völgyesi,
L. Jurácz, T. Levendovszky, and Á. Lédeczi, “Next generation (meta)
Figure 5: Formula Code Editor modeling: Web-and cloud-based collaborative tool infrastructure.” in
MPM@ MoDELS, 2014, pp. 41–60.
[5] E. Jackson and J. Sztipanovits, “Formalizing the structural semantics
of domain-specific modeling languages,” Software & Systems Mod-
7. Conclusion and Future Work eling, vol. 8, no. 4, pp. 451–478, Sep 2009.
[6] E. Jackson, W. Schulte, and N. Bjorner, “Open-
This paper discusses the integration of WebGME, a world logic programs: A new foundation for formal
meta-programmable modeling tool with Formula, a formal specifications,” Tech. Rep., May 2013. [Online]. Avail-
framework and tool for specifying domain specific modeling able: https://www.microsoft.com/en-us/research/publication/open-
world-logic-programs-a-new-foundation-for-formal-specifications/
languages. The purpose of the integration has been the
construction of an advanced modeling tool that provides [7] L. De Moura and N. Bjørner, “Satisfiability modulo
theories: Introduction and applications,” Commun. ACM,
extensive model engineering services, such as graphical vol. 54, no. 9, pp. 69–77, Sep. 2011. [Online]. Available:
modeling interface, scalable model repository, web-based http://doi.acm.org/10.1145/1995376.1995394
implementation architecture and concurrent modeling as [8] E. K. Jackson, “A module system for domain-specific
well as rigorous formal foundations and tool for specifying languages,” CoRR, vol. abs/1405.4041, 2014. [Online]. Available:
modeling language semantics, model transformation seman- http://arxiv.org/abs/1405.4041
tics, consistency checking, and model synthesis. Seamless [9] A. Ledeczi, M. Maroti, A. Bakay, G. Karsai, J. Garrett, C. Thomason,
integration of these services are enablers for the safe use of G. Nordstrom, J. Sprinkle, and P. Volgyesi, “The generic modeling en-
domain specific modeling language (DSML) technologies vironment,” in Workshop on Intelligent Signal Processing, Budapest,
Hungary, vol. 17, 2001, p. 1.
in application domains, where heterogeneous and changing
modeling domains need to be integrated and evolved. [10] E. K. Jackson and W. Schulte, “Formula 2.0: A language for formal
specifications,” in Unifying Theories of Programming and Formal
As described in the paper, the current level of integration Engineering Methods. Springer, 2013, pp. 156–206.
focused on automated and fully synchronized generation [11] E. K. Jackson, T. Levendovszky, and D. Balasubramanian, “Reason-
of Formula representation from WebGME models. In the ing about metamodeling with formal specifications and automatic
next step we will address the opposite direction: the auto- proofs,” in International Conference on Model Driven Engineering
generation of WebGME plugins from Formula specifications Languages and Systems. Springer, 2011, pp. 653–667.
for constraint checking and model transformation. The pri- [12] E. K. Jackson, W. Schulte, and N. Bjørner, “Detecting specification
mary goal is to preserve the advantages of the Formula- errors in declarative languages with constraints,” in Model Driven
based declarative specification of model transformations, Engineering Languages and Systems - 15th International Conference,
MODELS 2012, Innsbruck, Austria, September 30-October 5, 2012.
such as conciseness, semantic precision and preservation of Proceedings, 2012, pp. 399–414.
domain invariants after the transformation - but without los-
[13] E. K. Jackson and J. Sztipanovits, “Constructive techniques for meta-
ing the efficiency of an imperative language implementation, and model-level reasoning,” in MoDELS, vol. 7. Springer, 2007, pp.
which is particularly important for large models. 405–419.
[14] L. de Moura and N. Bjørner, Z3: An Efficient SMT Solver. Berlin,
Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340.
References
[15] M. Richters and M. Gogolla, “On formalizing the uml object con-
straint language ocl,” in International Conference on Conceptual
[1] J. Sztipanovits, T. Bapty, S. Neema, X. Koutsoukos, and E. Jackson, Modeling. Springer, 1998, pp. 449–464.
“Design tool chain for cyber-physical systems: Lessons learned,” in [16] B. Broll and Á. Lédeczi, “Extensible visual constraint language,” in
Proceedings of DAC15. IEEE, 2015, pp. 1–8. Proceedings of the Workshop on Domain-Specific Modeling. ACM,
2015, pp. 63–70.