Difference between pages "Tool user manual" and "TASTE Communication Device"

From TASTE
(Difference between pages)
Jump to: navigation, search
 
 
Line 1: Line 1:
== User Manual Dummy Model ==
+
== Introduction ==
 +
CommunicationDevice (CD) is a new type of TASTE project, that allows to model low level system drivers and integrate CD driver with existing or new TASTE project. It comes with two pre-defined templates: Broker and Broker + Packetizer. Depending on a selected template CD allows to model either Broker or Broker and Packetizer communication components. CommunicationDevice is a part of the SpaceCreator and Kazoo projects.
  
This User Manual explains how to create different types of properties (Boolean Stop Conditions, Message Sequence Charts and SDL Observers) within a simplified TASTE model, and how to run the Model-Checker with each of them to evaluate the verification results. The User Manual Dummy model is composed of a GUI component (Environment) and two SDL functions (Function 2 and Function 3).
+
== Capabilities ==
 +
The following functionalities are supported:
 +
* creation of new CD project from QTC wizard – SpaceCreator
 +
* modeling and implementation of broker and packetizer
 +
* CD code generation done be Kazoo templates
 +
* integration with full TASTE project
  
:[[File:ClipCapIt-220607-114021.PNG]]
+
==How to create CD project==
 +
Communication device project can be created form QT Creator wizard that can be opened with TASTE command. Then under File->New File or Project (Ctrl + N)
 +
[[File:Cd_wizard_2.png]]
  
The state machines of Function 2 and Function 3 are depicted in the following figures:
 
  
:[[File:ClipCapIt-220607-114752.PNG]]
+
Non-Qt Project -> Communication Device Project
  
 +
[[File:Cd wizard 1.png]]
  
In order for Function 2 to transition to Cmd state, it first needs to receive 3 consecutive status messages with true values. When a false value is received, counter is reset to 0 and it starts again. When Cmd state is reached, it continues receiving status messages from the Environment and will only proceed with the triggering of the command interface when a true value for status is received, resetting counter to 0 and transitioning back to Wait state after command is triggered.
 
  
:[[File:ClipCapIt-220607-114824.PNG]]
+
CD wizard starts with “Project Location” tab. User shall provide Name for the project and path under which project will be created.
  
When Function 3 receives the status parameter through the command interface from Function 2, it checks whether its value is true or false. Since Function 2 only triggers the command interface when status value is true, status value that Function 3 receives should always have a true value. If the value received is that of false, Function 3 enters an Error state. Upon reception of a true status value, Function 3 triggers tm interface sending to the Environment component the status parameter.
+
[[File:Cd_wizard_3.png]]
  
== Properties Definition and Model-Checking ==
+
Next tab “Project Initialization” provides capabilities of selecting interface view template and CD board. Under IV template either “Broker” or “Broker_Packetizer” can be selected. Under Communication Device board either “x86 Linux CPP” or “SAM V71 FreeRTOS N7S” can be selected.
The Model-Checking wizard can be accessed from the Space Creator interface view GUI through its dedicated MC icon on the bottom left side:
+
 
:[[File:ClipCapIt-220607-115116.PNG]]
+
[[File:Cd_wizard_4.png]]
Once MC icon is clicked, the Model-Checking Wizard will open displaying this window:
+
 
:[[File:ClipCapIt-220607-115123.PNG]]
+
Next tab is standard “Kit Selection” tab.
By right-clicking on the properties folder, a window is displayed allowing the user to select the type of property to be created from a drop-down list:
+
 
**Update picture**
+
[[File:Cd_wizard_5.png]]
Each of the following subheadings describes the process for the creation, definition and model-checking of each of the 3 different property types considered.
+
 
=== Boolean Stop Conditions (BSC) ===
+
Under last tab that is “Project Management” version control can be added. Also wizard displays all files that will be added to Communication Device project.
To create a Boolean Stop Condition property, one must select “Boolean Stop Condition – Observer” from the New Property drop-down list:
+
 
**Update figure**
+
[[File:Cd_wizard_6.png]]
Once created and given a name, it will appear within the Properties folder on the left. In order to edit it, one must double click on the .pr file of the BSC property:
+
 
:[[File:ClipCapIt-220607-115434.PNG]]
+
===Generated CD project files details===
The following template will be displayed for the definition of the Boolean Stop Condition:
+
Communication Device Project wizard adds the following files to the project:
:[[File:ClipCapIt-220607-115450.PNG]]
+
* taste.pro – empty taste.pro file that will be automatically generated during build
The following BSC is created for the User Manual Dummy model, based on this template:
+
* Makefile – entry build and clean procedure that includes Kazoo and SC dependencies definitions
:[[File:ClipCapIt-220607-115511.PNG]]
+
* deploymentvew.dv.xml – predefined deploymentview.dv.xml that includes CD build partition
This Boolean Stop Condition aims to verify that the maximum allowed value for counter parameter defined for Function 2 is 3, so that a value of 4 can never be encountered. If a value of 4 is encountered, then the Model-Checking of this property will lead to the encountering of error scenarios as it will trigger the stop condition.
+
* interfaceview.xml – interfaceview with Broker, Packetizer and interfaces. In this file user shall model Broker or Broker and Packetizer (depending on a template) along with required and provided components interfaces .
Once the BSC property is defined, the next step is to select it by checking the property .pr file check box and configure the Model-Checker. The verification configuration can be set through the IF model-checker tab displayed at the top of the Model Checking Wizard:
+
* <project name>.acn – ACN project model for custom binary encoding rules.
:[[File:ClipCapIt-220607-115533.PNG]]
+
* <project name>.asn – ASN non user-editable model that contains all the basic data types.
The first option the user can select is the type of scenario the Model-Checker shall look into: either error or success scenarios, or both. Since Boolean Stop Conditions model error scenarios, just error scenarios check box is selected.
+
* <project name>.pro/shared – QTC project files with custom user build settings.
The next fields refer to:
+
* <project name>configuration.acn - ACN project configuration model for custom binary encoding rules.
*The maximum number of scenarios that the Model-Checker will display as an output (a default value of 5 is selected).
+
* <project name>configuration.asn - ASN user-editable model that contains definition of Driver Configuration. This file will be used by ocarina-components.aadl and Board1.xml and shall be implemented by the user.
*The time limit for the exploration (a default value of 120 seconds is selected).
+
* <project name>privatedata.acn - ACN project privatedata model for custom binary encoding rules.
*The exploration algorithm, either Depth First Search (DFS) or Breadth First Search (BFS). The former is recommended.
+
* <project name>privatedata.asn - ASN user-editable model that contains definition of Private Data structure. This type shall be used in main.c[pp] to indicate the type of the variable that is passed as a private pointer to the driver. Shall be implemented by the user.
Additional optional fields allow the user to select the maximum number of environment calls and the maximum number of states to explore. None of these fields have been considered for the model-checking of this property.
+
 
Once the user has configured the verification setting, the Model-Checker can be ran by clicking Call IF button. A terminal window will open, displaying the following at the end of the verification execution:
+
==Exemplary CD broker and packetizer modeling and implementation==
:[[File:ClipCapIt-220607-115623.PNG]]
+
Based on selected CD “Interface view template” either broker or broker and packetizer can be modeled and implemented. In this example second template will be used.  
This terminal window shows the time it has taken for the Model-Checker to execute (0 s), the number of states explored (2325) and the number of transitions (2955). If any error scenarios were encountered, they would have appeared in this window. Note that for the verification of this property, no error scenarios have been identified, confirming the correct behavior of the system design.
+
 
:[[File:ClipCapIt-220607-115642.PNG]]
+
===CD IV file specifics – fixed system elements===
To provide the reader with an idea of what an actual encountering of error scenarios when model-checking a Boolean Stop Condition would look like, BSC-1 has been modified so that now the Error state will be triggered by a counter value of 3 instead of 4. If running the Model-Checker with the same exact configuration the following results are obtained:
+
After opening IV file in the editor user can find (depending on selected template) Broker and Packetizer components. These are virtual components that are not taken for final code generation. Purpose of those elements is to provide “must have” set of interfaces. Those are required to match newly created and modeled communication components to existing in TASTE runtime calls.
:[[File:ClipCapIt-220607-115720.PNG]]
+
 
Now, one error scenario has been obtained, with a very quick execution of the model-checker as it has only explored 39 states and 46 transitions, with a verification time of 0 s. In order to analyse this error scenario, the Model-Checking execution terminal windows shall be first closed. The generated error scenarios will appear under the output folder in the IF model-checker tab:
+
[[File:Cd_broker_pack_iv_1.png|1100px]]
:[[File:ClipCapIt-220607-115740.PNG]]
+
 
By clicking on model_bsc_1_e1msc, the associated transformed Message Sequence Chart can be reviewed:
+
User can’t remove those element neither the interfaces and will be informed about that while trying to do so.
:[[File:ClipCapIt-220607-115755.PNG]]
+
 
Indeed, it can be seen how 3 consecutive true values for status message have been received by Function 2, and thus counter parameter reaching a value of 3, effectively triggering the stop condition.
+
[[File:Cd_broker_pack_iv_2.png]]
=== Message Sequence Charts (MSC) ===
+
 
To create a Message Sequence Chart property, one must select “Message Sequence Chart” from the New Property drop-down list:
+
===Modeling Packetizer component===
**Update figure**
+
While modeling Packetizer user shall provide a TASTE function that implements needed interfaces and connect that function to pre-defined virtual Packetizer component. Also each interface shall contain set of input and output parameters. The easiest way to do so is by dragging each interface from virtual Packetizer with left Ctrl key pressed and drop it on custom function. This way each interface will be copied along with set of parameters.
Once created and given a name, it will appear within the Properties folder on the left. In order to edit it, one must double click on the .msc file of the MSC property:
+
 
:[[File:ClipCapIt-220607-115916.PNG]]
+
[[File:Cd_broker_pack_iv_3.png|1100px]]
The following template will be displayed for the definition of the Message Sequence Chart:
+
 
:[[File:ClipCapIt-220607-115937.PNG]]
+
 
A description of all the possible property type combinations and their meaning is provided in the note. Property-type field shall be specified according to the described Usage, where [] concepts are optional and () are mandatory.
+
[[File:Cd_pack_params_1.png|t300px]]
The following MSC was created for the User Manual Dummy model, based on this template:
+
[[File:Cd_pack_params_2.png|500px]]
:[[File:ClipCapIt-220607-115955.PNG]]
+
 
This Message Sequence Chart is defined as search unintended. This means that the Model Checker will try to find at least one execution with this sequence, representing an undesired behavior of the system. Indeed, command interface will only be triggered upon reception of a true status message value from the Environment GUI, so it is expected that the Model-Checker will not find this sequence in any of the executions.
+
To avoid build errors another function can be connected to Broker and it’s implementation is not required.
Once the MSC property is defined, the next step is to select it by checking the property .msc file check box and configure the Model-Checker. The verification configuration can be set through the IF model-checker tab displayed at the top of the Model Checking Wizard:
 
:[[File:ClipCapIt-220607-120009.PNG]]
 
The first option the user can select is the type of scenario the Model-Checker shall look into: either error or success scenarios, or both. Since MSC-1 type is Search Unintended, only Error scenarios are checked so that if any is found they can be further analysed.
 
The next fields refer to:
 
*The maximum number of scenarios that the Model-Checker will display as an output (a default value of 5 is selected). This number includes both error and success scenarios.
 
*The time limit for the exploration (a default value of 120 seconds is selected).
 
*The exploration algorithm, either Depth First Search (DFS) or Breadth First Search (BFS). The former is recommended.
 
Additional optional fields allow the user to select the maximum number of environment calls and the maximum number of states to explore. None of these fields have been considered for the model-checking of this property.
 
Once the user has configured the verification setting, the Model-Checker can be ran by clicking Call IF button. A terminal window will open, displaying the following at the end of the verification execution:
 
:[[File:ClipCapIt-220607-120033.PNG]]
 
This terminal window shows the time it has taken for the Model-Checker to execute (0 s), the number of states explored (1083) and the number of transitions (1310). If any error scenarios were encountered, they would have appeared in this window. Note that for the verification of this property, no error scenarios have been identified, confirming the correct behavior of the system design.
 
:[[File:ClipCapIt-220607-115642.PNG]]
 
To provide the reader with an idea of what an actual encountering of success scenarios when model-checking a Message Sequence Chart would look like, a second MSC has been defined with search intended type:
 
:[[File:ClipCapIt-220607-120103.PNG]]
 
MSC-2 models a desired behaviour of the system which consists in receiving three consecutive true status message values from Environment to Function 2, which is the condition that needs to be met for the latter to transition into Cmd state. Thus, the expected verification results is the encountering of at least one success scenario.
 
The verification configuration is identical to that of MSC-1 but looking for Success Scenarios rather than for Error Scenarios. The following results are then obtained when running the Model-Checker for MSC-2:
 
:[[File:ClipCapIt-220607-120129.PNG]]
 
A total of four success scenarios have been obtained. In order to analyse these success scenarios, the Model-Checking execution terminal windows shall be first closed. The generated success scenarios will appear under the output folder in the IF model-checker tab:
 
:[[File:ClipCapIt-220607-120142.PNG]]
 
By clicking on model_bsc_1_s1msc, the associated transformed Message Sequence Chart can be reviewed:
 
:[[File:ClipCapIt-220607-120200.PNG]]
 
Indeed, it can be seen how 3 consecutive true values for status message have been received by Function 2. This property is equivalent to the previously modified BSC-1 in which the stop condition was the counter reaching a value of 3.
 
=== SDL Observers (OBS) ===
 
To create an SDL Observer property, one must select “Observer” from the New Property drop-down list:
 
:[[File:ClipCapIt-220607-120241.PNG]]
 
Once created and given a name, it will appear within the Properties folder on the left. In order to edit it, one must double click on the .pr file of the OBS property:
 
:[[File:ClipCapIt-220607-120254.PNG]]
 
The following template will be displayed for the definition of an Observer:
 
:[[File:ClipCapIt-220607-120308.PNG]]
 
The following OBS is created for the User Manual Dummy model based on this template:
 
:[[File:ClipCapIt-220607-120327.PNG]]
 
This Observer property aims to identify if Function 3 ever enters into an Error state upon triggering of command interface from Function 2.
 
Once the OBS property is defined, the next step is to select it by checking the property .pr file check box and configure the Model-Checker. The verification configuration can be set through the IF model-checker tab displayed at the top of the Model Checking Wizard:
 
:[[File:ClipCapIt-220607-120353.PNG]]
 
The first option the user can select is the type of scenario the Model-Checker shall look into: either error or success scenarios, or both. For this Observer property, both success and error scenarios are selected.
 
The next fields refer to:
 
*The maximum number of scenarios that the Model-Checker will display as an output (a default value of 5 is selected).
 
*The time limit for the exploration (a default value of 120 seconds is selected).
 
*The exploration algorithm, either Depth First Search (DFS) or Breadth First Search (BFS). The former is recommended.
 
Additional optional fields allow the user to select the maximum number of environment calls and the maximum number of states to explore. None of these fields have been considered for the model-checking of this property.
 
Once the user has configured the verification setting, the Model-Checker can be ran by clicking Call IF button. A terminal window will open, displaying the following at the end of the verification execution:
 
:[[File:ClipCapIt-220607-120419.PNG]]
 
This terminal window shows the time it has taken for the Model-Checker to execute (0 s), the number of states explored (60) and the number of transitions (71). Only success scenarios have been encountered (1), confirming the correct behaviour of the system.
 
The generated success scenario will appear under the output folder in the IF model-checker tab:
 
:[[File:ClipCapIt-220607-120433.PNG]]
 
By clicking on model_obs_1_s1msc, the associated transformed Message Sequence Chart can be reviewed:
 
:[[File:ClipCapIt-220607-120447.PNG]]
 
Indeed, it can be seen how the command interface is triggered upon reception of a true status message value, rather than upon reception of a false value.
 

Revision as of 17:24, 29 November 2022

Introduction

CommunicationDevice (CD) is a new type of TASTE project, that allows to model low level system drivers and integrate CD driver with existing or new TASTE project. It comes with two pre-defined templates: Broker and Broker + Packetizer. Depending on a selected template CD allows to model either Broker or Broker and Packetizer communication components. CommunicationDevice is a part of the SpaceCreator and Kazoo projects.

Capabilities

The following functionalities are supported:

  • creation of new CD project from QTC wizard – SpaceCreator
  • modeling and implementation of broker and packetizer
  • CD code generation done be Kazoo templates
  • integration with full TASTE project

How to create CD project

Communication device project can be created form QT Creator wizard that can be opened with TASTE command. Then under File->New File or Project (Ctrl + N) Cd wizard 2.png


Non-Qt Project -> Communication Device Project

Cd wizard 1.png


CD wizard starts with “Project Location” tab. User shall provide Name for the project and path under which project will be created.

Cd wizard 3.png

Next tab “Project Initialization” provides capabilities of selecting interface view template and CD board. Under IV template either “Broker” or “Broker_Packetizer” can be selected. Under Communication Device board either “x86 Linux CPP” or “SAM V71 FreeRTOS N7S” can be selected.

Cd wizard 4.png

Next tab is standard “Kit Selection” tab.

Cd wizard 5.png

Under last tab that is “Project Management” version control can be added. Also wizard displays all files that will be added to Communication Device project.

Cd wizard 6.png

Generated CD project files details

Communication Device Project wizard adds the following files to the project:

  • taste.pro – empty taste.pro file that will be automatically generated during build
  • Makefile – entry build and clean procedure that includes Kazoo and SC dependencies definitions
  • deploymentvew.dv.xml – predefined deploymentview.dv.xml that includes CD build partition
  • interfaceview.xml – interfaceview with Broker, Packetizer and interfaces. In this file user shall model Broker or Broker and Packetizer (depending on a template) along with required and provided components interfaces .
  • <project name>.acn – ACN project model for custom binary encoding rules.
  • <project name>.asn – ASN non user-editable model that contains all the basic data types.
  • <project name>.pro/shared – QTC project files with custom user build settings.
  • <project name>configuration.acn - ACN project configuration model for custom binary encoding rules.
  • <project name>configuration.asn - ASN user-editable model that contains definition of Driver Configuration. This file will be used by ocarina-components.aadl and Board1.xml and shall be implemented by the user.
  • <project name>privatedata.acn - ACN project privatedata model for custom binary encoding rules.
  • <project name>privatedata.asn - ASN user-editable model that contains definition of Private Data structure. This type shall be used in main.c[pp] to indicate the type of the variable that is passed as a private pointer to the driver. Shall be implemented by the user.

Exemplary CD broker and packetizer modeling and implementation

Based on selected CD “Interface view template” either broker or broker and packetizer can be modeled and implemented. In this example second template will be used.

CD IV file specifics – fixed system elements

After opening IV file in the editor user can find (depending on selected template) Broker and Packetizer components. These are virtual components that are not taken for final code generation. Purpose of those elements is to provide “must have” set of interfaces. Those are required to match newly created and modeled communication components to existing in TASTE runtime calls.

Cd broker pack iv 1.png

User can’t remove those element neither the interfaces and will be informed about that while trying to do so.

Cd broker pack iv 2.png

Modeling Packetizer component

While modeling Packetizer user shall provide a TASTE function that implements needed interfaces and connect that function to pre-defined virtual Packetizer component. Also each interface shall contain set of input and output parameters. The easiest way to do so is by dragging each interface from virtual Packetizer with left Ctrl key pressed and drop it on custom function. This way each interface will be copied along with set of parameters.

Cd broker pack iv 3.png


t300px Cd pack params 2.png

To avoid build errors another function can be connected to Broker and it’s implementation is not required.