Sage Journals: Discover world-class research

Abstract

A cyber-physical system is an integration of computation, networking, and physical processes. This article introduces a novel physical control framework to integrate various devices to form the lower-level abstraction network. Two relevant protocols within this framework are proposed for information exchange between different network environments. Furthermore, a formal verification method for the proposed protocols is discussed. The model-checking tool SPIN is used to model and formally verify such protocols. The properties of the protocols are expressed using linear temporal logic to enable model-checking. Implementation results are presented to provide a deeper understanding of the proposed protocols.

Keywords

Cyber-physical system formal verification Zigbee constrained application protocol Internet of Things

Introduction

A cyber-physical system (CPS)¹ connects the physical world objects and computing systems. However, the embedded systems in CPSs have limited computation and storage capabilities. Cloud computing has been quite successful in integrating several application areas including on-demand data centers, remote processing and storage, big data analytics, and resource virtualization. Hence, combining cloud computing with CPS is a new direction for industrial applications.² In cloud manufacturing environments, it is important to have monitoring capability to detect any exception cases in different sites. Wireless sensor networks (WSN) can help to sense, inspect, and gather the information of cloud manufacturing environments.

A generic platform is needed to integrate heterogeneous monitoring resources and devices into cloud CPS. In this work, first, we present a novel physical control framework (PCF) to integrate different networks and devices. Next, we propose two protocols for supporting visiting Zigbee nodes using constrained application protocol (CoAP). We specify the models of the two protocols to perform formal verification using SPIN³ model-checking tool. In the past, we have already presented our concept along with an initial model-checking.⁴ In this expanded article, we elaborate on the concept, add the protocol implementation for information exchange between Zigbee and CoAP networks. Finally, PCF is implemented as a Web-of-Things (WoT) solution for resource-constrained devices.

The rest of the article is organized as follows. In the “Related work” section, we summarize the existing methods of connecting a WSN with TCP/IP networks. A brief introduction to the verification tool used in our experiment is given in section “Formal verification tool.” Next, our proposed solution is presented in section “PCF.” Section “Communication conversion protocols” gives a detailed introduction of the two adaptation protocols named device network access protocol (DNAP) and device control transmission protocol (DCTP), to bridge a Zigbee network and a CoAP network together in the framework. Simulation and verification methods of the two protocols are discussed in section “Simulation and verification.” A security communication way is proposed in section “Security.” Implementation results on the hardware platform are presented in section “Implementation.” Finally, conclusions are presented in section “Conclusion and future works.”

Related work

How to connect a WSN to a traditional TCP/IP network is the first challenge for cloud CPS. Oil and gas companies traditionally use wired-gas sensing systems because of their reliability and robustness. Due to the evolution of digital technologies and wireless communications, a WSN can be an alternate sensing solution for the oil and gas industry.⁵ Chao et al.⁶ provided an analysis regarding the ways in which a WSN can be used in developing a toxic gas monitoring system. Aliyu et al.⁷ provided a Zigbee technology–based gas safety and monitoring system. However, such solutions isolated the WSN from the TCP/IP network.

Recent technology trend is to connect a WSN to the wider Internet over TCP/IP connections. The 6LoWPAN concept originated from the idea that the Internet protocol could and should be applied even to the smallest devices.⁸ The 6LoWPAN defines a method for the IPv6 packets to be carried on top of low-power and lossy networks (LLNs). The 6LoWPAN uses the IEEE 802.15.4 standard. Currently, some model systems are using 6LoWPAN to join WSN and IP networks together. The E-SURAKSHAK⁹ is an example of one such CPS system related to healthcare, and its end-to-end bidirectional Internet connectivity is provided by 6LoWPAN.

UDP is a more suitable transport layer protocol for communication and real-time data transfer in sensor data acquisition and remote control application scenarios. Hence, most of the Internet of Things (IoT) communication networks mainly use UDP at the transport layer. At the application layer, there is also a need for a protocol to integrate real-world sensor devices to the Web. Modeling sensors’ RESTful resources can offer services to the world using the HTTP protocol. Dillon et al.¹⁰ analyzed the use of web in IoT with a CPS system, and provided a novel WoT framework for CPSs. Raggett¹¹ summarized the implementation challenges and security problems associated with the conversion from IoT to WoT. Most WoT implementations focus on the data exchange at the application layer, and they also need to take into account the reliance of the IP layer. Most RESTful approaches are based on the HTTP protocol, but that would be too complex for smart devices. The Internet Engineering Task Force (IETF) established the constrained RESTful environments (CoRE) working group to realize the REST architecture in LLNs. This group offers solutions for the embedded web servers in constrained smart devices. One cloud application uses CoAP¹² to communicate with the web services deployed on a smart device, in a similar manner as using HTTP. Each resource still corresponds to a unique universal resource identifier (URI). A research survey and analysis related to CoAP is presented in Villaverde et al.,¹³ and it was concluded that CoAP is better suited for LLNs compared to other RESTful protocols as it introduces lower overhead and minimizes delays while maintaining reliability. The work of Thombre et al.¹⁴ evaluates the performance of the CoAP stack on a device using the Contiki OS and Cooja simulator in a 5-hop LLN. Cho et al.¹⁵ proposed a system to allow communication between HTTP and CoAP networks. Sheng et al.¹⁶ proposed a framework including an efficient device management solution for WSN based on CoAP. The underlying network of this framework is based on 6LoWPAN. However, none of the existing works address the problem of integrating a WSN with CoAP in a Zigbee environment.

The work of Mitsugi et al.¹⁷ proposed a framework to implement UPnP over Zigbee network, and to facilitate end-to-end HTTP communication between Zigbee and IP networks. This work used CoAP as the bridge protocol. The proposed solution required that the sensor MCU associated with the Zigbee transceiver can handle CoAP messages. This solution approach is not suitable for Zigbee devices that cannot run CoAP stack. However, our proposed solution overcomes this drawback.

The authors of the White Paper¹⁸ recommend using a Zigbee gateway between Zigbee networks and IP networks such as the Internet. This solution required that the Zigbee gateway must allow interactions between IP applications and the applications on Zigbee devices, and provided an extensible set of RPC protocols (SOAP, REST, and GRIP). But this article does not describe the CoAP binding method for REST-styled services.

To address the above-mentioned problem, we propose a new binding method for CoAP. Our solution can fulfill the features specified in Zigbee Alliance White Paper,¹⁸ related to addressing core IP connectivity, and connecting the Zigbee networks to IP networks or remote applications. The proposed framework can scale easily, and there is no need to use CoAP stack on every Zigbee endpoint device. A new Zigbee device can join an LLN without any constraints and register itself by sending requests using the DNAP format. This fulfills the requirement of Zigbee Alliance White Paper¹⁸ in terms of enabling web service for every Zigbee device based on CoAP.

CoAP provides an Observing method,¹⁹ allowing servers to send every resource state change to interested clients in an active manner. The Observe function offers the possibility for a client to have an up-to-date representation of the resource without the client having to constantly poll for information regarding the new changes. Compared to the HTTP, this feature is an enhancement for CoAP. For this reason, we design a timing mode to implement the Observe function in Zigbee networks.

We try to find a formal specification and model verification method for protocol used in IoT. The research work of Aziz²⁰ presents a formal model of the MQTT protocol based on a timed process algebra called TPi. The authors also present a statistical analysis by manually limiting the number of copies of input variables. This approach is an abstract way to simplify the analysis of the MQTT protocol and has weak describing ability compared to model-checking tools. Model-checking technology becomes increasingly prominent in industrial practice. There are some tools for model-checking, with different capabilities suited to different kinds of problems. For example, the tools SLAM and BLAST are only used for performing statistical analysis of sequential C programs to check safety properties. The SPIN tool focuses on interaction between processes, and SPIN can also check liveness property of the protocols. In this sense, SLAM and BLAST are only supporting a subset of the functionalities covered by SPIN. The KRONOS aims to verify real-time systems and is dedicated to observation of real-time properties. KRONOS introduces clock into system states, which makes the verification of untimed temporal properties much less efficient than SPIN.

The work of Capella et al.²¹ proposes a reference model to standardize a variety of WSN monitoring platforms which are used to gather information about processing condition of an IoT system. Our PCF can be used as the implementation of an off-the-shelf component for this model. The control gateway can be used as a sniffer to capture the WSN messages for the interchange layer, and the PCF can be an off-the-shelf component to obtain information in a standard way for the information layer.

Formal verification tool

The SPIN tool can be used for the formal verification of asynchronous process systems or protocols. We choose it to trace any logical design errors in our proposed protocol. During the validation process, it supports all correctness requirements expressible using linear temporal logic (LTL)²² formulas.

The LTL is a modal temporal logic with modalities referring to time. The LTL is built up from a finite set of propositional variables $A$ , the logical operators set {¬,∧,∨,→,↔}, and the temporal modal operators set ${[] (always)$ , $< > (eventually)$ , $N (next)$ , $U (until)$ , $W (weaklyuntil)}$ . The symbol ⊧ denotes “satisfy.”

Definition 1. Formally, the set of LTL formulas over $A$ is inductively defined as follows:

$True$ and $False$ both are LTL formulas;

If $p \in A$ , then $p$ is an LTL formula;

$\neg Ψ, Ψ \land Φ, Ψ \lor Φ$ , $Ψ \to Φ$ , $Ψ \leftrightarrow Φ$ , $[] Ψ$ , $< > Ψ$ , $N Ψ$ , $Ψ U Φ$ , and $Ψ W Φ$ are LTL formulas if and only if (iff) $Ψ$ and $Φ$ are LTL formulas.

Definition 2. Let $AP$ be a non-empty set of atomic propositions. A Kripke structure is a four-tuple defined as

$M = (S, s_{0}, R, L)$ , where

$S$ is a finite set of states;

$s_{0} \in S$ is an initial state;

$R \subseteq S \times S$ is a transition relation, for which it holds that $\forall s \in S, \exists s' \in S, and (s, s') \in R$ ;

$L : S \to 2^{AP}$ is a function which labels each state with the atomic propositions which hold true in that state.

A finite transition system is a Kripke structure of $M = (S, s_{0}, R, L)$ . An execution of the finite transition system is an infinite sequence of its states $π = s_{0}, s_{1}, s_{2} . . .$ called path, where $\forall s_{i} \in S, (s_{i}, s_{i + 1}) \in R, and π^{i} = s_{i}, s_{i + 1}, s_{i + 2} . . .$ .

Definition 3. Suppose $M = (S, s_{0}, R, L)$ is Kripke Structure and $π = s 0, s 1, s 2 . . .$ is a path in $M$ , the relation $π ⊧ f$ is defined inductively as follows:

$π ⊧ p$ iff $p \in L (π_{0}), p \in AP$ ;

$π ⊧ \neg Ψ$ iff not $π ⊧ Ψ (π ⊭ Ψ)$ ;

$π ⊧ Ψ \lor Φ$ iff $π ⊧ Ψ$ or $π ⊧ Φ$ ;

$π ⊧ Ψ \land Φ$ iff $π ⊧ Ψ$ and $π ⊧ Φ$ ;

$π ⊧ N Ψ$ iff $π^{1} ⊧ Ψ$ ( $π^{1} = s_{1}, s_{2} . . .$ , in the next time step $Ψ$ must be true);

$π ⊧ Φ U Ψ$ if $\exists i \geq 0, π^{i} ⊧ Ψ$ and $\forall k, 0 \leq k < i, π^{k} ⊧ Φ$ .

Thus, an LTL formula $f$ holds in $s$ if and only if it holds for all paths starting at $s$ . If a formula $f$ holds in $s_{0}$ , it is denoted by $M ⊧ f$ .

We use SPIN to verify the protocols’ general properties of reachability, deadlock freeness, livelock freeness, termination, and consistency. For this purpose, correctness requirements expressions in LTL are used with SPIN to trace the model of our data communication protocols in PCF.

PCF

PCF is a framework to integrate different devices and LLNs together. Figure 1 shows the details of the PCF model. PCF hides device implementation details from the higher-level application, and provides logical interfaces for physical objects. Based on IP protocol, PCF offers uniform access interface constituted by physical control unit (PCU), CPS control gateway layer, and heterogeneous LLNs. With overlay network technologies, PCF can be extended or shortened on demand and make the control crossing physical boundaries between network devices. All control-related operations are executed by the physical control point (PCP).

Figure 1.

Physical control framework.

PCU

PCU is an access and control sub-platform for device control. PCU receives the task descriptions from the application layer, and manages the device registrations and cancelations as a generic access network controller. PCU follows the instructions from the application to provide synchronous and asynchronous control for specific devices and assigns them to the corresponding PCPs.

Device control command conversion module

Device control command conversion module (DCM) transforms an application layer command to a control command for the devices. At the application layer, CPS has no need to consider the underlying differences among devices and subnets. Application processes use a unified scripting language to describe the details of a task and data scheme. DCM transforms the scripting language into an appropriate hardware platform task description language. So, the underlying network will be transparent to the higher-level application in the CPS.

CPS control gateway

The CPS control gateway acts as a connector between the PCU and the underlying heterogeneous networks. Devices can connect to the CPS control gateway through Zigbee interfaces. Once the communication occurs between a sensing domain protocol and a network domain protocol, the gateway needs to execute a protocol conversion. With the action of PCP, the CPS gateway could translate the data in the CoAP format from the side of computer network to another format on the WSN side.

If the clients on the Internet use HTTP instead of CoAP, the HTTP-CoAP proxy²³ can be deployed in the PCF.

Physical control point

A PCP receives an applications control command in CoAP format and forms a control message with the DCTP format. Next, the PCP sends the message to a destination device. The CPS control gateway works with the PCP and forwards the message to the final destination node. If a device needs to send data to an application, PCP will execute a protocol conversion again. PCP runs as a CoAP server and responds for the CoAP client in the IP network.

Communication conversion protocols

We design two protocols to provide an adaption layer for Zigbee protocols. They work as bridge protocols and can be used to solve the control for smart devices, transformation of protocols, and inter-node communication problems of the PCF. Such devices can be sensors, actuators, coordinators, or gateways.

DNAP

DNAP is responsible for the access and exit of various types of equipment from the PCF. The operations of DNAP include device registration, address assignment, and device disconnection. The PCP automatically creates a device list to store the access information of devices at this point. The work-flow of DNAP is specified below:

New devices to join PCF

Whenever a new device boots up, first, it joins a Zigbee network and receives its 16-bit network address. This network address is also used as device ID. The device then sends an access request to CPS gateway to establish a connection with a PCP. The PCP then sends a CONACK message back to the device containing its ID. Furthermore, the device sends its detailed resource information to the PCP to do resource registration.

Device to exit the PCF

Initiative exit: If a device requests to quit the PCF, the PCP disconnects the device after receiving the request. Next, it releases the system resource and reports that the device exit is successful.

Passive exit: When the device is disconnected or failed, the PCP cannot receive response packets on time. Next, the PCP issues a disconnect request and waits for a reply message until a time-out happens. If a time-out occurs, the PCP releases the system resource and deletes the device information from device list. Message type of the protocol data unit (PDU) is specified in Table 1.

Table 1.

Message type of DNAP protocol data unit.

PDU type		Function
Request PDU	CONNECT	Initiates a connection request to the gateway
	DEVINFO	Send information to the gateway device.
	DISCONNECT	Disconnect the device.
Response PDU	CONACK	Response for CONNECT PDU, and send device ID back.
	ACCEPT	Notify device registration is complete.
	ACK	Device confirm registration have done.
	DROPACK	Confirm equipment revoked.

The PDU format of DNAP is shown in Table 2.

Table 2.

DNAP protocol data unit format.

Message type

PCP ID

Device ID

Seq. no.

Length

Data

When a device needs to join the PCF, it can use DNAP to initialize an access request. Once the device has a successful access to the PCF, a PCP will be assigned to it. The PCP becomes an agent for the device and provides multi-tasking support for the higher-level application layer.

DCTP

The IEEE 802.15.4 network consisting of tiny inexpensive autonomous devices equipped with sensors is a key technology for CPS to obtain physical data from real world. In a WSN, each sensor uses a 64-bit MAC address which is different from the IP address. In many Zigbee networks, there is no convergence mechanism to provide seamless communication between a WSN and an IP network. For this reason, we propose the DCTP to coordinate the control and execution.

While traditional Zigbee networks comprise anywhere between 5 and 20 nodes, we can form an LLN of this size and combine multiple LLNs into a large-scale WSN as needed. Every LLN is connected by a CPS control gateway. The gateway plays an important role of protocol conversion between a Zigbee LLN and an IP network. By using the DCTP message format, the control command can be sent to a destination device, and the sensing data or event notification message from the device can be sent back to the higher-level application layer. A CPS gateway connects with the coordinator in a Zigbee network. PCF uses DHCP server to dynamically assign IP address to a new CPS gateway. The application uses this IP address to communicate with devices in the LLN. PCP transforms all the control commands from DCTP format to CoAP format, and the corresponding response data from CoAP format to the DCTP format, respectively. CPS gateway transmits DCTP message to target device using its ID. The PDU of DCTP is designed as specified in Table 3

Table 3.

Protocol data unit of DCTP.

PDU type	Source ID	Destination ID
Port	Timestamp	Control/data type	Length of data
Data

There are two types of directions for the communication between the PCP and a WSN. The first direction is called control direction, and it consists of communication from PCP to WSN. The other direction is from WSN to the PCP, called data direction.

Control direction

In this case, the PDU is called a control PDU. The source ID is from the CPS control gateway, and the destination ID is from the destination Zigbee device. The value of port domain is used for correspondence with specific control applications. Timestamp value is dependent on the implementation of the sensor system. There are two time control models. First one is the control-response mode, and the second one is the timing mode. Once the application decides to execute control-response mode, the timestamp value is set to the time at which a command is sent. In timing mode, timestamp value is set to zero. The next domain contains two types:

Specified control: This is represented using binary format number ‘01’ or ‘10’. This control format is used to communicate with specific resources. The control command is organized into several resource-name/command pairs and stored in the data domain. Then the coordinator distributes it to the destination device. ‘01’ type is for normal communication and ‘10’ is for single point observe.

Broadcast control: This is represented using binary format number ‘11’ or ‘00’. This control message format is used to communicate with all devices in the WSN. The control command is available for all WSNs.

Data direction

In this case, the PDU is called a data PDU and it is used to transfer data related to the sensing data and device status to the PCP. The source ID is from Zigbee device, and the destination ID is for the CPS control gateway. The value of port domain is the port number which is obtained from the control PDU. Timestamp value is dependent on the timestamp of the received control PDU. If the device is in control-response mode, the timestamp value is set to the time at which the response data is sent to the CPS gateway. In the timing mode, the timestamp value is set to zero. Then, the next domain type chooses data, and it also has two types:

Response to the specified control PDU: This is represented using binary format number ‘01’ or ‘10’. The coordinator of a WSN collects the sensing data and device status from specific devices. The coordinator organizes this information into several resource-name/data pairs, stores in the data domain, and sends this information to the PCP. ‘01’ type is for single point response and ‘10’ is for single point observe response.

Bulk transfer: This is represented using binary format number ‘11’ or ‘00’, and is used to transfer original acknowledgement data collected from a large WSN or the result of data fusion with compressive sensing theory. ‘11’ type is for multi-point response and ‘00’ is for multi-point observe response.

The PDU type of DCTP is shown in Table 4. PCP receives a command from the application layer, and translates the command to a CTRDEV PDU, and sends it to the coordinator on the gateway. The coordinator periodically transmits the acknowledgement data back to the PCP using ACKDATA PDU under timing mode or the sensing data under control-response mode.

Table 4.

PDU type of DCTP.

PDU type		Function
Request PDU	CTRDEV	Send a group of control instructions to the coordinator.
Response PDU	ACKDATA	Transfer the sensation data back periodically or responsively.

Simulation and verification

We use SPIN to simulate and verify the DNAP and DCTP protocols described in the previous section, and to trace whether they have any logical design errors.

Analysis and modeling of DNAP

By setting a PCP process and a group of WSN coordinators, we model the DNAP in SPIN to simulate various conditions such as device registration, loss of messages, and retransmission. Simulation result is shown in the message sequence diagram of Figure 2.

Devices register sequence diagram

As shown in Figure 2, five devices try to join the PCF at random time through a coordinator labeled the TCPoint. Most of the devices can complete all the registration steps at the beginning. Also, we purposefully introduced features of loss of messages and retransmission of messages for some devices, and these devices still could fix such problems and finish all the registration steps without any difficulty.

Message loss and retransmission analysis

For the case of packet loss at the device side, the simulation result is shown in Table 5, whereas the result for the case of packet loss at the PCP side is shown in Table 6. From the results, it can be noted that the response for packet loss errors or retransmissions is handled correctly under the DNAP protocol.

Verification

DNAP verification is done using SPIN. The results of the verification process are shown in Figure 3. The three plus (+) symbols in the figure used to point out that we choose three verification methods to verify for any invalid end states, acceptance cycles, and assertion violations.

The tool has checked 138,845 states and found no errors. It means that there are no deadlocks, and the verification model for DNAP meets the safety requirements. By checking the acceptance cycles, this model did not violate the liveness property.

In an initial version of DNAP, we did not consider the packet losses. When verification was executed, we observed a deadlock. After tracing the error location using the XSPIN message flows, we found out the reason. Then, retransmission mechanism and timeout process were added to improve the initial version of DNAP. The improved version of DNAP got through the second time verification without any errors as shown in Figure 3.

Figure 2.

Simulation results of DNAP.

Table 5.

Simulation result of packet loss at the device side.

	The device side	The PCP side
CONNECT drop	Status: Cannot get CONACK packet from PCP in time.DNAP resolution: Re-send it several times if timeout.	Status: Haven’t received CONNECT packet.DNAP resolution: wait.
DEVINFO drop	Status: Cannot get ACCEPT packet from PCP in time.DNAP resolution: Re-send it several times if timeout.	Status: Haven’t received DEVINFO packet.DNAP resolution: Wait for some time, give up this register if timeout.

Table 6.

Simulation result of packet loss at the PCP side.

	The device side	The PCP side
CONNECT drop	Status: Cannot get CONACK packet from PCP in time.DNAP resolution: Re-send CONNECT packet several times.	Status: Haven’t received DEVINFO packet.DNAP resolution: Wait for some time, give up this register if timeout.
ACCEPT drop	Status: Cannot get ACCEPT packet from PCP in time.DNAP resolution: Wait.	Status: Cannot receive ACK packet in time.DNAP resolution: It has deal with it at the device side, so to avoid network congestion DNAP done nothing at the PCP side.

Figure 3.

Verification result of DNAP.

Analysis and modeling of DCTP

We model two work patterns of DCTP for different utilizations.

Control-response mode

This mode works in a request-response mode. A reply associated with the sent control data is received only if the timestamp is within the range of the control window. So, the application and the device process tasks asynchronously. The timestamp is also used for the heartbeat detection. So, the PCP can check whether the sensors are offline. During the data transfer, the two sides perform the following actions.

The PCP side maintains the latest timestamp value that has been sent to WSN, and this value is denoted by $St$ . Whenever the underlying WSN transmits data through the coordinator, the PCP needs to check the received timestamp ( $T$ ) to decide whether to receive or reject the data.

If $St - W < T \leq St$ , PCP receives the data.

If $T \leq St - W$ , the received data are obsolete, data are dropped.

If $T > St$ , it is an abnormal data packet and is dropped.

In the above logical operations, $W$ is the maximum receive window size.

The sensor side maintains the latest timestamp value it received from the PCP, and this value is denoted by $NT$ . Whenever the sensor receives a control data packet from the PCP, it updates the value of $NT$ , and sends out the appropriate control signals to sensors.

We use LTL to describe the properties and behavior of DCTP under control-response mode.

Definition 4. The execution of DCTP can be represented by a Kripke structure of $M = = (S, s_{0}, R, L$ ), where

$S$ is a finite set of protocol states of DCTP.

$s_{0} \in S$ is an initial state of DCTP.

$R \subseteq S \times S$ is the set of all state transition of DCTP, for which it holds that $\forall s \in S, \exists s' \in S$ , and $(s, s') \in R, (s, s')$ is one state transition.

$L : S \to 2^{AP}$ is a function which labels each state of the DCTP with the atomic propositions which hold true in that state.

$AP = {ϕ_{1}, ϕ_{2}, ϕ_{3}, ϕ_{4}, ψ_{1}, ψ_{2}}$ .

$ϕ_{1}$ : PCU receives a datagram from a device.

$ϕ_{2}$ : The timestamp of the received datagram is greater than the latest timestamp value that PCP has sent. $ϕ_{3}$ : The timestamp of the received datagram is within the receive window.

$ϕ_{4}$ : The timestamp of the received datagram is outside of the receive window.

$ψ_{1}$ : PCP drops the datagram.

$ψ_{2}$ : PCP receives the datagram.

Proposition 4.1. At any time, if the PCP receives a datagram whose timestamp is greater than the latest timestamp value that PCP has sent, then PCP drops the datagram. For this scenario, the LTL formula is given by

$P = [] (\neg (ϕ_{1} \land ϕ_{2}) U ψ_{1})$ (1)

Proposition 4.2. At any time, if the PCP receives a datagram whose timestamp is within the receive window, and then PCP can receive the datagram. For this scenario, the LTL formula is given by

$Q = [] (\neg (ϕ_{1} \land ϕ_{3}) U ψ_{2})$ (2)

Proposition 4.3. At any time, if the PCP receives a datagram whose timestamp is outside the receive window, and then PCP must drop the datagram. For this scenario, the LTL formula is given by

$H = [] (\neg (ϕ_{1} \land ϕ_{4}) U ψ_{1})$ (3)

An execution of the DCTP is an infinite sequence of its states $π = s_{0}, s_{1}, s_{2} . . .$ . We have to check $\forall π \in M$ , whether $π$ holds in $P$ , $Q$ and $H$ in SPIN

$\begin{matrix} π ⊧ [] (\neg (ϕ_{1} \land ϕ_{2}) U ψ_{1}) \\ \land [] (\neg (ϕ_{1} \land ϕ_{3}) U ψ_{2}) \\ \land [] (\neg (ϕ_{1} \land ϕ_{4}) U ψ_{1}) \end{matrix}$ (4)

SPIN converts the LTL formulas on the left-hand side of Figure 4 into three PROMELA never-claims: P, Q, and H. Then, the SPIN tool performs three model checks to verify whether properties of P, Q, and H hold true in the given protocol.

Figure 4.

Verification results under control-response mode.

The model-checking operation performs an exhaustive search over all the states reachable by the transit process. On our verification testing computer, the complete description of a global system state for checking every model required 524 bytes of memory (per state). The longest depth-first search paths contain 645, 537, and 645 transitions from the root of the tree for P, Q, and H, respectively. As shown in the right-hand side of the figure, no errors were found in these searches.

Figure 5 shows examples of three kinds of message flow in DCTP. It can be observed from Figure 5(a) that if the timestamp (line 93, T = 1000, W = 10, St = 1001) is within the receive window, the corresponding message will be received. As shown in Figure 5(b), if the timestamp is outside of the receive window (line 133, T = 982, W = 10, St = 1002), the corresponding message will be dropped. Furthermore, as shown in Figure 5(c), if the timestamp is abnormal (line 347, T = 1030, W = 10, St = 1010), the corresponding message will be dropped and error handling mechanism will be triggered.

2. Timing mode

Sometimes, applications need to collect data continuously from WSN on a long-term basis. For this purpose, we propose the timing mode to provide support for the Observe option of CoAP in the Zigbee LLN. The data type for the timing mode PDU can be “01” or “11” in the binary format. The binary format “01” is used to send data from the specific sensor that is specified in the control type PDU. The binary format “11” is used to periodically transfer the results of multi-sensor data in an LLN.We verify the timing mode of the protocol in SPIN using all possible states. The verification result is shown in Figure 6. The result of the figure indicates that the protocol did not encounter any deadlocks. In observe way, the first message sent by client is of control type must be set to ‘00’ or ‘10’. The notification response data type can be ‘00’ or ‘10’ in the subsequent cycles. The binary value ‘10’ implies single point observe, and the value ‘00’ means multi-point observe. The SPIN tool set up the model-checking for five sensors in an LLN and performed two types of verification, and the tool did not find errors. This implies that no deadlocks were encountered. By checking acceptance cycles, this model did not violate the liveness property. The Observe method can be correctly executed using the DCTP message format.

Figure 5.

Simulation result examples of three kinds of message flow in DCTP: (a) timestamp $T$ : $St - W < T \leq St$ , (b) timestamp $T$ : $T \leq St - W$ , and (c) timestamp $T$ : $T > St$ .

Figure 6.

Verification results under timing mode.

Security

In order to facilitate transmission of sensitive information, PCF permits communication via secure encryption. When a Zigbee device joins an LLN, PCF performs an encrypted node authentication. The coordinator is configured to deny network access to un-authenticated nodes. Devices and the coordinator use the pre-shared key (PSK) to establish authentication and encrypt the communication channel based on AES-128 in the LLN. DNAP and DCTP messages are encrypted and encapsulated within the payload of a Zigbee message. After PCP executing a protocol transform, the data coming from an LLN can be transmitted via secure CoAP. To protect CoAP transmissions, datagram TLS (DTLS) has been proposed as the primary security protocol. PCP and client perform a handshake to establish a DTLS session. DTLS message in the form of application data type can be used to transmit encrypted information between source and destination for a CoAP application.

Implementation

Our prototype system is built on top of a Zigbee networks. Each LLN is formed by five CC2530 nodes. The comparison results for Request/Response mode are shown in Figure 7. Four tests were conducted with the sleep time of Zigbee nodes varying from 1 to 4s. Each test is performed 50 times. The additional time overhead compared to normal Zigbee communication was calculated to be between 10 and 20 ms. So, the proposed framework did not result in a significant overhead to convert communication from one format to another.

Figure 7.

Request/response delay compared to normal Zigbee communication.

With PCF, the Firefox application with Copper plugin can access sensors using URI “coap://domain/resourceName.” Applications based on service-oriented architecture (SOA) can also easily access sensors using URI under CoAP. Figure 8 shows the CoAP Observe mode to subscribe data from a sensor. The test duration was 5 min, and the test statistics confirmed that no status-reporting messages were lost. From this observation, it can be concluded that the PCF can implement the Observe effect on top of Zigbee networks. So, PCF is a WoT solution for resource-constrained IoT devices.

Figure 8.

CoAP observe communication for Zigbee node.

Conclusion and future works

In this article, we proposed a solution for providing a universal communication platform for CPS. In order to integrate multiple protocol devices into framework, we provided the DNAP to implement a smart device register. We also designed the DCTP to facilitate communication between sensors and the application layer. This can be viewed as a CoAP solution for upgrading IoT to WoT network. We also used the SPIN model-checker tool to perform the simulation and verification for the proposed protocols DNAP and DCTP.

Possible future works include designing protocols to facilitate the 3G devices to join the PCP, extending the PCF to integrate scripting support for the application logic, and attempting to construct a self-organizing overlap network that is overlaid on a WoT network.

Footnotes

Academic Editor: George Nikolakopoulos

Declaration of conflicting interests

The author(s) declared no potential conflicts of interest with respect to the research,authorship,and/or publication of this article.

Funding

The author(s) received no financial support for the research,authorship,and/or publication of this article.

References

Lee

. Cyber physical systems: design challenges. In: Proceedings of the 11th IEEE international symposium on object and component-oriented real-time distributed computing (ISORC), Orlando, FL, 5–7 May 2008, pp.363–369. New York: IEEE.

Chaâri

Ellouze

Koubâa

. Cyber-physical systems clouds: a survey. Comput Netw 2016; 108: 260–278.

Bell-Labs. Verifying multi-threaded software with spin, http://spinroot.com/spin/whatispin.html (accessed 25 April 2016).

Cai

. Control protocols design for cyber-physical systems. In: Proceedings of the advanced information technology, electronic and automation control conference (IAEAC), Chongqing, China, 19–20 December 2015, pp.668–671. New York: IEEE.

Reza

Talevski

. Applications of wireless sensor networks in the oil, gas and resources industries. In: Proceedings of the 24th IEEE international conference on advanced information networking and applications, Perth, WA, Australia, 20–23 April 2010, pp.941–948. New York: IEEE.

Chao

Dargie

Lin

. Energy model for h2s monitoring wireless sensor network. In: Proceedings of the 11th IEEE international conference on computational science and engineering, São Paulo, Brazil, 16–18 July 2008, pp.402–409. New York: IEEE.

Aliyu

Al-Shaboti

Garba

. Hydrogen sulfide (h2s) gas safety system for oil drilling sites using wireless sensor network. Procedia Comput Sci 2015; 63: 499–504.

Mulligan

. The 6LoWPAN architecture. In: Proceedings of the 4th workshop on embedded networked sensors, Cork, 25–26 June 2007, pp.78–82. New York: ACM.

Rao

Amir

Dagale

. e-surakshak: a cyber-physical healthcare system with service oriented architecture. In: Proceedings of the 2012 international symposium on electronic system design (ISED), Kolkata, India, 19–22 December 2012, pp.177–182. New York: IEEE.

10.

Dillon

Zhuge

. Web-of-things framework for cyber–physical systems. Concurr Comp: Pract E 2011; 23(9): 905–923.

11.

Raggett

. The web of things: challenges and opportunities. Comput 2015; 48(5): 26–32.

12.

Shelby

Hartke

Bormann

. The constrained application protocol (CoAP). Proposed Standard, RFC 7252, June 2014, http://www.ietf.org/rfc/rfc7252.txt

13.

Villaverde

Pesch

Alberola

RDP

. Constrained application protocol for low power embedded networks: a survey. In: Proceedings of the sixth international conference on innovative mobile and internet services in ubiquitous computing, Palermo, 4–6 July 2012, pp.702–707. New York: IEEE.

14.

Thombre

Islam

Andersson

. Performance analysis of an IP based protocol stack for WSNs. In: Proceedings of the IEEE conference on computer communications workshops (INFOCOM WKSHPS), San Francisco, CA, 10–15 April 2016, pp.360–365. New York: IEEE.

15.

Cho

Chun

Jin

. Enhancing CoAP proxy for semantic composition and multicast communication. In: Adjunct proceedings of the 2015 ACM international joint conference on pervasive and ubiquitous computing and proceedings of the 2015 ACM international symposium on wearable computers, Osaka, Japan, 7–11 September 2015, pp.205–208. New York: ACM.

16.

Sheng

Wang

Yin

. Lightweight management of resource-constrained sensor devices in internet of things. IEEE Internet Things 2015; 2(5): 402–411.

17.

Mitsugi

Yonemura

Hada

. Bridging UPnP and Zigbee with CoAP: protocol and its performance evaluation. In: Proceedings of the workshop on Internet of Things and service platforms, Tokyo, Japan, 6–9 December 2011, pp.1–8. New York: ACM.

18.

Zigbee Alliance. Understanding Zigbee gateway: how Zigbee extends an IP network. Zigbee Alliance White Paper, September 2010.

19.

Hartke

. Observing resources in the constrained application protocol (CoAP). Proposed Standard, RFC 7641, September 2015, http://www.ietf.org/rfc/rfc7641.txt

20.

Aziz

. A formal model and analysis of an iot protocol. Ad Hoc Netw 2016; 36: 49–57.

21.

Capella

Campelo

Bonastre

. A reference model for monitoring IoT WSN-based applications. Sensors 2016; 16(11): 1816.

22.

Huth

Ryan

. Predicate logic. In: Huth