Early Timing Analysis based on Scenario-based Requirements Specifications – description of sosym paper validation artefacts

This website describes the validation artifacts used in the paper submitted to the sosym journal and accessible here.

Gemoc Simulator

the Gemoc simulator archive is downloadable here. It contains three folders

The first folder (gemoc_studio) is a version 3.0.0rc2 of the Gemoc studio for win32 64 bit platform, available here in which the Papyrus UML editor (with the SysML and MARTE profil) and the Gemoc concurrent engine have been installed. If you have another platform than win32, download the appropriate version the Gemoc studio from here and install the Papyrus UML editor. Then, copy all the repertories from the dropins folder of the provided archive into your version of the Gemoc studio (they contain the SysML and MARTE profiles). Finally, install the concurrent engine by using the Gemoc discovery as illustrated below

Language Workbench

The second folder (languageworkspace) is an eclipse workspace containing the definition of our language (both its syntax in terms of two UML profiles and in terms of its behavioral semantics by using MoCCML and ECL). To use it, start the Gemoc Studio with the appropriate extensions in it (at startup). If no plugins are in your workspace, please import them (import –> existing project into workspace). You should then have the following workspace.

Four of these plugins are of prime importance in our context:

The definition of our syntax, given in de.fraunhofer.iem.swt.msd.tam.tamProfile
The definition of TAM specific constraints, given in de.fraunhofer.iem.swt.msd.tam.mocc
The mapping of the MoCC on the syntax, given in de.fraunhofer.iem.swt.msd.tam.dse
The definition of the language, that glue all the pieces together, given in de.fraunhofer.iem.swt.msd.tam.xdsml

Here are some excerpt of each of the artifacts provided in the archive.

Excerpt of the TAM_Profile (de.fraunhofer.iem.swt.msd.tam.tamProfile). TAM is an UML profile that uses MARTE and enables the formalization of system properties in early development stages

Excerpt of the ECL specification for early timing analyses of MSDs (de.fraunhofer.iem.swt.msd.tam.dse). The ECL specification defines relevant domain-specific events and the realtions between them. These relations constitute the semantics that ist used for early timing analyses of MSDs. The provided ECL specification is described [7] and does not contain the msgCreate event.

An exemplarly MOCC automata (de.fraunhofer.iem.swt.msd.tam.mocc). These automata are initialized within the ECL specification in order to define the relations between domain-specific events. The shown automata defines the order in which the events “msc_msgCreate”, “msc_msgSend”, “msc_msgReceive”, “msc_msgConsume”, “msc_taskStart”, and “msc_taskComplete” occur for an MSD message. It is instantiated for each individual MSD message by the ECL specification.

Modeling Workbench

The artifacts of the language workbench are used in order to conduct early timing analyses of MSDs in the modeling workbench. In order to start the modeling workbench please klick on “Run” and select “Start Runtime”.

The lanaguage workbench contains the following plugins:

de.fraunhofer.iem.swt.msd.examples.ebeas_small: An exemplarly MSD specification with a total amount of four MSDs.
de.fraunhofer.iem.swt.msd.tam.simulationPreProcess: A pre-processing routine for the simulation. This routine retrieves relevant information from the model and stores it at a pre-defined location in the model. This enables a simpler ECL specification.

MSD Models

“de.fraunhofer.iem.swt.msd.examples.ebeas_small” contains the MSD specification that is presented in [7]. The model structure is described in the following:

Types and Interfaces: These packages contain the components and interfaces of the MSD specification. They constitute the Type View of the MSD specification.
Collaboration: The collaboration contains the elements of the Architecture View for one particular use case. That is, the compontents that are involved in the use case (e.g. acc:AdaptiveCruiseControl and dsrc:DSRC) and the connectors between these components (e.g. obstacleCon and emcBrakeWarningCon). Furthermore, the collaboration contains four MSDs that are categorized into TamRequirementMSDs and TamAssumptionMSDs. The TamRequirementMSDs define the desired behavior of the involved components, whereas the TamAssumptionMSDs define assumption on the workload for the system by specifieng the occurrence frequencies of the initial messages. This model contains the MSDs EmcyBrakeTriggeringLeadingVehicle and UpdateSa that are described in Chapter 7 of [7].
Platform: This package defines the system properties of the platform that is used to run the software components.
SystemMessages: This package is created by the pre-processing routine (de.fraunhofer.iem.swt.msd.tam.simulationPreProcess) and contains some pre-processed information for the simulation. For more information on the pre-processing routine please refer to [7]. In order to re-create this package, select “Run” and “PreProcessing”.

Additionally to “de.fraunhofer.iem.swt.msd.examples.ebeas_small”, we provide the model “de.fraunhofer.iem.swt.msd.examples.ebeas_onlyEmcyBrake” which contains only the TamRequirementMSD EmcyBrakeTriggeringLeadingVehicle.

Simulation

The third folder (modelworkspace_JD) contains different models that can be simulated with our approach. To use them, you have to run an eclipse application from the language workspace. It will provide a new eclipse with all the language definition provisioned in it, and consequently provide a modeling workbench in which a developer can model and execute her/his models.

I order to run one of these models, you have to create a run/debug configuration for a Gemoc Concurrent execution, like for instance the following:

You can now debug your model by choosing the logical step in the logical step decider view and you have the feedback on the timing diagram view (VCD)

Exhaustive Simulation

Note that the GEMOC studio compiled the associated timemodel in the gemoc-gen folder. Based on this timemodel, you can construct the whole scheduling state space representing all the acceptable schedules for your model. In the behavioral semantics we provided in Zenodo, the interactions were re-entrant so that the state space is infinite (it is always possible to (re)enter in an interaction at any time). Adding a simple constraint make the system bounded:

   inv makeItBounded:
         let firstMessage : Message = self.fragment->selectByType(MessageOccurrenceSpecification)->first().message in
         let lastMessage : Message = self.fragment->selectByType(MessageOccurrenceSpecification)->last().message in
         Relation Alternates((firstMessage).taskStart,(lastMessage).taskComplete)

When this code is added to the ECL file and the timemodel generated accordingly (for instance by relaunching a simulation) then it is possible to ask for the construction of the scheduling state space by right clicking on the timemodel file, going into the “TimeSquare” menu then “Compute State Space”. After some time (possibly long depending on the size of the state space) the state space is shown in the “MoCCML state space view”. Any cycle in the graph is a correct periodic behavior of the system. A dot file is also created. One can use it to drive analysis. In our case we used it to retrieve and highlight two periodic behaviors of the system that are conforming the semantics (one is the shortest one among the 4000 first cycles and the other is the longest one among these cycles). The results, based on de.fraunhofer.iem.swt.msd.examples.ebeas_onlyEmcyBrake is a state space with 9775 states and 14865 transitions (For your information, the memory used is about 3Go and the time spent: 108 minutes. Note that there is here room or improvement since this has never been optimized). The two automatically extracted periodic behaviors are highlighted on blue and red on the graphs presented below (all are equivalent under different layouts and the violet lines are shared between the two schedules) and the associated schedules follow. In these schedules, the first part is the name of the UML element, the middle part is a unic ID and the last part is the name of the associated DSE. Note that on the state space representations we can see that some of the schedules are not respecting the deadline and lead to deadlock (e.g., on the left and right parts of the first representation). The script to obtain such representation can be obtained here.

link to the big pdf of state space with labels

############################################ shortest schedule among 4000 first cycles ############################################ MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_send, obstacle_2_objSysSend obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_receive, obstacle_2_objSysReceive MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime neighborTbl_5_acquireRes, PU1_7_dispatch, obstacle_2_oneEvent, MSDSpec_0_globalTime, obstacle_2_objSysTaskStart, req_obstacle_9_taskStart obstacle_2_oneEvent, obstacle_2_objSysConsume, req_obstacle_9_consume, MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime obstacle_2_oneEvent, obstacle_2_objSysTaskComplete, MSDSpec_0_globalTime, req_obstacle_9_taskComplete emcyBrakeWarning_1_objSysSend, MSDSpec_0_globalTime, req_emcyBrakeWarning_10_send, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBrakeWarning_10_receive, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysReceive, emcyBrakeWarning_1_oneEvent emcyBrakeWarning_1_objSysConsume, req_emcyBrakeWarning_10_consume, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent emcyBrakeWarning_1_objSysTaskStart, req_emcyBrakeWarning_10_taskStart, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent req_emcyBrakeWarning_10_taskComplete, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysTaskComplete, emcyBrakeWarning_1_oneEvent enableBraking_3_oneEvent, enableBraking_3_objSysSend, req_enableBraking_8_send, MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime enableBraking_3_oneEvent, req_enableBraking_8_receive, MSDSpec_0_globalTime, enableBraking_3_objSysReceive MSDSpec_0_globalTime req_enableBraking_8_consume, enableBraking_3_oneEvent, MSDSpec_0_globalTime, enableBraking_3_objSysConsume enableBraking_3_oneEvent, enableBraking_3_objSysTaskStart, PU2_6_dispatch, MSDSpec_0_globalTime, req_enableBraking_8_taskStart MSDSpec_0_globalTime MSDSpec_0_globalTime enableBraking_3_oneEvent, req_enableBraking_8_taskComplete, MSDSpec_0_globalTime, enableBraking_3_objSysTaskComplete MSDSpec_0_globalTime, emcyBraking_4_objSysSend, req_emcyBraking_11_send, emcyBraking_4_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBraking_11_receive, emcyBraking_4_objSysReceive, MSDSpec_0_globalTime, emcyBraking_4_oneEvent emcyBraking_4_objSysConsume, req_emcyBraking_11_consume, MSDSpec_0_globalTime, emcyBraking_4_oneEvent emcyBraking_4_objSysTaskStart, req_emcyBraking_11_taskStart, MSDSpec_0_globalTime, emcyBraking_4_oneEvent MSDSpec_0_globalTime, req_emcyBraking_11_taskComplete, emcyBraking_4_objSysTaskComplete, emcyBraking_4_oneEvent ###################### ############################################ longest schedule among 4000 first cycles ############################################ MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_send, obstacle_2_objSysSend obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_receive, obstacle_2_objSysReceive MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime neighborTbl_5_acquireRes, PU1_7_dispatch, obstacle_2_oneEvent, MSDSpec_0_globalTime, obstacle_2_objSysTaskStart, req_obstacle_9_taskStart MSDSpec_0_globalTime obstacle_2_oneEvent, obstacle_2_objSysConsume, req_obstacle_9_consume, MSDSpec_0_globalTime obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_receive, obstacle_2_objSysReceive obstacle_2_oneEvent, MSDSpec_0_globalTime, req_obstacle_9_send, obstacle_2_objSysSend MSDSpec_0_globalTime obstacle_2_oneEvent, obstacle_2_objSysConsume, req_obstacle_9_consume, MSDSpec_0_globalTime MSDSpec_0_globalTime neighborTbl_5_acquireRes, PU1_7_dispatch, obstacle_2_oneEvent, MSDSpec_0_globalTime, obstacle_2_objSysTaskStart, req_obstacle_9_taskStart MSDSpec_0_globalTime MSDSpec_0_globalTime obstacle_2_oneEvent, obstacle_2_objSysTaskComplete, MSDSpec_0_globalTime, req_obstacle_9_taskComplete MSDSpec_0_globalTime emcyBrakeWarning_1_objSysSend, MSDSpec_0_globalTime, req_emcyBrakeWarning_10_send, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime obstacle_2_oneEvent, obstacle_2_objSysTaskComplete, MSDSpec_0_globalTime, req_obstacle_9_taskComplete MSDSpec_0_globalTime emcyBrakeWarning_1_objSysSend, MSDSpec_0_globalTime, req_emcyBrakeWarning_10_send, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBrakeWarning_10_receive, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysReceive, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime emcyBrakeWarning_1_objSysConsume, req_emcyBrakeWarning_10_consume, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime emcyBrakeWarning_1_objSysTaskStart, req_emcyBrakeWarning_10_taskStart, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime req_emcyBrakeWarning_10_taskComplete, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysTaskComplete, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime enableBraking_3_oneEvent, enableBraking_3_objSysSend, req_enableBraking_8_send, MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBrakeWarning_10_receive, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysReceive, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime emcyBrakeWarning_1_objSysConsume, req_emcyBrakeWarning_10_consume, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime emcyBrakeWarning_1_objSysTaskStart, req_emcyBrakeWarning_10_taskStart, MSDSpec_0_globalTime, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime req_emcyBrakeWarning_10_taskComplete, MSDSpec_0_globalTime, emcyBrakeWarning_1_objSysTaskComplete, emcyBrakeWarning_1_oneEvent MSDSpec_0_globalTime enableBraking_3_oneEvent, enableBraking_3_objSysSend, req_enableBraking_8_send, MSDSpec_0_globalTime enableBraking_3_oneEvent, req_enableBraking_8_receive, MSDSpec_0_globalTime, enableBraking_3_objSysReceive MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime req_enableBraking_8_consume, enableBraking_3_oneEvent, MSDSpec_0_globalTime, enableBraking_3_objSysConsume MSDSpec_0_globalTime enableBraking_3_oneEvent, enableBraking_3_objSysTaskStart, PU2_6_dispatch, MSDSpec_0_globalTime, req_enableBraking_8_taskStart MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime enableBraking_3_oneEvent, req_enableBraking_8_receive, MSDSpec_0_globalTime, enableBraking_3_objSysReceive enableBraking_3_oneEvent, req_enableBraking_8_taskComplete, MSDSpec_0_globalTime, enableBraking_3_objSysTaskComplete MSDSpec_0_globalTime MSDSpec_0_globalTime, emcyBraking_4_objSysSend, req_emcyBraking_11_send, emcyBraking_4_oneEvent req_enableBraking_8_consume, enableBraking_3_oneEvent, MSDSpec_0_globalTime, enableBraking_3_objSysConsume MSDSpec_0_globalTime enableBraking_3_oneEvent, enableBraking_3_objSysTaskStart, PU2_6_dispatch, MSDSpec_0_globalTime, req_enableBraking_8_taskStart MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime MSDSpec_0_globalTime enableBraking_3_oneEvent, req_enableBraking_8_taskComplete, MSDSpec_0_globalTime, enableBraking_3_objSysTaskComplete MSDSpec_0_globalTime MSDSpec_0_globalTime, emcyBraking_4_objSysSend, req_emcyBraking_11_send, emcyBraking_4_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBraking_11_receive, emcyBraking_4_objSysReceive, MSDSpec_0_globalTime, emcyBraking_4_oneEvent MSDSpec_0_globalTime emcyBraking_4_objSysConsume, req_emcyBraking_11_consume, MSDSpec_0_globalTime, emcyBraking_4_oneEvent MSDSpec_0_globalTime emcyBraking_4_objSysTaskStart, req_emcyBraking_11_taskStart, MSDSpec_0_globalTime, emcyBraking_4_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime, req_emcyBraking_11_taskComplete, emcyBraking_4_objSysTaskComplete, emcyBraking_4_oneEvent MSDSpec_0_globalTime MSDSpec_0_globalTime req_emcyBraking_11_receive, emcyBraking_4_objSysReceive, MSDSpec_0_globalTime, emcyBraking_4_oneEvent emcyBraking_4_objSysConsume, req_emcyBraking_11_consume, MSDSpec_0_globalTime, emcyBraking_4_oneEvent emcyBraking_4_objSysTaskStart, req_emcyBraking_11_taskStart, MSDSpec_0_globalTime, emcyBraking_4_oneEvent MSDSpec_0_globalTime, req_emcyBraking_11_taskComplete, emcyBraking_4_objSysTaskComplete, emcyBraking_4_oneEvent ######################

Java Simulator

The Java Simulator uses a hard-coded implementation of the semantics defined via ECL and MoCCML in order to simulate a given MSD specification. This approach is not as flexible as the direct execution in Gemoc (i.e. an adaption of the semantics requires reprogramming the simulator) but has a significantly higher performance. The java simulator is implemented as a Eclipse plugin that is contained in the dropings directory of the provided Eclipse instance.

Currently, the Java simulator only support the WCET simulation policy. That is, it postpones the occurrence of events until the last possible time step. However, additional simulation policies (e.g. BCET, Random, User Selection) are planed for future work.

Java Simulator Model

The plugin de.fraunhofer.iem.swt.msd.examples.ebeas_big contains an exemplarly MSD specification for the Java simulator. This specification consists of five collaboration with a total amount of 20 MSDs (de.fraunhofer.iem.swt.msd.examples.ebeas_big/ebeas_msdSpec). In order to simulate this model the five MSD collaboration must be merged to one collaboration and linked to the platform model.We describe these procedures in the following. Since they require some manual steps, we also provide the merged MSD specification (de.fraunhofer.iem.swt.msd.examples.ebeas_big/ebeas_msdSpec_merged).

MSD Merge (optional)

The MSD merge is implemented as a qvto transformation in the plugin MSDSpecMerge. It takes an MSD specification with several collaboration as input, merges the collaborations and creates an MSD specification with the merged collaboration. For more information on the MSD merge transformation please refer to the JavaSimulator documentation. Afterwards a platform model for the merged collaboration can be created with the TAM profile. The result should look like the model de.fraunhofer.iem.swt.msd.examples.ebeas_big/ebeas_msdSpec_merged.

Simulation

In order to start the Java simulator right-click on the model (ebeas_msdSpec_merged.uml) and select Java Simulation -> Start Simulation.

The output of the simulation is a .vcd file with the clock ticks. The name of the .vcd file is generated automatically and contains the current date and time. If this file is not displayed automatically in the package explorer, please click on refresh. The vcd file contains the clocks on the left. The clock ticks are visualized as pulses:

Please note that the simulation stops after approx. 650 timesteps. The reason is that the model contains a timing violation that is identified after 650 timesteps. In this case, the simulation stops and the user is notified by an entry in the Eclipse console.

The clocks that shall be visualized by the simulator can be selected by means of the ebeas_msdSpec_merged.filter file. For the concrete semantics of .filter files please refer to the JavaSimulator tutorial. Additionally, we also provide some pre-created traces (de.fraunhofer.iem.swt.msd.examples.ebeas_big/traces). This directory contains the following traces:

final_allClocks: vcd with all clocks that are created for the simulation
final_onlyEssentialClocks_complete: only the clocks that represent object system events
final_onlyEssentialClocks: a selection of the object system clocks

Home

Gemoc Simulator

Language Workbench

Modeling Workbench

MSD Models

Simulation

Exhaustive Simulation

Java Simulator

Java Simulator Model

MSD Merge (optional)

Simulation