

\section{Introduction}



Modeling languages are often used for designing complex systems. Using dedicated design studios allows increasing the understandability and usability of modeling languages, as well as decreasing development costs by eliminating errors at design time.
Design studio components can be organized in the following three categories: 1)~\emph{semantic integration}, 2)~\emph{service integration}, and 3)~\emph{tool integration}. Semantic integration components comprise the domain of the modeling language, \ie its \emph{metamodel} that explicitly specifies the building blocks of the language and their relations. Service integration components include dedicated model editors, code editors, and GUI/Visualization components for modeling and simulating results. Additionally, service integration components include model transformation and code generation services, model repositories, and version control services. Finally, tool integration components consist in integrated tools such as run-times and verification tools.

Figure~\ref{fig:studioFlow} shows the main steps of the workflow of a design studio. Initially, models are designed using dedicated model editors. Optionally, design patterns stored in model repositories may be used to simplify the modeling process. 
Next, the checking loop starts (step 1), where the models are checked for conformance. If the required conformance conditions are not satisfied by the model, the checking mechanism must point back to the problematic nodes of the model in the model editor and inform the developer of the inconsistency causes to facilitate model refinement. Finally, when the conformance conditions are satisfied (step 2), the refined models may be analyzed and/or executed (step 3) by using integrated, into the design studio, third party tools. The output of the tools is then collected and sent back to the model editors (step 4) for visualization of analysis or execution results.

\begin{figure} [t]
  \centering
  \includegraphics[scale=0.35]{WorkFlow.pdf}
  \caption{Main design studio components and work-flow}
  \label{fig:studioFlow}
 
\end{figure}


We present the DesignBIP studio for modeling and generating systems with the BIP~\cite{Basu11-RCBSD} framework. BIP comprises a language with rigorous operational semantics and a dedicated tool-set including code generators, run-time support tools, \ie BIP engines, and verification tools~\cite{dfinder, esst4bip}. Depending on the application domain, BIP offers several compilation chains, targeting different execution platforms and programming languages such as C++~\cite{Basu11-RCBSD} Java~\cite{SPE:SPE2495} Haskell, and Scala~\cite{edelmannfunctional}.

The specification of models in the BIP framework is done by using the BIP language in a textual manner~\cite{BIPGrammar} without offering any dedicated code editors. Thus, developing large systems with the BIP toolset can be challenging and error prone. In DesignBIP we have opted for a graphical language to enhance readability and easiness of expression. DesignBIP offers a complete modeling solution, in which we have integrated the tools offered by JavaBIP, the Java-based implementation of BIP~\cite{SPE:SPE2495}. Relying on the observation that systems are usually built from multiple instances of the same component type, we propose a parameterized graphical language for BIP that enhances scalability and reduces the model size.

DesignBIP is a web-based, collaborative, version controlled design studio based on~WebGME~\cite{maroti2014next}. DesignBIP allows real-time collaboration between multiple developers. Project changes are committed and versioned, which enables branching, merging and viewing the history of a project. DesignBIP\footnote{https://cps-vo.org/group/BIP} is easily accessed through a web interface and is open source\footnote{https://github.com/anmavrid/DesignBIP}.
Our contributions are as follows:
\begin{compactitem}
\item We extend \emph{architecture diagrams}~\cite{MavridouBBS16}, a graphical parameterized language, to accommodate the specification of BIP parameterized models.
\item We prove a set of necessary and sufficient conditions for checking the encodability of parameterized BIP graphical models into logical formulas.
\item We study the model transformation from graphical models to logical formulas and develop code generation plugins.
\item We develop dedicated BIP model editors, code editors, and model repositories.
\item We integrate the JavaBIP engine and provide visualization of its output.
\end{compactitem}

 


\emph{Paper organization:}
Section 2 describes the BIP language. Section 3 describes the parameterized graphical language of DesignBIP. Section 4 describes  service integration components, \ie model and code editors, model repositories, and code generators. Section 5 describes the integration with the JavaBIP engine.
Section 6 discusses related work. Section 7 discusses concluding remarks and future work. 


\section{The BIP Language}
\label{secn:bip}

Component behavior in BIP is described by Labeled Transition Systems (LTS). 
LTS transitions are of three types: \emph{enforceable}, \emph{spontaneous}, and \emph{internal}\footnote{JavaBIP includes all three, whereas BIP1 and BIP2 include the enforceable and internal types.}. 
Enforceable transitions are handled by the BIP-engine and are labeled with \emph{ports}. Ports form the interface of a component and are used to define interactions with other components. 
 Spontaneous transitions take into account changes in the environment and, thus, they are not handled by the BIP-engine but rather executed after detection of external events. Finally, internal transitions allow a component to update its state based on internal information.
 
 \begin{figure*} [t]
\centering
\hfill
\begin{subfigure}[b]{0.23\textwidth}
  \begin{tikzpicture}[shorten >=1pt,node distance=.7cm,>=stealth'
      ,initial text=
      ,every state/.style={draw=green,thick}
      ,group/.style = {draw=darkgreen, thin, rectangle, minimum width=2.5cm}
      ,port/.style = {font=\small, minimum size=5mm}
      ,legend/.style = {font=\bf}
    ]

    \node[port] (rndv2) {synchron};
    \node[port, node distance=1.5cm] (brdc2) [right of=rndv2]{trigger};
    \draw [style=-*, thick, darkgreen] ($(rndv2.north)+(0,.8cm)$) -| (rndv2.north);
    \draw [style=-triangle 45 reversed, thick, darkgreen] ($(brdc2.north)+(0,.8cm)$) -| (brdc2.north);
  \end{tikzpicture}
  \caption{Port attributes}
  \label{fig:attributes}
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.18\textwidth}
  \centering
 
 
  \begin{tikzpicture}[shorten >=1pt,node distance=.7cm,>=stealth'
      ,initial text=
      ,every state/.style={draw=darkgreen,thick}
      ,group/.style = {draw=darkgreen,thin,rectangle, minimum width=2.5cm}
      ,port/.style = {font=\small, minimum size=5mm}
      ,legend/.style = {font=\bf}
    ]

   
    \node[port] (h){};

    \node[port, node distance=.3cm] (ar) [left of=h]{$s$};
    \node[port, node distance=.3cm] (br) [right of=h]{$r_1$};
    \node[port, node distance=.6cm] (cr) [right of=br]{$r_2$};
    \draw [style=-*, thick, darkgreen]($(h.west)+(0,1cm)$)-|(ar.north);
    \draw [style=-*, thick, darkgreen] ($(h.west)+(0,1cm)$) -|(br.north);
    \draw [style=-*, thick, darkgreen] ($(h.west)+(0,1cm)$) -|(cr.north);

    \node[port, node distance=1em] (rndv) [below of=br]{$\{sr_1r_2\}$};
  \end{tikzpicture
  \caption{Rendezvous}
  \label{fig:rendezvous}
\end{subfigure}
\hfill
\begin{subfigure}[b]{0.18\textwidth}
 
 
  \begin{tikzpicture}[shorten >=1pt,node distance=.7cm,>=stealth'
      ,initial text=
      ,every state/.style={draw=darkgreen,thick}
      ,group/.style = {draw=darkgreen,thin,rectangle, minimum width=2.5cm}
      ,port/.style = {font=\small, minimum size=5mm}
      ,legend/.style = {font=\bf}
    ]

    \node[port] (h2){};
    \node[port, node distance=.3cm] (abr) [left of=h2]{$s$};
    \node[port, node distance=.3cm] (bbr) [right of=h2]{$r_1$};
    \node[port, node distance=.6cm] (cbr) [right of=bbr]{$r_2$};
    \draw [style=-triangle 45 reversed, thick, darkgreen]($(h2.west)+(0,1cm)$)-|(abr.north);
    \draw [style=-*, thick, darkgreen] ($(h2.west)+(0,1cm)$) -|(bbr.north);
    \draw [style=-*, thick, darkgreen] ($(h2.west)+(0,1cm)$) -|(cbr.north);

    \node[port, node distance=1em] (brdc) [below of=bbr]{$\{s, sr_1, sr_2, sr_1r_2\}$};
  \end{tikzpicture
  \caption{Broadcast}
  \label{fig:broadcast}
\end{subfigure}
\hspace*{\fill}

\bigskip
\begin{subfigure}[b]{0.62\textwidth}
 
 
  \begin{tikzpicture}[shorten >=1pt,node distance=.7cm,>=stealth'
      ,initial text=
      ,every state/.style={draw=darkgreen,thick}
      ,group/.style = {draw=darkgreen,thin,rectangle, minimum width=2.5cm}
      ,port/.style = {font=\small, minimum size=5mm}
      ,legend/.style = {font=\bf}
    ]

    \node[port] (start) {};
    \node[port, node distance=1.5cm](h4)[left of=start]{};

    \node[port, node distance=1cm] (ab) [below of=h4] {$r_1$};
    \node[port, node distance=1cm] (ac) [right of=ab]{$r_2$};
    \node[port, node distance=1cm] (aa) [left of=ab]{$s$};

    \node[port, node distance=1.4cm] (leg4) [below of=h4] {$\{r_1r_2, sr_1r_2\}$};


    \draw [style=-*, thick, darkgreen] ($(h4.south)+(0,.1cm)$) -- ++(right:.5cm) -| (ac.north);
    \draw [style=-*, thick, darkgreen]  ($(h4.south)+(0,.1cm)$) -| (ab.north);
    \draw [style=-triangle 45 reversed, thick, darkgreen] ($(h4.south)+(0,.5cm)$) -- ++(right:.2cm) -| ($(h4.south)+(+.5,0cm)$);
    \draw [style=-*, thick, darkgreen]  ($(h4.south)+(0,.5cm)$) -| (aa.north);

   

    \node[port, node distance=1.5cm](baa) [right of=start]{};
    \node[port, node distance=1cm] (bb) [below of=baa]{$r_1$};
    \node[port, node distance=1cm] (bc) [right of=bb]{$r_2$};
    \node[port, node distance=1cm] (ba) [left of=bb]{$s$};


    \draw [style=-*, thick, darkgreen] ($(baa.south)+(0,.1cm)$) -- ++(right:.5cm) -| (bc.north);
    \draw [style=-*, thick, darkgreen]  ($(baa.south)+(0,.1cm)$) -| (bb.north);
    \draw [style=-*, thick, darkgreen] ($(baa.south)+(0,.5cm)$) -- ++(right:.2cm) -| ($(baa.south)+(+.5,0cm)$);
    \draw [style=-triangle 45 reversed, thick, darkgreen]  ($(baa.south)+(0,.5cm)$) -| (ba.north);

    \node[port, node distance=1.4cm] (leg5) [below of=baa] {$\{s, sr_1r_2\}$};

   

    \node[port, node distance=4.5cm](caa) [right of=start]{};
    \node[port, node distance=1cm] (cb) [below of=caa]{$r_1$};
    \node[port, node distance=1cm] (cc) [right of=cb]{$r_2$};
    \node[port, node distance=1cm] (ca) [left of=cb]{$s$};

    \draw [style=-*, thick, darkgreen] ($(caa.south)+(0,.1cm)$) -- ++(right:.5cm) -| (cc.north);
    \draw [style=-triangle 45 reversed, thick, darkgreen]  ($(caa.south)+(0,.1cm)$) -| (cb.north);
    \draw [style=-*, thick, darkgreen] ($(caa.south)+(0,.5cm)$) -- ++(right:.2cm) -| ($(caa.south)+(+.5,0cm)$);
    \draw [style=-triangle 45 reversed, thick, darkgreen]  ($(caa.south)+(0,.5cm)$) -| (ca.north);

    \node[port, node distance=1.4cm] (leg6) [below of=caa] {$\{s, sr_1, sr_1r_2\}$};
  \end{tikzpicture
  \caption{Hierarchical connectors}
  \label{fig:hierarchical}
\end{subfigure}
\caption{BIP connectors and their associated interaction sets}
\label{fig:connectors}
  
\end{figure*}
 
An \emph{interaction} in BIP is a non-empty set of ports that defines allowed synchronization of actions among components. BIP interactions represent a clean, abstract concept of \emph{architecture} which is separated from component behavior.
Interaction models can be represented in many equivalent ways. Among these are connectors~\cite{BliSif07-acp-emsoft} and Boolean formulas~\cite{bliudze2010causal} on variables representing port participation in interactions. Connectors are most appropriate for graphical design and interaction representation, whereas Boolean formulas are most appropriate for efficient encoding and manipulation by the BIP-engine.

BIP connectors contain ports, which form their interface. Each port of a connector has an attribute \emph{trigger} (represented by a triangle, \fig{attributes}) or \emph{synchron} (represented by a bullet, \fig{attributes}). 
Given a connector involving a set of ports $\{p_1,...,p_n\}$, the set of its interactions is defined as follows: an interaction is any non-empty subset of $\{p_1,...,p_n\}$ which contains some port that is a trigger (\fig{broadcast}); otherwise, (if all ports are synchrons) the only possible interaction is the maximal one that is, $\{p_1,...,p_n\}$ (\fig{rendezvous}). 
The same principle is recursively extended to hierarchical connectors, where one interaction from each subconnector is used to
form an allowed interaction according to the synchron/trigger typing of the connector nodes (\fig{hierarchical}). 

Alternatively, \emph{interaction logic} can be used to define interaction models.
The propositional interaction logic (PIL) is defined by the grammar:
\begin{align*}
\phi ::= \ensuremath{\mathit{true}}\ |\ p\ |\ \compi \phi\ |\ \phi \vee \phi
\,,
\end{align*}
with any $p \in P$, where $P$ is the set of ports of a BIP system. Conjunction  is defined as follows:  $\phi_1 \wedge \phi_2 \bydef{=} \compi{(\compi{\phi_1} \vee \compi{\phi_2})}$.
To simplify notation, we omit conjunction in monomials, \eg writing $sr_1r_2$ instead of $s \wedge r_1 \wedge r_2$.
Let $\gamma$ be a non-empty set of interactions. The meaning of a PIL formula $\phi$ is defined by the satisfaction relation: $\gamma \models \phi$ iff for all $a \in \gamma$, $\phi$ evaluates to $\ensuremath{\mathit{true}}$ for the valuation induced by $a$: $p=\ensuremath{\mathit{true}}$, for all $p\in a$ and $p=\ensuremath{\mathit{false}}$, for all $p \not\in a$.

Consider the \emph{Star architecture} shown in \fig{starPIL}, where a single component $C$ acts as the center, and three other components $S_1,\ S_2,\ S_3$ communicate with the center through binary rendezvous connector
. Component $C$ has a single port $p$ and all other components have a single port $q_i\ (i=1,2,3)$. The corresponding PIL formula is: $p q_1\compi{q_2}\compi{q_3} \vee p \compi{q_1} q_2\compi{q_3} \vee p \compi{q_1} \compi{q_2} q_3$.

\begin{figure} [t]
  \centering
  \includegraphics[scale=4]{starPIL.png}
  \caption{A Star architecture}
  \label{fig:starPIL}
 
\end{figure}

To define interactions independently from the number of component instances, PIL can be extended with quantification over components~\cite{dybip}. This extension is particularly useful because, in practice, systems are built from multiple component instances of the same component type.
Similarly to~\cite{dybip}, JavaBIP uses a macro-notation based on FOIL that includes two macros.

The \textbf{Require} macro defines ports required for interaction. Let $T_1, T_2 \in \ensuremath{\mathcal{T}}$ be two component types. For instance:
\begin{align*}
  &T_1.p \ensuremath{\ \ \mathbf{Require}\ \ } T_2.q\ T_2.q\ ;\ T_2.r\,,
\end{align*}
means that, to participate in an interaction, each of the ports $p$ of component instances of type $T_1$ requires either the participation of \emph{precisely two} of the ports $q$ of component instances of type $T_2$ or one instance of $r$. Notice the semicolon in the macro that separates the two options.

The \textbf{Accept} macro defines optional ports for participation, \ie it defines the boundary of interactions. This is expressed by explicitly excluding from interactions all the ports that are not optional.
For instance, if ${p,q,r}$  is the set of port types of component types $T_1, T_2 \in \ensuremath{\mathcal{T}}$ then:
\begin{align*}
	\label{eq:accept}
	 &T_1.p \ensuremath{\ \ \mathbf{Accept}\ \ } T_2.q\,,
\end{align*}
means that instances of $r$ are excluded from interaction with instances of $p$.
To illustrate the use of the macros, let us define the Star architecture style with Require/Accept:
\begin{align*}
  \mathtt{S.q} &\ensuremath{\ \ \mathbf{Require}\ \ } \mathtt{C.p}
  &\mathtt{S.q} &\ensuremath{\ \ \mathbf{Accept}\ \ } \mathtt{C.p}
  \\
  \mathtt{C.p} &\ensuremath{\ \ \mathbf{Require}\ \ } \mathtt{S.q}
  &\mathtt{C.p} &\ensuremath{\ \ \mathbf{Accept}\ \ } \mathtt{S.q}
\end{align*}

The syntax and semantics of first-order interaction logic (FOIL) as well as the Require/Accept macronotation are presented in greater detail in the technical report~\cite{mavridouDesignBIPReport}.

\section{Semantic Integration Components}

We present the BIP parameterized graphical language that was integrated in DesignBIP. The DesignBIP metamodel can be found in the technical report~\cite{mavridouDesignBIPReport}.
\subsection{Architecture Diagrams for BIP}
\label{sec:simplediagrams}


Architecture diagrams~\cite{MavridouBBS16} is a parameterized graphical language for the description of
the structure of a system by showing the system's component types and their attributes for coordination
We extend the definition of architecture diagrams with triggers and synchrons to define BIP connectors.
A BIP architecture diagram consists of a set of \emph{component types} and a set of \emph{connector motifs}. Each component type $T$ is characterized by a set of \emph{port types} $T.P$ and a \emph{cardinality} parameter $n$, which specifies the number of instances of $T$.
 \fig{ex1} shows an architecture diagram consisting of two component types $T_1$ and $T_2$ with $n_1$ and $n_2$ instances and port types $p$ and $q$, respectively.  Instantiated components have port instances $p_i$, $q_j$ for $i,j$ belonging to the intervals $[1,n_1]$, $[1,n_2]$, respectively.
 
 \begin{figure} [t]
	\centering
	\includegraphics[scale=1]{Example2.png}
	\caption{A BIP architecture diagram}  	
  	\label{fig:ex1}
  	  
\end{figure}
\begin{figure} [t]
	\centering
	\includegraphics[scale=1]{Example1.png}
  	\caption{A conforming architecture to the diagram in \fig{ex1}}
  	\label{fig:obtArchEx1}
  
\end{figure}

Connector motifs are non-empty sets of port types.
Each port type $p$ in a connector motif has two constraints represented as a pair $m:d$. Multiplicity $m$ of a port type constrains the number of port instances of this type that are involved in each connector defined by the connector motif. Degree $d$ of a port type constrains the number of connectors attached to every port instance of this type. Additionally, each port type has a typing (attribute) represented by $t_p$, which can be either \emph{trigger} (represented by a triangle) or \emph{synchron} (represented by a bullet) (see BIP connectors in Section \ref{secn:bip}). A connector motif  defines a set of possible configurations, where a configuration is a non-empty set of connectors. The meaning of a diagram is the union of all configurations corresponding to each connector motif of the diagram. Let us present the semantics of connector motifs through the example of \fig{ex1}, which has a single connector motif involving port types $p$ and $q$.

\fig{obtArchEx1} shows the unique configuration obtained from the diagram of \fig{ex1} by taking $n_1=1$, $m_p=1$, $d_p=1$; $n_2=2$, $m_q=2$ and $d_q=1$. This is the result of composition of constraints for port types $p$ and $q$.
 For instance, since the multiplicity of $q$ is $2$, then both $q_1$ and $q_2$ must be involved in the the same connector. The degrees of $p$ and $q$ are equal to $1$, thus there is exactly one connector attached to their port instances. Port instances retain the typing of their corresponding port types. The set of interactions defined by the connector in \fig{obtArchEx1} is the following: $\{q_1, q_2, q_1q_2, q_1p, q_2p, q_1q_2p\}$.



Formally, a {\em BIP architecture diagram} $\ensuremath{\mathcal{D}}\ = \langle \ensuremath{\mathcal{T}}, \ensuremath{\mathcal{C}} \rangle$ consists of:
\begin{itemize}
\item a set of \emph{component types} $\ensuremath{\mathcal{T}} = \{T_1, \dots, T_k\}$ of the form $T = (T.P, n)$, where $T.P \neq \emptyset$ is the set of \emph{port types} of component type $T$ and $n \in \ensuremath{\mathbb{N}}$ is the \emph{cardinality} parameter associated to component type $T$
\item a set of \emph{connector motifs} $ \ensuremath{\mathcal{C}} = \{\ensuremath{\Gamma}_1, \dots, \ensuremath{\Gamma}_l\}$ of the form  $\ensuremath{\Gamma} =(a, \{m_p:d_p,\ t_p\}_{p \in a})$, where
\begin{itemize}
\item $\emptyset \neq a \subset \bigcup_{i=1}^k T_i.P$ is a set of port types
\item  $m_p, d_p \in \ensuremath{\mathbb{N}}$ (with $m_p > 0$) are the \emph{multiplicity} and \emph{degree} associated to port type $p \in a$
\item $t_p \in \{synchron,\ trigger\}$ is the typing of port type $p \in a$
\end{itemize}
\end{itemize}


For a component $c \in \ensuremath{\mathcal{B}}$ and a component type $T$, we say that {\em $c$ is of type $T$} if the ports of $c$ are in a bijective correspondence with the port types in $T$.

An architecture $\langle \ensuremath{\mathcal{B}}, \gamma \rangle$ \emph{conforms} to a diagram $\langle \ensuremath{\mathcal{T}}, \ensuremath{\mathcal{C}} \rangle$  if, for each $i \in [1,k]$, 
  the number of components of type $T_i$ in $\ensuremath{\mathcal{B}}$ is equal to $n_i$ and
  $\gamma$ can be partitioned into disjoint sets $\gamma_1,\dots,\gamma_l$, such that, for each connector motif $\ensuremath{\Gamma}_i =(a, \{m_p:d_p,\ t_p\}_{p \in a}) \in \ensuremath{\mathcal{C}}$ 
  and each $p \in a$, 
\begin{enumerate}
\item in each connector in $\gamma_{i}$ there are exactly $m_p$ instances of $p$ typed as $t_p$,
\item each instance of $p$ is involved in exactly $d_p$ connectors in $\gamma_{i}$
\end{enumerate}
The meaning of a BIP architecture diagram is the set of all architectures that conform to it.

\subsubsection{Conformance Conditions}
\label{sec:conformance}
DesignBIP encodes connector motifs in the Require/Accept macronotation (Section \ref{secn:bip}) in order to give the latter as input to the integrated JavaBIP-engine. Nevertheless, the semantic domains of BIP architecture diagrams and interaction logic (Section \ref{secn:bip}) do not coincide. An architecture diagram defines a set of configurations, whereas, an interaction logic formula defines exactly one configuration. Consider the architecture diagram shown in \fig{nontranslatablediagram} with a single connector motif, which defines two configurations: $\gamma_1 = \{p_1 q_1, p_2 q_2\}$ and $\gamma_2 = \{p_1 q_2, p_2 q_1\}$, and thus, cannot be encoded into interaction logic. 
Let us now consider the architecture diagram shown in Figure
\ref{fig:translatable2}, which is a variation of the diagram shown in \fig{nontranslatablediagram} with degrees set to $d_p=d_q=2$. This diagram defines exactly one configuration and thus, can be encoded into interaction logic. In particular, it defines the configuration $\gamma = \{p_1 q_1, p_2 q_2, p_1 q_2, p_2 q_1\}$.  This shows that we can restrict an architecture diagram to define exactly one configuration by constraining its multiplicities or degrees.

\begin{figure}
\centering
\includegraphics[scale=1]{nontranslatablediagram.pdf}
\caption{An architecture diagram that cannot be encoded into FOIL}
\label{fig:nontranslatablediagram}
\end{figure}

\begin{figure} [t]
	\centering
	\includegraphics[scale=1]{encodable2}
  	\caption{An architecture diagram that can be encoded into FOIL}
  	\label{fig:translatable2}
  
\end{figure}
 
We denote $s_p = n_p \cdot d_p / m_p\ \in \mathbb{N}$ the \emph{matching factor} of a port type $p$, where $n_p$ is the cardinality of the component type that contains $p$. The matching factors of all port types participating in the same connector motif must be equal integers, in which case they represent the number of connectors defined by the connector motif. The maximum number of distinct connectors defined by a connector motif $\ensuremath{\Gamma} = (a, \{m_p:d_p,\ t_p\}_{p \in a})$ is equal to $\prod_{q \in a} {\binom{n_q}{m_q}}$.
Consider the connector motif shown in \fig{nontranslatablediagram}. The matching factors of its port types are $s_p = s_q = 2$ and are not equal to ${\binom{2}{1}} \cdot {\binom{2}{1}}$, which represents the maximum number of connectors that can be defined by this connector motif. The matching factors of the connector motif shown in Figure \ref{fig:translatable2} is $4$.

\prop{srequirement} provides the necessary and sufficient conditions for a BIP diagram to define exactly one conforming architecture for each evaluation of its cardinality parameters. If these conditions hold, then the diagram can be encoded into FOIL. The encoding conditions are as follows: 1) the multiplicity of a port type must be less than or equal to the number of component instances that contain this port and 2) the matching factors of all port types participating in the same connector motif must be equal to the maximum number of connectors that the connector motif defines. Since, by the semantics of diagrams, connector motifs correspond to disjoint sets of connectors, these conditions are applied separately to each connector motif.
The proof of Proposition \ref{prop:srequirement} can be found in the technical report~\cite{mavridouDesignBIPReport}. Corollary \ref{col:srequirement} follows directly from Proposition \ref{prop:srequirement}.

\begin{proposition}
\label{prop:srequirement}
A BIP architecture diagram has exactly one conforming architecture iff, for each connector motif $\ensuremath{\Gamma} = (a, \{m_p:d_p,\ t_p\}_{p \in a})$ and each $p \in a$, we have 1) $m_p \le n_p$ and 2)~$s_p = \prod_{q \in a} {\binom{n_q}{m_q}}$.
\end{proposition}

\begin{corollary}
\label{col:srequirement}
A BIP architecture diagram can be specified in FOIL using the Require/Accept macro-notation iff, for each connector motif $\ensuremath{\Gamma} = (a, \{m_p:d_p,\ t_p\}_{p \in a})$ and each $p \in a$, we have 1) $m_p \le n_p$ and 2) $s_p = \prod_{q \in a} {\binom{n_q}{m_q}}$.
\end{corollary}
 




\section{Service Integration Components}

We present the model and code editors, the code generators, and the model repositories of DesignBIP.

\subsection{Model and Code editors}


  \begin{figure} [t]
 	\centering
 	\includegraphics[scale=0.5]{routes.png}
 	\caption{DesignBIP LTS model editor and Java code editor}
   	\label{fig:editors}
 \end{figure}

A developer provides the system specification by using the dedicated model and Java code editors of DesignBIP. In particular, the developer must specify 1)~component behavior in the form of BIP LTS, 2)~component interaction in the form of BIP architecture diagrams and 3)~the actions associated with transitions and guards, as well as variable declarations directly in Java.
Figures \ref{fig:editors} and \ref{fig:editors2} present the DesignBIP LTS and BIP diagram model editors, as well as the Java code editor. In the code editor, the darker parts represent code that was automatically generated by the input given in the model editors, while the bright code parts represent input given directly in the code editor. In the LTS model editor, enforceable and internal transitions are illustrated with solid arrows, while spontaneous transitions are illustrated with dashed arrows. The code and model editors are tightly synchronized, \ie changes are instantaneously propagated.

   \begin{figure} 
 	\centering
 	\includegraphics[scale=0.45]{routesAlltogether.png}
 	\caption{DesignBIP architecture diagrams model editor}
   	\label{fig:editors2}
 \end{figure}

\subsection{Behavior generation plugin: LTS to Java code}

As explained earlier, a developer graphically specifies the LTS that represents component behavior. DesignBIP generates the Java code that describes the LTS specified by the developer. In particular, DesignBIP generates code in the form of Java annotations that describes the ports, component types, transitions, and guards of each LTS. For instance, Java annotations describing the ports of the \texttt{Route} component type (Figure~\ref{fig:editors2}) are shown in the right-hand side of Figure~\ref{fig:editors}. 

Firstly, before the plugin generates the Java code, it checks the correct instantiation of each specified LTS according to the constraints defined in the DesignBIP metamodel, which can be found in the technical report~\cite{mavridouDesignBIPReport}. For instance, the plugin checks whether each LTS has exactly one initial state. If errors exist, DesignBIP returns to the developer a message explaining the error and pointers (displayed as \texttt{Show node}) to the incorrect nodes of the specified model as shown in Figure~\ref{fig:errors}. In the case of a correct behavioral model, DesignBIP returns a set of Java files, i.e., one Java file for each specified component type. The complete generated Java annotations for the \texttt{Route} component type can be found in the technical report~\cite{mavridouDesignBIPReport}.

\begin{figure}
  \centering
  \includegraphics[scale=0.52]{errors.png}
  \caption{Behavioral errors as returned by DesignBIP}
  \label{fig:errors}
\end{figure}



\subsection{Interaction generation plugin: BIP architecture diagrams to XML code}

We propose Algorithm~\ref{alg:macrosencoding}, with polynomial-time complexity for the encoding of a BIP architecture diagram into Require/Accept macros (Section \ref{secn:bip}). For each port type, we instantiate two sets of variables: \texttt{require} and \texttt{accept}. For the sake of simplicity, we write $p$ instead of $T.p$.

\begin{algorithm}
 \footnotesize
\KwData{Diagram $\ensuremath{\mathcal{D}}\ =\ \langle \ensuremath{\mathcal{T}}, \ensuremath{\mathcal{C}} \rangle$, where $\ensuremath{\mathcal{C}} = \{ \Gamma_1, \dots, \Gamma_n \}$ and $\ensuremath{\Gamma} =(a, \{m_p:d_p,\ t_p\}_{p \in a})$}
\KwResult{Returns the macros for each port type in $\ensuremath{\mathcal{D}}$}

$require  \longleftarrow \{\};$ 
$accept \longleftarrow \{\};$\\
/* for each port type p in the diagram */ \newline
\For{$p \in$ $\ensuremath{\mathcal{T}}.P$}{
  $require[p] = $ $new\ Set\ ()$;
  $accept[p] = $ $new\ Set\ () $; \newline
  /* for all connector motifs attached to p */ \newline
  \For{$\Gamma \in p.connectorMotifs$}{
  /* if the connector motif is singleton */ \newline
    \If{$|a| == 1$}{
      $require[p].add(-)$;  $accept[p].add(-)$; 
    }
    \Else{
       /* if the multiplicity of end attached to $p$ is not $1$,
       add all ports of the connector motif */ \newline
      \If{$m_p > 1$}{
        $accept [p].add(a);$
      }
      /* otherwise add all ports excluding $p$ */ \newline
      \Else {
        $accept [p].add(a \setminus \{p\});$
      }
      /* if the end attached to $p$ is trigger */ \newline
     \If{$t_p ==\ $\textnormal{trigger}}{
      $require[p].add(-);$ \newline
      }
      /* else if there exists at least one trigger */ \newline
      \ElseIf{$\exists\ p \in a\ : t_p\ == \textnormal{trigger}$}{
      	\For{$q \in a$ $\wedge$ $t_q ==\ \textnormal{trigger}$}{
			/* for each trigger add an option */ \newline
				
				 $require$[$p$].$add(p);$ 
        }
      }
      /* else add all ports as many times as their multiplicity */ \newline
      \Else {
  		$optionRequire[p] = new List()$; \newline
        \For{$q \in a \setminus \{p\}$}{
               $optionRequire [p].add(\underbrace{qq\ldots q}_{m_q});$
        }
        $optionRequire[p].add(\underbrace{pp\ldots p}_{m_p - 1});$ \newline
        $require$[$p$].\textit{add(optionRequire}[$p$]);     
       } 
    }
  }
}
\Return $require$ and $accept$;
\caption{Encoding a BIP Diagram into Require/Accept Macros}
\label{alg:macrosencoding}
\end{algorithm}

The \texttt{accept} set of $p$ contains the right hand side of \ensuremath{\ \ \mathbf{Accept}\ \ } and  is constructed as follows. For each connector motif attached to $p$, if its size is: 1)~equal to $1$, \ie singleton connector motif, then we add - in \texttt{accept}\footnote{The dash - indicates that $p$ must not synchronize with any other port.}; 2)~greater than $1$ and the multiplicity of $p$ is greater than $1$, we add in \texttt{accept} all port types of the connector motif including $p$; 3)~greater than $1$ and the multiplicity of $p$ is equal to $1$, we add all port types of the connector motif except for $p$ to \texttt{accept}.

The \texttt{require} set of $p$ contains the right hand side of~\ensuremath{\ \ \mathbf{Require}\ \ } and is constructed as follows. For each connector motif attached to $p$, if its size is: 1)~ equal to $1$ or $p$ is typed as trigger then we add - to \texttt{require}\footnote{The dash - indicates that $p$ does not require any other port for synchronization.}; 2)~greater than $1$ and there exists at least one trigger, we add to \texttt{require} as many options as the number of triggers. In each option we add a trigger; 3)~greater than $1$ and there are no triggers, we add to \texttt{require} all port types of the connector motif except for $p$ as many times as their associated multiplicity and $m_p - 1$ times the port type $p$, to form a single option.

Before generating the XML code, DesignBIP checks the conformance conditions presented in Section~{ref:conformance}. Additionally, DesignBIP checks the correct instantiation of the multiplicity and degree constraints of each connector motif. If errors exist, DesignBIP returns to the developer messages explaining the errors and pointers to the incorrect nodes of the model. In the case of a correct interaction model, DesignBIP returns an XML file with the generated code.
Part of the generated XML code for the \texttt{Switchable Routes} example (Figure~\ref{fig:editors2}) can be found in the technical report~\cite{mavridouDesignBIPReport}. 

\subsection{Model repositories}
To promote reusability in DesignBIP, each project is accompanied by component type and coordination pattern~\cite{mavridou2016satellite} repositories. For instance, let us consider the mutual exclusion coordination pattern shown in Figure~\ref{fig:mutex} that enforces the \textit{no two processes can use the shared resource simultaneously} coordination property.
The shared resource is managed by the unique \mdash due to the cardinality being $1$ \mdash \texttt{Mutex Manager} component type. The multiplicities of all port types are $1$ and therefore, all connectors are binary. The degree constraints require that each port instance of a component of type \texttt{Process} be attached to a single connector and each port instance of the \texttt{Mutex Manager} be attached to $n$ connectors. The behaviors of the two component types enforce that once the resource is acquired by a component of type \texttt{Process}, it can only be released by the same component. 

\begin{figure}
  \centering
  \includegraphics[scale=1.8]{mutualExclusionStyle.pdf}
  \caption{The mutual exclusion pattern}
  \label{fig:mutex}
\end{figure}


To use a coordination pattern, a developer needs to create an instance of the pattern in the model and evaluate its cardinality parameters. For instance, if the developer wants to enforce mutual exclusion on two instances of \texttt{Process} then $n$ must be set equal to $2$.







\section{JavaBIP-engine Execution and Visualization}
\label{secn:engine}
After generating the system specification, the developer may use the integrated JavaBIP-engine to execute it. 
The JavaBIP-engine is offered through a dedicated plugin in DesignBIP. If the cardinality parameters of the component types have not been evaluated, the plugin asks the developer to provide the number of instances of each component type. It then instantiates the components and passes their reference to the JavaBIP-engine alongside with the generated Java and XML code. 
The plugin starts the JavaBIP-engine that runs the following three-step protocol in a cyclic manner:
1)~upon reaching a state, each component notifies the JavaBIP-engine about possible outgoing transitions, 2)~the JavaBIP-engine computes the possible interactions of the system, picks one, and notifies the involved components, 3)~the notified components execute the functions associated with the corresponding transitions. 

The output of the JavaBIP-engine (which transitions are picked at each execution cycle) is stored as a JSON object. When the plugin stops the execution of the engine (the execution time is defined by the developer), the output is sent back to the model editors of DesignBIP for simulation (see Figure~\ref{fig:engine}). Initially, the developer picks the subset of components whose execution wants to simulate. Starting by highlighting the initial states of these components, the visualizer shows which transitions are executed in each execution cycle by firstly highlighting the fired transitions and finally their destination states.

\begin{figure}
  \centering
  \includegraphics[scale=0.42]{engine.png}  \caption{Visualization of the execution of the \texttt{Switchable Routes example}}
  \label{fig:engine}
\end{figure}


\begin{comment}
\subsection{Conformance Checking with FORMULA}
\label{secn:formulaChecking}
Microsoft's FORMULA~\cite{jackson2013formula, jackson2010components} is a specification language and analysis tool for model-based abstraction. FORMULA uses algebraic data types and declarative rules in the form of stratified logic programs for defining formal specifications. FORMULA has been used in many applications of model-based engineering such as reasoning about metamodeling or finding specification errors. We integrate FORMULA into DesignBIP to check model conformance on a set of constraints, which can be either automatically derived from the DesignBIP metamodel or are specific to the language and thus, cannot be automatically derived. We automatically generated $22$ conformance rules and manually added $4$ rules.

Conformance checking with FORMULA is offered through a dedicated plugin. When a non-empty set of violations is encountered, the plugin returns the list of violations, describing the reasons why the violations occurred. Additionally, the plugin returns a list of pointers to the erroneous nodes of the DesignBIP project. The user can navigate to an erroneous node through a simple click.

\subsubsection{Automatically Generated Conformance Rules}
We define a methodology for automatically generating FORMULA constraints from UML class diagrams that contain the following relations: 1)~Composition, 2)~Uni-directional Association, and 3)~Inheritance. We chose this subset of UML class diagrams relations because these are the ones used for metamodeling in WebGME. First, we formalize the DesignBIP metamodel in FORMULA. Let us consider the \texttt{Transition\_Base} concept of the DesignBIP metamodel (see Figure \ref{fig:metamodel}). The equivalent FORMULA specification is:

\begin{Verbatim}[fontsize=\small]
TransitionBase ::= new (
id: String,
parent: any ComponentTypeTYPE,
attributes: any Attr__TransitionBase,
pointers: any Ptr__TransitionBase
).
Attr__TransitionBase ::= new (
  guardExpression: String,
  name: String,
  transitionMethod: String
).
Ptr__TransitionBase ::= new (
  dst: any StateTYPE + InitialStateTYPE,
  src: any StateTYPE + InitialStateTYPE
).
TransitionBaseTYPE ::= InternalTransition + SpontaneousTransition +
 EnforceableTransition.
\end{Verbatim}

Rules based on the composition relation involve the following constraints: 1) \textit{a concept must have exactly one parent of specific type}, and 2) depending on the multiplicities of the composition relation \textit{a parent must contain a specific number of children}. For instance, from the DesignBIP metamodel we can derive the following rule: \textit{Every component type must contain exactly one initial state}, or equivalently in FORMULA:

\begin{Verbatim}[fontsize=\small]
NotOneInitState :- p is ComponentTypeTYPE, 
1 != count({s | s is InitialStateTYPE, s.parent = p}).

conforms no NotOneInitState.
\end{Verbatim}
Similarly for every uni-birectional association we have the constraints that its source and destination should point to elements of specific types. Due to space limitations, we provide the full DesignBIP metamodel and conformance rules in FORMULA  in Appendix \ref{secn:FORMULAmetamodel} and \ref{secn:FORMULArules}, respectively.
\end{comment}


\begin{comment}
\subsection{Evaluation results}

The goal of this paper is not the evaluation of BIP, which has already been done in several application contexts~\cite{Basu11-RCBSD,SPE:SPE2495,mavridou2016satellite}, but a demonstration of an accessible and practical design studio for rigorous system design. Thus, we present evaluation results on the aspects of DesignBIP that we have implemented. Our evaluation is based on $4$ use cases, their models can be found online\footnote{https://github.com/DesignBIP/DesignBIP}. Table \ref{useCaseInfo} summarizes the complexity of each use case. Notice that Table \ref{useCaseInfo} is based on types and not on instances, thus, upon instantiation the number of states and synchronization primitives (\ie synchrons and triggers) can be much higher depending on the number of component and connector instances. For instance, for $1000$ component instances in the Switchable Routes example, we have $3000$ connectors and $3998$ states. The latter does not apply to the Satellite Software case study, in which all component type cardinalities are set to $1$. Thus, the Satellite Software case study specifies exactly one BIP system in which we have precisely $49$ component instances and $155$ connector motifs.

\begin{table}[t]
\centering
\caption{Use case complexity information}
\label{useCaseInfo}
\begin{tabular}{|l|c|c|c|c|c|}
\hline
\multicolumn{1}{|c|}{Use Case} & \begin{tabular}[c]{@{}c@{}}Component\\  Types\end{tabular} & \begin{tabular}[c]{@{}c@{}}Connector\\  Motifs\end{tabular} & Synchrons & Triggers & States \\ \hline
Switchable Routes              & 2                                                          & 3                                                           & 5         & 0        & 5      \\ \hline
Smart Grid                     & 7                                                          & 11                                                          & 18        & 3        & 15     \\ \hline
Modular Phone                  & 14                                                         & 29                                                          & 58        & 0        & 35     \\ \hline
Satellite software             & 49                                                         & 155                                                         & 196       & 38       & 136    \\ \hline
\end{tabular}
\end{table}

The case studies were run on an 3.1 GHz Intel Core i7 with 8GB RAM. We measure the time needed in seconds to generate the JavaBIP code and the BIP code for $49$, $100$ and $1000$ components (Table 2) for each case study except Satellite Software where we measure the time for $49$ components. Additionally, we measure the time needed in seconds to check conformance of models with FORMULA (Table 3). We ran the experiments $1000$ times and took the average.

\begin{table} [t]
\parbox{.45\linewidth}{
\centering
\caption{Code generation}
\begin{tabular}{|l|c|c|c|c|}
\hline
\multicolumn{1}{|c|}{} & \begin{tabular}[c]{@{}c@{}}BIP\\ 49\end{tabular} & \begin{tabular}[c]{@{}c@{}}BIP\\ 100\end{tabular} & \begin{tabular}[c]{@{}c@{}}BIP \\ 1000\end{tabular} & \multicolumn{1}{l|}{JavaBIP} \\ \hline
Switchable Routes                     & 1,389                                            & 2,980                                             & 5,592                                               & 1,264                        \\ \hline
Smart Grid                     & 2,569                                            & 3,998                                             & 7,984                                               & 2,302                        \\ \hline
Modular Phone                     & 1,792                                            & 3,650                                             & 6,861                                               & 1,678                        \\ \hline
Satellite Software                     & 3,786                                            & -                                                 & -                                                   & 3,398                        \\ \hline
\end{tabular}

}
\hfill
\parbox{.45\linewidth}{
\centering
\caption{Conformance checking}
\begin{tabular}{|l|c|}
\hline
\multicolumn{1}{|c|}{} & FORMULA \\ \hline
Switchable Routes                     & 0,560   \\ \hline
Smart Grid                     & 0,891   \\ \hline
Modular Phone                     & 0.934   \\ \hline
Satellite Software                     & 3,912   \\ \hline
\end{tabular}
}
\end{table}

JavaBIP code is based on component types, while BIP code depends on component instances. Interestingly, Table 2 shows that code generation times are higher for the Smart Grid case study than the Modular Phone case study although the latter contains more component types. What appears to impact the performance results is the architecture specification of Smart Grid, which contains more multi-party interactions and triggers. Table 3 shows that FORMULA conformance checking times remain relatively low even for large case studies (Satellite Software). For both types of results we measure the time from the point that the user starts the execution of a plugin till the moment it receives the output of the plugin, which includes parsing the model.
\end{comment}


\section{Related Work}
Model-driven component-based software engineering and development~\cite{beydeda2005model,heineman2001component,clemens1998component} has become an accepted practice for tackling software complexity in large-scale systems. It provides mechanisms to support design at the right level of abstraction, error detection, tool integration, verification and maintenance. Systems are built by composing and reusing small, tested building blocks called components.  

The Generic Modeling Environment (GME) and its successor WebGME are open source Model Integrated Computing (MIC) tools developed for creating domain specific modeling environments and has been effectively applied to a number of domains~\cite{stankovic2003vest, thramboulidis2005model, neema2016c2wt, beccani2015systematic}.

Close to our approach is the ROSMOD design studio~\cite{rosmod} that also relies on WebGME for collaborative code development and model editing features. The basic building blocks of ROSMOD are specified in its metamodel which is described in UML class diagrams~\cite{bell2003uml}. The code development and compilation process have been integrated in the graphical user interface to keep the framework self-sufficient. ROSMOD integrates code development, code generation, compilation, run-time monitoring, and execution time plot generation. Nevertheless, in ROSMOD component behavior is defined directly with code and thus connection to verification tools is not supported.

A plethora of approaches exists for architecture specification. Patterns~\cite{daigneau2011service,Hohpe:2003:EIP:940308} are commonly used for specifying architectures in practical applications. The specification of architectures is usually done in a graphical way using general purpose graphical tools. Such specifications are easy to produce but their meaning may not be clear since the graphical conventions lack formal semantics and thus are not amenable to formal analysis. 
Significant work has been done by the Architecture Description Languages (ADLs) community. Many ADLs have been developed for architecture specification~\cite{medvidovic2000classification,  ozkaya2013we} with rigorous semantics that facilitate communication of system properties and allow system analysis. 
Nevertheless, according to~\cite{malavolta2013industry}, architectural languages used in practice mostly originate from industrial development (e.g., UML) instead of academic research (e.g., ADLs).  Scientific questions remain about UML's formal properties~\cite{harel2004meaningful}. The use of UML has been demonstrated in~\cite{clements2002documenting, ivers2004documenting} for representing architectural concepts with a focus on the component and connector view. However, exploiting these constructors to express architecture views may result in a proliferation of models and stereotypes, which can be difficult to integrate into a well-structured code generation process. On the other hand, ADLs with formal semantics require the use of formal languages which are considered as challenging for practitioners to master~\cite{malavolta2013industry}. We chose architecture diagrams, which rely on a small set of notions and combine the benefits of graphical languages and rigorous formal semantics. 




\section{Conclusion}

We presented DesignBIP\footnote{https://cps-vo.org/group/BIP}, which is a web-based, open source design studio\footnote{https://github.com/anmavrid/DesignBIP} for modeling and generating BIP systems.
To define system coordination aspects, we used a parameterized graphical language with formal semantics called architecture diagrams, which we extended with BIP coordination primitives. Designing and reusing models that are based on types and not on instances allowed us to cope with the issues of modeling complexity and size. We have implemented dedicated model/code editors, visualizers, as well as integrated the JavaBIP-engine.
Additionally, we studied model transformations and implemented dedicated code generation plugins.  We have opted for generating code from high-level graphical structures to avoid tedious and error-prone development of Boolean formulas. Rooting the whole modeling and execution process in rigorous semantics allows the connection to checkers and analysis tools.  In the future, we are going to integrate data transfer information on connector motifs. We are also going to develop code generators for the BIP1 and BIP2 languages and  integrate verification tools.



\section*{Acknowledgements}
This research is supported by the National Science Foundation under award \# CNS-1521617. The authors would like to thank Hoang-Dung Tran and Venkataramana Nagarajan for helping with the implementation of DesignBIP.


\bibliographystyle{eptcs}
