Modeling languages are often used for designing complex systems. To simplify the modeling process, system designers can use dedicated modeling frameworks, which provide all necessary tools and services in order to facilitate system development and decrease costs by eliminating errors early at design time. Nowadays, the emergence of heterogeneous engineering domains has led to design flows that span multiple Domain Specific Modeling Languages (DSMLs). As a result, analyzing system behavior requires the semantic integration of modeling domains through languages that are supported by formal semantics, are easily adaptable, and provide scalable and eficient correctness-checking services. To this end, we present a framework that provides heterogeneous modeling services that are based on the combination of two formalisms, 1) logics and 2) graphs. On one hand, we use the FORMULA tool to formalize the semantics of DSMLs and provide a common integrated semantic background. On the other hand, we use graph queries specified in Gremlin to employ eficient query and model analysis services. Our framework ofers a complete model-based engineering solution that includes graphical modeling and version control services, which are integrated into a web-based collaborative environment.
Modeling frameworks are key enables of model-driven engineering.
They provide necessary tools and services to system designers in
order to facilitate system development and eliminate errors early
at design time. The adoption of model-engineering methods in
new cross-disciplinary fields such as Cyber-Physical Systems (CPS)
brings new challenges in modeling frameworks [
Analyzing system structure and behavior, and pursuing crossdomain trade-ofs requires the semantic integration of modeling domains. To do that, modeling frameworks must be extensible and adaptable to allow modeling in diferent DSMLs in a way that their semantics are captured in a formal manner to allow rigorously specifying model transformations. Additionally, modeling frameworks are called to provide heterogeneous services that include 1) engineering services for graphical modeling, metamodeling, version-control, etc.; 2) a common integrated semantic background represented in a formal language; 3) eficient and scalable correctness-checking mechanisms.
On one hand, even though logic-based languages [
Our work is based on previous preliminary work presented in [
Our web-based, open source1 framework provides a set of engineering services. It allows real-time collaboration between multiple developers. Project changes are committed and versioned, which enables branching, merging and viewing the history of a project.
The organization of the paper is as follows. Section 2 provides background information. Section 3 presents the theoretical foundation of our approach, which is based on labeled and typed graphs and first-order logic conformance conditions. Section 4 and 5 presents the translation of the graphs and conformance conditions in FORMULA and Gremlin languages, respectively. Section 6 discusses
the translation of specific metamodel and model instances in FORMULA and Gremlin, while also provides implementation details. Section 7 concludes the paper. 2
There exists a plethora of metamodeling languages and tools; Kern
et al. provide a comparative analysis [
A project in WebGME is a collection of metamodels and models. When a user creates a new project, it contains the First Class Object (FCO), which comprises the root of the inheritance hierarchy. FCO has a fixed attribute name of type String, which is inherited by all other objects. Additionally, objects may contain several other attributes. An Attribute defines a property of an object, which can be typed as String, Integer, Float, Enumeration, etc.
Relations between objects include Pointer, Set membership, Mixin, Inheritance, and Containment. Inheritance and Mixin are similar to UML inheritance and UML realization, respectively. Inheritance and Mixin are both associated with FCO by: 1) a strong containment for their “sources”, i.e., baseOf, interfaceOf and 2) a weak association for their “destinations”, i.e., instanceOf, implementationOf. The strong association denotes the fact that if the base (resp. interface) of an inheritance (resp. mixin) relation is deleted, the inheritance (resp. mixin) relation is deleted as well.
Furthermore, the Containment and Pointer are similar to a UML containment and UML binary directed named association, respectively. In the same manner, Set membership is similar to a UML directed named association between an instance of an owner object type and an unordered set of member objects of another type. Set membership can be considered as a collection of pointers. For all three relations their source is associated with FCO through a strong containment association and their destination is associated with FCO through a weak association. All three relations have additional user-defined properties. Set membership and Pointer include property name of type String. Additionally, Containment and Set membership include propery md of type UnlimitedNatural that denotes the destination multiplicity of the child. The source multiplicities of Containment and Set membership are always 1. Notice that Inheritance, Pointer, and Mixin do not have the md property because the multiplicities of their instances are not user defined but fixed. The source multiplicities of each Inheritance, Pointer, and Mixin instance are all equal to 1. The destination multiplicities of each Inheritance, Pointer, and Mixin instance are equal to ∗, 1, and ∗, respectively.
Before we provide the formal definitions let us first give the intuition
behind our approach. We aim at describing the semantics of a
metamodeling language with an abstract, high-level language that
enables easy reasoning. Graphs provide such an abstract language
and have been studied extensively for representing metamodels
and models [
We define labeled graphs, which are directed graphs edge-labeled with names and multiplicities, to specify (meta-)metamodels.
Definition 3.1. (Labeled graph). A labeled graph is a quadruple L = ⟨V , E, λv , λe ⟩, with a set of vertices V , a set of directed edges E ⊆ V 2, and labeling functions 1) λv : V 7→ N and 2) λe : E 7→ I × N × I , where N is a set of names and I is a set of intervals of the form = N2 ∪ N × {∗}.
For ease of presentation, we define the notation ∀e ∈ E, ∀v ∈ V : • src(e) ∈ V denotes the source vertex of e, • dst (e) ∈ V denotes the destination vertex of e, • ms(e) ∈ I denotes the source multiplicity of e, • md(e) ∈ I denotes the destination multiplicity of e, • n(e), n(v) ∈ N denote the names of e and v, respectively. We require the following uniqueness conditions: • ∀v1, v2 ∈ V , if n(v1) = n(v2) then v1 = v2, • ∀e1, e2 ∈ E, if src(e1) = src(e2), n(e1) = n(e2), and dst (e1) = dst (e2) then e1 = e2 with source and destination multiplicities ms(e1) ∪ ms(e2) and md(e1) ∪ md(e2), respectively. Next, we define Model graphs, which we use to specify models.
Definition 3.2. (Model graph). A model graph is a Labeled graph
M = ⟨V , E, λv , λe ⟩ such that for all edges e ∈ E, ms(e) = md(e) =
[
Typed graphs have been previously studied by the model
transformation community [
Definition 3.3. (Typed graph). A typed graph is a quadruple T = ⟨L, M, τv , τe ⟩ where L and M are labeled and model graphs, respectively; τv : VM ∪ VL 7→ 2VL , τe : EM 7→ EL
Definition 3.3 describes the inheritance relation 1) between vertices of the model or labeled graph and vertices of the labeled graph and 2) edges of the model graph and edges of the labeled graph. The L graph specifies a metamodel with node types and edge types. The M graph is an instance model referencing these types. The type(s) of each vertex v and edge e, of M, is τv (v) and τe (e), respectively.
Definition 3.4. (Model conformance). For a typed graph T = ⟨L, M, τv , τe ⟩, a model, represented by the model graph M, conforms to a metamodel, represented by the labeled directed graph L if a set of conditions hold: n conforms(T ) = Û (i), i=1 where (i) represents logical formulae that are either 1) generic and automatically derived from T or 2) application-specific and thus, user-defined. 3.1
For a typed graph T = ⟨L, M, τv , τe ⟩, we derive the following conformance conditions:
(1) ≜ ∀vM ∈ VM , ∃vL ∈ VL : vL ∈ τv (vM ) .
Meaning of (1): for each vertex in the model graph there exists a vertex in the labeled graph that characterizes its type. (2) ≜ ∀eM ∈ EM , ∃eL ∈ EL :
τe (eM ) = eL ∧ src(eL) ∈ τv (src(eM )) .
Meaning of (2): for each edge eM in the model graph, there exists an edge eL in the labeled graph, such that eM is of type eL and the source vertex of eM is of type of the source vertex of eL. (3) ≜ ∀eM ∈ EM , ∃eL ∈ EL :
τe (eM ) = eL ∧ dst(eL) ∈ τv (dst(eM )) .
Meaning of (3): for each edge eM in the model graph, there exists an edge eL in the labeled graph, such that eM is of type eL and the destination vertex of eM is of type of the destination vertex of eL. (4) ≜ ∀vA ∈ VM , ∀eL ∈ EL, ∀VMS ⊆ VM , ∃vB ∈ VMS , ∀eM ∈ EM : src(eL) < τv (vA) ∨ src(eM ) , vA ∨
dst(eM ) , vB ∨ τe (eM ) , eL ∨ |VMS | ∈ md(eL).
Meaning of (4): each vertex vA of the model graph is correctly connected to a subset of the vertices of the model graph according to the destination multiplicities of all the edges of the labeled graph that are connected to the vertex that corresponds to the type of vA. (5) ≜ ∀eL ∈ EL, ∀vM ∈ VM , ∃eM ∈ EM : src(eL) < τv (vM ) ∨ 0 ∈ md(eL) ∨ (src(eM ) = vM ∧ eL = τe (eM )) .
Meaning of (5): for each edge eL of the labeled graph there exists at least an edge eM , which is an instance of eL in the model graph if the corresponding destination cardinality of eL does not include zero and there exists at least a node vM such that src(eM ) = vM . (6) ≜ ∀vA ∈ VM , ∀eL ∈ EL, ∀VMS ⊆ VM , ∃vB ∈ VMS , ∀eM ∈ EM : src(eL) < τv (vA) ∨ src(eM ) , vB ∨
dst(eM ) , vA ∨ τe (eM ) , eL ∨ |VMS | ∈ ms(eL).
Meaning of (6): each vertex vA of the model graph is correctly connected to a subset of the vertices of the model graph according to the source multiplicities of all the edges of the labeled graph that are connected to the vertex that corresponds to the type of vA. (7) ≜ ∀eL ∈ EL, ∀vM ∈ VM , ∃eM ∈ EM : dst(eL) < τv (vM ) ∨ ∧ 0 ∈ ms(eL) ∨ (dst(eM ) = vM ∧ eL = τe (eM )) .
Meaning of (7): for each edge eL of the labeled graph there exists at least an edge eM , which is an instance of eL in the model graph if the corresponding source cardinality of eL does not include zero and there exists at least a node vM such that dst(eM ) = vM .
FORMULA (Formal Modeling Using Logic Programming and
Analysis) [
Next, we show the equivalent specifications of a labeled, model and typed graph in FORMULA. The complete specification is wrapped in a domain block, which delimits a domain-specific abstraction.
The specification of a labeled graph is as follows: MetaNode ::= new ( name : String ).
MetaEdge ::= new ( name : String , src : MetaNode ,
dst : MetaNode , ms: Multiplicity , md: Multiplicity ). Multiplicity ::= new ( low : Natural , high : Natural + {"*" }).
FORMULA supports algebraic data types and these are used to encode user defined relations. For example, the first line of the labeled graph specification declares a data type constructor MetaNode() for instantiating meta-level nodes (VL). This constructor produces MetaNode instances that have a field called name of type String.
Similarly, the specification of a model graph is as follows: Node ::= new ( name : String , type : MetaNode ).
Edge ::= new ( name : String , type : MetaEdge ,
src : Node , dst : Node ).
For simplification, we have omitted the source and destination multiplicities of a model graph since they are always equal to 1.
The inheritance relation between the nodes and edges of the labeled and model graphs is defined through the typed graph. We use the following transitive closure relation to specify node inheritance: NodeInheritance ::= new ( base : MetaNode ,
instance : MetaNode + Node ).
NodeInstanceOf ::= ( MetaNode , MetaNode + Node ). NodeInstanceOf (b,i) :- NodeInheritance (b,i) ;
NodeInheritance (b,m), NodeInstanceOf (m,i).
Edge inheritance can be directly checked through the type argument of each Edge. We additionally define the WrongMultiplicity condition, which follows directly from the labeled graph definition. WrongMult :- Multiplicity (low , high ), high !="*", low > high . 4.1
To generate the conditions presented in Section 3.1 in FORMULA, for a typed graph T = ⟨L, M, τv , τe ⟩, we take the negation of the formulas. Due to space limitations we show the equivalent specification for a subset of conditions. The negation of (2) is translated to FORMULA as follows: not2 :- e is Edge , no {m | m is MetaEdge ,
m = e.type , NodeInstanceOf (m.src ,e. src )}.
The negation of (4) is translated to FORMULA as the conjunction of (not4a) and (not4b), which are defined as follows: not4a :- n is Node , m is MetaEdge ,
NodeInstanceOf (m.src ,n), count ({s|s is Node , e is Edge (_,m,n,s )}) < m.md. low . not4b :- n is Node , m is MetaEdge ,
NodeInstanceOf (m.src ,n), m.md. high != "*", count ({s|s is Node , e is Edge (_,m,n,s )}) > m.md. high .
Graph databases use graph structures to represent and store data.
They allow to retrieve data of complex hierarchical structures in a
simple and fast manner, in comparison with relational databases.
We use the Gremlin traversal machine and language [
Similarly, we generate the conditions presented in Section 3.1 as Gremlin queries. Due to space limitations we show the equivalent specifications for conditions (2) and (4): not2 = g.V (). has ('class ','Edge '). not ( match (__.as('s'). out ('type '). out ('src '). as('a'), __.as('s'). out ('src '). out ('type '). as('b') . where ('b',eq('a')))). hasNext (); Query not2 uses the match step where multiple traversals can be checked. For every Edge vertex it checks whether there is no match based first on type and second on src edges, and continues by checking for no match in the opposite order, i.e., first on src and second on type. Similarly, queries not4a, not4b are as follows: not4a = g.V (). has ('class ',' MetaEdge '). match (__.as('m'). in('type '). groupCount (). by( out ('src ')). order ( local ). by( values , incr ). select ( values ). limit (local ,1). as('actual '),__.as('m'). outE ('src '). properties ('min '). value (). as('allowed '). where ('allowed ',gt('actual ')).
hasNext (); not4b = g.V (). has ('class ',' MetaEdge '). where ( outE ('src '). has ('max ')). match (__.as('m'). in('type '). groupCount (). by( out ('src ')). order ( local ). by( values , decr ). select ( values ). limit (local ,1). as('actual '),__.as('m'). outE ('src '). properties ('max '). value (). as('allowed ').
where ('allowed ',gt('actual ')). hasNext ();
We apply our framework on the DesignBIP tool [
The DesignBIP metamodel is partly shown in Figure 3. A Project contains zero or more ComponentType objects. Each ComponentType contains at least one StateBase, at least one TransitionBase, and zero or more Guard instances. A ComponentType contains exactly one InitialState. StateBase is an abstract object, meaning that it can only be instantiated as InitialState or State. Similarly, TransitionBase is also an abstract object. The TransitionBase object points to StateBase through the src and dst pointers.
6.1.1 DesignBIP metamodel in FORMULA. Our dedicated WebGMEbased FORMULA code editor parses the MetaNodes and then automatically creates the corresponding FORMULA rules. The MetaNodes are specified in FORMULA as shown in the second row of Figure 2. Next, the plugin parses the relations specified in the metamodel and their multiplicities and creates multiplicity rules, e.g.,: starMultiplicity is Multiplicity (0,"*"). exactlyOneMultiplicity is Multiplicity (1, 1).
As you can see in Figure 3, WebGME concepts have attributes of type String and asset. The types of these attributes are modeled as MetaNodes in the labeled graph, while the containment of an attribute by a concept is modeled as a MetaEdge, as follows: String is MetaNode (" String "). metaAttr1 is MetaEdge (" guardName ", TransitionBase , String , starMultiplicity , exactlyOneMultiplicity )
Next, the plugin creates FORMULA rules for the additional MetaEdge instances. Pointers are specified as shown in the fourth row of Figure 2. Similarly, containments are specified as shown in the second row of Figure 2. Set memberships are specified as shown in the sixth row of Figure 2. Inheritance is specified with the constructor NodeInheritance, as shown in the last row of Figure 2.
6.1.2 DesignBIP metamodel in Gremlin. To generate the graph database queries, we have created a second translator. The equivalent Gremlin specifications for the WebGME concepts and relations are shown in Figure 2. A notable diference between the FORMULA and Gremlin specifications is that the cardinalities are defined in the form of min and max properties of edges of the graph. Additionally, the unbounded cardinality intervals are simply represented by not defining the max property. Another diference is the type edges. They represent the NodeInstanceOf relationship which means that every base of a MetaNode is directly connected and we do not have to make long traversals to get the information.
Let us now consider the DesignBIP FSM model shown in Figure 4.
The FSM has four states off, on, done, wait. The states are conSpontaneousTransition, and InternalTransition (Figure 3). Transitions on, off, and finished, illustrated by continuous lines, are of type EnforceableTransition. Transition end, illustrated
S p o n t a n e o u s T r a n s i t i o n 4 e n d , m o d e l A t t r 1 ) nected with transitions that are of three types: EnforceableTransition, The containment relation between the !finished attribute and the
6.2.2 DesignBIP Model in Gremlin. Next, we present portions of the generated Gremlin specification for the model of Figure 4.
For instance, the on state is specified in Gremlin as follows.
State2on = graph . addVertex ('class ','Node ', 'name ','s2 ').
State2on . addEdge ('type ',State ).
State2on . addEdge ('type ', StateBase ).
State2on . addEdge ('type ',FCO ).
The translation take cares of realizing the transitive closure of the FORMULA definition of NodeInheritance. Similarly, the specification of the guardname attribute in Gremlin is as follows: modelAttr1 . addEdge ('type ',String ). modelAttr1HasGuard = graph . addVertex ('class ','Edge ', ' guardName ','_t4 '). modelAttr1HasGuard . addEdge ('src ', Transition4end ). modelAttr1HasGuard . addEdge ('dst ', modelAttr1 ). modelAttr1HasGuard . addEdge ('type ', metaAttr1 ).
The specification of relations, for example the pointer relation between state off and enforceable transition on, is as follows: modelPointer1 = graph . addVertex ('class ','Edge ','name ','p1 '). modelPointer1 . addEdge ('type ', metaPointer1src ). metaPointer1 . addEdge ('src ', EnforceableTransition3on ). metaPointer1 . addEdge ('dst ', InitialState1off ).
To extend and allow the integration of these diferent representations, we developed two dedicated code editors (the FORMULA one can be seen in Figure 5) to the WebGME. Both editors have two types of content: 1) read-only content that is generated from the visually created meta-model and model and 2) a user-defined portion where the user can add any additional constraint. The read-only part can only be altered by using the graphical model or meta-model editor of the WebGME. The code-editors also provide ‘check-buttons’ to run an on-demand evaluation of the given model. This is done through dedicated plugins that communicate with the integrated FORMULA and Gremlin console engines to check the well-formedness of the model. Though we have not completed any extensive performance testing between the two representations, our first tests show that conformance checking in Gremlin is more scalable and eficient than a similar task in FORMULA. With the BIP domain (having 49 MetaNodes and 39 MetaEdges) and a relatively large model (4082 Nodes and 12670 Edges), the FORMULA execution took 113s while the Gremlin remained under 1s.
This paper discusses the integration of WebGME with 1) FORMULA a formal framework for specifying DSMLs and 2) Gremlin an graphbased query language. The purpose of the integration has been the construction of an advanced modeling tool that provides heterogeneous services. In particular, our framework provides: 1) extensive model engineering services, such as graphical modeling interfaces, scalable model repositories, a web-based architecture that allows collaborative modeling which is backed-up by version control services; 2) rigorous formal foundations through the integration of the FORMULA language that can be used for specifying language semantics, model transformation rules, automated consistency checking, and model synthesis; 3) eficient Gremlin queries that can be used for checking model conformance, clustering, and data analysis of large and complex systems. In the future, we will use FORMULA for model synthesis and proof generation.
This research was supported by the National Science Foundation under award CNS-1521617.