Running Example: The Synchronized Product Operator between Timed Finite State Machines
The synchronized product operator coordinates models conforming to the Timed Finite State Machine (TFSM) language; a state machine language augmented with timed transitions. Briefly, the operator accepts two models conforming to TFSM as argument. It selects the events with same name, and then, it coordinates the selected events by forcing a simultaneous occurrence between events.
To run the example, we need a GEMOC studio with the BCOoL plug-in installed. In the first GEMOC studio workspace, we create new project example of TFSM language.
In the second GEMOC studio workspace, we import the project from the BCOoLExample repository in github. The project includes the needed interfaces libraries, and the operator. In addition, it includes some example models to apply the operator.
To generate the model of coordination between two TFSMs, two steps are needed. First, we compile the BCOoL spec as is shown in the picture. This generates a qvto transformation that applies between any pair of models conforming to the TFSM language (in src-gen).
Once compiled, the qvto transformation enables to generate the model of coordination between any pair of TFSM models. To do so, we select the input models (jobB.tfsm and jobA.tfsm) and we click on create ccsl coordination.
This results in the generation of a CCSL specification that includes the CCSL spec of each model plus the coordination. The specification can be executed by using TimeSquare.
The specification can be executed by using TimeSquare. Figure illustrates the partial timing output (VCD) of the execution of the whole example. In the Figure, we highlight the events that results coordinated.
The workbench also offers the possibility to obtain by exploration quantitative results on the scheduling state-space. Figure illustrate the graphical representation of the state-space for our example. The exploration results in 66 states and 3454 transitions.
The Surveillance Camera System (MoDELS2015)
In this example, we use BCOoL to develop three coordination operators between the TFSM and the Activity lenguages. These operators are used to specify three coordination patterns between these languages. First, we syncronize FSMEvents of the TFSM language and Signals from the Activity lenguage. Second, we propose a hierarchical coordination operator in which the entering of states are coordinated with the execution of an activity. Finally, we propose a timing coordination operator to coordinate the time in a TFSM and an Activity.
The picture illustrates the application of the operators in a surveillance camera system. To coordinate the models, we have to specify a timing and hierarchical coordination between the states of the TFSM CameraEncoderControl and the activities doJPEG and doJPEG2000.
In addition, we have to synchronize the activity BatterySensor and the TFSM CameraEncoderControl by coordinating the corresponding Signals and FSMEvents. To coordination these models, we develop in the following three BCOoL operators.
In a GEMOC studio, we need in the language workbench the TFSM and the Activity language. The TFSM language must be imported from
here. To get the activity language, we need to clone the following
github repository. Then, in the workspace, we need to import all the projects in the folders activitydiagram/dev/gemoc_commons/ and activitydiagram/dev/gemoc_concurrent/language_workbench/. In addition, we need to import the project org.gemoc.sample.bcool.tfsmandactivityhierarchical that contains the operators. We can get this project from
here. The language workbench should look as in the picture.
In the modeling workbench, we import the project org.gemoc.sample.bcool.cameracontrol from
here. The modeling workbench should look as in the picture. The project includes the heterogeneous models of the surveillance camera system. Also, it contains the BFlow specification that defines how the operators defined in the BCOoL specification must be applied between the models of the camera to get a coordinated system.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the the BFlow specification. Notice that, before to launch the execution, the directory gemoc-gen should contain the generated file CameraControlFlow.xml. This file is automatically generated from the BFlow specification. In case that the file was not generated, it is necessary to edit the
BFlow specification, and then, store it. This will generate the corresponding file in the gemoc-gen directory.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.
The directory gemoc-gen contains the resulting coordinated model together with the timemodel of each individual model. The coordinated model can then be used for verification. For example, the figure illustrates the use of TimeSquare to get a VCD representation of the coordinated system. In this example, we cannot compute the state-space graph since the behavior of the coordinated model is not finite.
To watch the complete procedure go to
Video
The Coffee Machine Example (Demo MoDELS2015)
In this example, we use BCOoL to develop the synchronized product operator between the TFSM and the Activity lenguages. The operator coordinates FSMEvents from the TFSM and Actions from the Activity language by comparing its names.
The picture illustrates the application of the operators in a coffee machine. To coordinate the models, we have to synchronize the activity CoffeeAlgorithm and the TFSM CoffeeCoin by coordinating the corresponding Actions and FSMEvent. In the following, we develop an operator in BCOoL to generate the coordination between these models.
In a GEMOC studio, we need in the language workbench the TFSM and Activity languages. For the TFSM language, it is only necessary to go to File, New, and then Example. In the wizard, we select the GEMOC TFSM language. To get the activity language, we need to clone the following
github repository. Then, in the language workbench, we need to import all the projects from the folders activitydiagram/dev/gemoc_commons/ and activitydiagram/dev/gemoc_concurrent/language_workbench/. Finally, we have to import the bcool project org.gemoc.sample.bcool.tfsmandactivity. We can get this project from
here. The language workbench should look as in the picture.
In the modeling workbench, we import the project org.gemoc.sample.bcool.coffeemachine from
here. The modeling workbench should look as in the picture. The project includes the different models of the coffee machine and the bflow specification to get the coordinated model.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the bflow specification.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.
The directory gemoc-gen contains the resulting coordinated model together with the timemodel of each individual model. The coordinated model can then be used for verification. For example, the figure illustrates the use of TimeSquare to compute the state-space graph.
Figure illustrate the graphical representation of the state-space for our example. The exploration results in 39 states and 405 transitions, without deadlocks. The edges in red represents the transition that contains the events that are forced to happen simultaneously by the coordination (
full graph in .dot format).
To watch the complete procedure go to
Video
A BCOoL operator between the TFSM and SigPML languages
In this example, we use BCOoL to develop an operator between the TFSM and the SigPML (Signal Processing Modeling Language) languages. SigPML is an extension of SDF in which an application is described as a set of Agents. Upon activation, each agent uses the data on its Input Ports, executes N processing cycles and produces computed results on its Output Ports. In this context, we use BCOoL to define an operator that synchronizes the occurrences of FSMEvents and the starting of Agents by relying on their names.
In the following, we use the GEMOC studio to first develop the operator. Then, in the modeling wokbench, we use this operator to coordinate the heterogenenous models of a coffee machine.
In the language workbench, we need the TFSM and SigPML languages. There are two ways to get these languages. They can be deployed by using the wizard. Or, they can be imported from
here. The language workbench should look as in the picture.
Also, in the language workbench, we have to import the project that contains the BCOoL specification. This corresponds with the project named org.gemoc.sample.bcool.tfsmandsigpml. One way to get this project is by using the wizard. To do so, go to New > Example > GEMOC language workbench examples. Also, the project can be downloaded from
here
In the modeling workbench, we have to import the project that contains the models of the coffee machine and the BFLoW specification. The project can get it by doing New > Example > GEMOC modeling workbench examples. Also, this project can be imported from
here. The modeling workbench should look as in the picture.
To execute the coordinated system, we first need to go to Debug Configuration and configure the Gemoc Coordinated eXecutable Models as shown in the picture. The launcher contains information about the BFLoW specification used to build the coordination model and then launch the simulation.
By clicking on debug, the coordinated execution is launched. The engine provides several options to drive the execution of the models. For instance, it enables a system designer to select the next valid execution step. Also, the workbench provides the animation of models.
To watch the complete procedure go to Video
A BCOoL Operator that uses a mapping language to find correspondences
In this example, we use BCOoL to develop the synchronized product operator between the TFSM and the Activity lenguages. The operator coordinates the ocurrences of FSMEvents and the starting of an Action. To find the elements to coordinate, we rely on a third language named Mapping Language which contains correspondences between the TFSM and Activity languages. This lenguage is imported in the BCOoL specification and used in the matching correspondence to find the elements to coordinate.
The example can be found
here. In this case the language workbench has to contain the TFSM and Activity language and also the mapping language (e.g., org.gemoc.sample.bcool.mapping). Then, import the project org.gemoc.sample.bcool.coffeemachinewithsigpml into the modeling workbench.
Vara Larsen, M., “BCool: the Behavioral Coordination Operator Language”, PhD thesis.
[BIBTEX]
[PDF]
Vara Larsen, M., DeAntoni, J., Combemale, B. and Mallet, F. “A Model-Driven Based Environment for Automatic Model Coordination.” In MoDELs (DEMO), Ottawa, 2015.
[BIBTEX]
[PDF]
Vara Larsen, M., DeAntoni, J., Combemale, B. and Mallet, F. “A Behavioral Coordination Operator Language (BCOoL).” In MoDELs, Ottawa, 2015.
[BIBTEX]
[PDF]
Vara Larsen, M., DeAntoni, J., Combemale, B. and Mallet, F. “Framework for Heterogeneous Modeling and Composition.” In Conference en IngenieriE du Logiciel (CIEL’14), Paris, 2014.
[BIBTEX]
[PDF]
Vara Larsen, M., Goknil, A. “Railroad Crossing Heterogeneous Model.” In GEMOC workshop 2013 - International Workshop on The Globalization of Modeling Languages, Miami, 2013.
[BIBTEX]
[PDF]