Python Package Requirements
Step 4. Setup the IoTtalk Server
1. Enter the directory of the IoTtalk Server.
cd ~/<myname>-iottalk-docker
2. Modify the service definition YAML file docker-compose.yml.
vim docker-compose.yml
Please add the section given in Figure A.2 into the YAML file.
Line 1 ...
Line 2 services:
Line 3 ...
Line 4 BigraphTalk:
Line 5 image: bigraphtalk Line 6 ports:
Line 7 - 9720:9720 Line 8 networks:
Line 9 - iottalk-net Line 10 restart: on-failure Line 11 volumes:
Line 12 - bigraph:/bigraphtalk Line 13 AFLtalk:
57
Line 23 VerificationTalk:
Line 24 image: verificationtalk
Figure A.2 Service Definition YAML File docker-compose.yml of IoTtalk Server.
Step 5. Start up the VerificationTalk Subsystem with IoTtalk Server
1. Run the container of the service (including VerificationTalk Subsystem) provided by IoTtalk Server.
docker-compose up
Finally, the current version of IoTtalk Server supports the verification mechanism, which can verify the correctness of the IoTtalk application.
58
Appendix B.
Format of Message from IoTtalk to BigraphTalk
Figure B.1 shows the message format sent from IoTtalk to BigraphTalk via socket. This JSON-format message represents the information related to the configuration of the project to be verified. It has three keys Device_List, Join_List, and Forbidden_Configuration [6].
The value corresponding to the key Device_List is an array of devices that build the project [6]. We encode each device into the JSON-format data which has three keys
Device_Id, Device_Model, and DF_List. Device_Id is a unique identifier for the device in the
IoTtalk system [6]. Device_Model is the name of the device model of the device. DF_List is an array of the device features of the device [6]. Each element in the array represents the attributes of the device feature. If the DF_Parameter does not have the maximum or minimum value, we will omit the corresponding attribute [6].The value corresponding to the key Join_List is an array of Joins that connect the devices in the project [6]. The information of Joins is encoded into the JSON-format data, which has three keys Join_Id, Join_Fn, and Devices. Each Join has a unique Join_Id and a function described by the JSON-format value corresponding to the key Join_Fn [6]. A join function has a unique identifier Fn_Id and the description Fn_Input/Fn_Output for its input/output [6]. The value corresponding to the key Devices uses arrays of device features to denote the connection of the Join [6].
The value corresponding to the key Forbidden_Configuration is an array of forbidden configurations which only involve the devices in the project [6]. The information of forbidden configurations is encoded into the JSON-format data, which has two keys FC_name and Data.
FC_name is the name of the forbidden configuration. The value corresponding to the key Data is an array. Each element of this array designates a particular device feature. If a forbidden configuration involves several device features of the same device, then we assign the same Device_Id to them [6]. If a forbidden configuration involves the same device feature of
59
several distinct devices, we assign different Device_Id to them [6].
Line 1 {
60
Figure B.1 JSON object sent from IoTtalk to BigraphTalk.
61
Appendix C.
Format of Message from BigraphTalk to IoTtalk
Figure C.1 shows the message format sent from BigraphTalk to IoTtalk via socket. This array-format message expresses the information about errors found by BigraphTalk. If BigraphTalk does not detect any error, then IoTtalk will receive an empty array [6]. Each error is encoded into the JSON-format data, which has three keys Error_Type, Error_Msg, and
Data. Error_Type is one of “Forbidden Configuration”, “Possible Forbidden Configuration”,
“Type Mismatch”, “Missing Argument”, and “Parameter Mismatch” [6]. Error_Msg gives the detailed text information. The value corresponding to the key Data is an array. Each element of this array indicates the problematic connection with the corresponding Join and device feature [6].
Line 1 [{
Line 2 'Error_Type': error_type, Line 3 'Error_Msg': error_message, Line 4 'Data': [{
Line 5 'Join_Id': join_id, Line 6 'Device': {
Line 7 'Device_Id': device_id, Line 8 'DF_Name': df_alias_name Line 9 }
Line 10 }, Line 11 ...]
Line 12 }, Line 13 ...]
Figure C.1 JSON object sent from BigraphTalk to IoTtalk.
62
Appendix D.
Forbidden Configuration Management Procedures
When a user sends a request, the BigraphTalk Event Handler redirects the requests to the corresponding procedures in Forbidden Configuration Module to store or query the data, and returns the retrieved data. Table D.1 lists the procedures that support CRUD operations on forbidden configuration.
Procedure Rule Input and
Output Description Table D.1 Forbidden Configuration Management Procedures.
63
Appendix E.
Format of Message from IoTtalk to AFLtalk
Figure E.1 shows the HTTP message format sent from IoTtalk to AFLtalk. This JSON-format message represents the information related to the join functions to be tested. It has one key Join_List. The value corresponding to the key Join_List is an array of Joins that connect the devices in the project. The information of Joins is encoded into the JSON-format data, which has two keys Join_Id and Join_Fn. Each Join has a unique Join_Id and a function described by the JSON-format value corresponding to the key Join_Fn. A join function has a unique identifier Fn_Id, the function code, and the description Fn_Input/Fn_Output for its input/output.
64
Line 23 ...]
Line 24 }
Figure E.1 JSON object sent from IoTtalk to AFLtalk.
65
Appendix F.
Format of Message from AFLtalk to IoTtalk
Figure F.1 shows the HTTP message format returned from AFLtalk to IoTtalk. This JSON-format message expresses the information about the errors found by AFLtalk. The value corresponding to the key Result is an array. Each element of this array is the JSON-format data with three keys Join_Id, Crash, and Hang, which represents the testing result of join functions. Join_Id indicates which Join applies the join function. The value corresponding to the key Crash and Hang are arrays that record the input causing the error.
Line 1 {
Line 2 'Result': [{
Line 3 'Join_Id': join_id,
Line 4 'Crash': [crash_input, ...], Line 5 'Hang': [hang_input, ...]
Line 6 }, Line 7 ...]
Line 8 }
Figure F.1 JSON object returned from AFLtalk to IoTtalk.
66