Schedulability Analysis of Distributed Real-Time Sensor Network Applications Using Actor-Based Model Checking
- 531 Downloads
Programmers often use informal worst-case analysis and debugging to ensure schedules that satisfy real-time requirements. Not only can this process be tedious and error-prone, it is inherently conservative and thus likely to lead to an inefficient use of resources. We propose to use model checking to find a schedule which optimizes the use of resources while satisfying real-time requirements. Specifically, we represent a Wireless sensor and actuator network (WSAN) as a collection of actors whose behavior is specified using a C-based actor language extended with operators for real-time scheduling and delay representation. We show how the abstraction and compositionality properties of the actor model may be used to incrementally build a model of a WSAN’s behavior from node-level and network models. We demonstrate the approach with a case study of a distributed real-time data acquisition system for high frequency sensing using Timed Rebeca modeling language and the Afra model checking tool.
KeywordsSensor network Schedulability analysis Actor Timed Rebeca Model checking
Wireless sensor and actuator networks (WSANs) can provide low-cost continuous monitoring. However, building WSAN applications is particularly challenging. Because of the complexity of concurrent and distributed programming, networking, real-time requirements, and power constraints, it can be hard to find a configuration that satisfies these constraints while optimizing resource use. A common approach to address this problem is to perform an informal analysis based on conservative worst-case assumptions and empirical measurements. This can lead to schedules that do not utilize resources efficiently. For example, a workload consisting of two periodic tasks would be guaranteed to be safe only if the sum of the two worst-case execution times (WCET) were less than the shorter period, whereas it is possible in practice to have many safe schedules violating this restriction.
A second approach is trial and error. For example, in , an empirical test-and-measure approach based on binary search is used to find configuration parameters: worst-case task runtimes, timeslot length of the communication protocols, etc. Trial and error is a laborious process, which nevertheless fails to provide any safety guarantees for the resulting configuration.
A third possibility is to extend scheduling techniques that have been developed for real-time systems  so that they can be used in WSAN environments. Unfortunately, this turns out to be difficult in practice. Many WSAN platforms rely on highly efficient event-driven operating systems such as TinyOS . Unlike a real-time operating system (RTOS), event-driven operating systems generally do not provide real-time scheduling guarantees, priority-based scheduling, or resource reservation functionality. Without such support, many schedulability analysis techniques cannot be effectively employed. For example, in the absence of task preemption and priority-based scheduling, unnecessarily conservative assumptions must be used to guarantee correctness in the general case.
We propose an actor-based modeling approach that allows WSAN application programmers to assess the performance and functional behavior of their code throughout the design and implementation phases. The developed models are analyzed using model checking to determine the parameter values resulting in the highest system efficiency. Note that our use of model checking is similar to the work of Jorgerden et al. who use it to maximize the life-time of batteries in embedded systems .
We represent a WSAN application as a collection of actors . The model can be incrementally extended and refined during the application design process, adding new interactions and scheduling constraints. We use Timed Rebeca  as the modeling language and its model checking tool Afra [1, 15] for analysis of WSAN applications. Timed Rebeca is a high-level actor-based language capable of representing functionality and timing behavior at an abstract level. Afra supports modeling and analysis of both of Rebeca and Timed Rebeca models; we use the timed model checking engine. Afra uses the concept of Floating Time Transition System (FTTS)  for the analysis of Timed Rebeca models. FTTS significantly reduces the state space that needs to be searched. The idea is to focus on event-based properties while relaxing the constraint requiring the generation of states where all the actors are synchronized. As the examples in  suggest, this approach can reduce the size of the state space by 50 to 90 %. Using FTTS fits with the computation model of WSAN applications and the properties that we are interested in.
We present a case study involving real-time continuous data acquisition for structural health monitoring and control (SHMC) of civil infrastructure . This system has been implemented on the Imote2 wireless sensor platform, and used in several long-term development of several highway and railroad bridges . SHMC application development has proven to be particularly challenging: it has the complexity of a large-scale distributed system with real-time requirements, while having the resource limitations of low-power embedded WSAN platforms. Ensuring safe execution requires modeling the interactions between the CPU, sensor and radio within each node, as well as interactions among the nodes. Moreover, the application tasks are not isolated from other aspects of the system: they execute alongside tasks belonging to other applications, middleware services, and operating system components. In the application we consider, all periodic tasks (sample acquisition, data processing, and radio packet transmission) are required to complete before the next iteration starts. Our results show that a guaranteed-safe application configuration can be found using the Afra model checking tool. Moreover, this configuration improves resource utilization compared to the previous informal schedulability analysis used in , supporting a higher sampling rate or a larger number of nodes without violating schedulability constraints.
We show how a WSAN application may be modeled naturally as a system of actors. The abstraction and modularity of the actor model makes the approach scalable.
We present a real-world case study that illustrates the effectiveness of our approach for a real WSAN application.
We show how model checking toolsets can be used for an efficient schedulability analysis of WSAN application. Our case study shows we can compare the effects of different communication protocols on system performance.
A WSAN application is a distributed system with multiple sensor nodes, each comprised of the independent concurrent entities: CPU, sensor, radio system, and bridged together via a wireless communication device which uses a transmission control protocol. Interactions between these components, both within a node and across nodes, are concurrent and asynchronous. Moreover, WSAN applications are sensitive to timing, with soft deadlines at each step of the process needed to ensure correct and efficient operation.
Due to performance requirements, and latencies of operations on sensor nodes, sensing, data processing, and communication processes must be coordinated. In particular, once a sample is acquired from a sensor, its corresponding radio transmission activities must be performed. Concurrently, data processing tasks–such as compensating sensor data for the effects of temperature changes–must be executed. Moreover, the timing of radio transmissions from different nodes must be coordinated using a communication protocol.
2.1 The Actor Model of WSAN Applications
The Actor model is a well-established paradigm for modeling distributed and asynchronous component-based systems. This model was originally introduced by Hewitt as an agent-based language where goal directed agents did logical reasoning . Subsequently, the actor model developed as a model of concurrent computation for open distributed systems where actors are the concurrently executing entities . One way to think of actors is as a service oriented framework: each actor provides services that may be requested via messages from other actors. A message is buffered until the provider is ready to execute the message. As a result of processing a message, an actor may send messages to other actors, and to itself. Extensions of the actor model have been used for real-time systems, in particular: RT-synchronizer , real-time Creol , and Timed Rebeca .
We represent components of each WSAN node capable of independent action as an actor. Specifically, as shown in Fig. 1, a sensor node is modeled using four actors: Sensor (for the data acquisition) CPU (processor), RCD (a radio communication device) and Misc (carrying out miscellaneous tasks unrelated to sensing or communication). Sensor collects data and send it to CPU for further data processing. Meanwhile, CPU may respond to messages from Misc by carrying out other computations. The processed data is sent to RCD to forward it to a data collector node actor. We model the communication medium as an actor (Ether) and the receiver node also by the actor RCD. Using the actor Ether facilitates modularity: specifically, implementation of the Media Access Control (MAC) level details of communication protocols is localized, making it is easy to replace component sub-models for modeling different communication protocols without significantly impacting the remainder of the model. During the application design phase, different components, services, and protocols may be considered. For example, TDMA  as a MAC-level communication protocol may be replaced by B-MAC  with minimal changes.
Although schedulability analysis of WSAN applications can be challenging in the absence of a real-time scheduler, we reduce the problem of checking for deadline violations to the problem of reachability from a relatively small set of possible initial configurations. Model checking is the natural approach to this class of problems, and it is the approach we explore in this paper.
2.2 Timed Rebeca and the Model Checking Toolset
A Timed Rebecca (TR) model consists of reactive classes and a main program which instantiates actors (called rebecs in TR). As usual, actors have an encapsulated state, a local time, and their own thread of control. Each actor contains a set of state variables, methods and a set of actors it knows. An actor may only send messages to actor that it knows. Message passing is implemented by method calls: calling a method of an actor (target) results in sending a message to the target. Each actor has a message bag in which arriving messages may be buffered; the maximum capacity of the bag is defined by the modeler.
Timing behavior in TR is represented using three timing primitives: delay, after, and deadline. A delay term models the passing of time for an actor. The primitives after and deadline can be used in conjunction with a message send: after n indicates it takes n time units for the message to be delivered to its receiver; deadline n indicates that if the message is not taken in n time units, it should be purged from the receiver’s bag.
Afra 1.0 supports model checking of Rebeca models against LTL and CTL properties. Afra 2.0 supports deadlock detection and schedulability analysis of TR models; we use Afra 2.0 in this work. TR and Afra toolset have previously been used to model and analyze realtime actor based models such as routing algorithms and scheduling policies in NoC (Network on Chip) designs [26, 27].
3 Schedulability Analysis of a Stand-Alone Node
We now illustrate our approach using a node-level TR model of a WSAN application to check for possible deadline violations. Specifically, by changing the timing parameters of our model, we find the maximum safe sampling rate in the presence of other (miscellaneous) tasks in the node. Then, we show how the specification of a node-level model can be naturally extended to network-wide specifications.
As shown in Fig. 2, the maximum capacity of the message bag of Sensor is set to 10, the only actor Sensor knows about is of type CPU (line 4), and Sensor does not have any state variables (line 5). The behavior of Sensor is to periodically acquire data and send it to CPU. Sensor is implemented using a message server sensorLoop (lines 13–17) which sends the acquired data to CPU (line 15). The sent data must be serviced before the start time of the next period, specified by the value of period as the parameter of deadline. Recall that there is a nondeterministic initial offset after which the data acquisition becomes a periodic task. To represent this property, Sensor which sends a sendLoop message to itself; the message is nondeterministically delivered after one of 10, 20, and 30 (line 11). After this random offset, a sensor’s periodic behavior is initiated (line 13). Note that in line 1, the sampling rate is defined as a constant. A similar approach is used in the implementation of the Misc reactive class.
Note that computation times (delay’s) depend on the low-level aspects of the system and are application-independent; they can be measured before the application design. For schedulability analysis, we set the deadline for messages in a way that any scheduling violations are caught by the model checker.
4 Schedulability Analysis of Multi-node Model with a Distributed Communication Protocol
Transitioning from a stand-alone node model a network model requires that the wireless communication medium Ether to be specified in order to model the communication protocol it supports. Then both the node-level and multi-node models must be considered. Recall that nodes in the multi-node model periodically send their data to an aggregator node (Fig. 1). The sending process is controlled by a wireless network communication protocol. The reactive class of Ether (Fig. 5) has three message servers: these are responsible for sending the status of the medium, broadcasting data, and resetting the condition of the medium after a successful transmission. Broadcasting data takes place by sending data to a RCD which is addressed by the receiverDevice variable. So, we can easily examine the status of the Ether using the value of receiverDevice (i.e., medium is free if receiverDevice is not null, line 13). This way, after sending data, the value of receiverDevice and senderDevice must be set to null to show that the transmission is completed (lines 28 and 29). Data broadcasting is the main behavior of Ether (lines 15 to 26). Before the start of broadcasting, the Ether status is checked (line 16) and data-collision error is raised in case of two simultaneous broadcasts (line 24). With a successful data broadcast, Ether sends an acknowledgment to itself (line 19) and the sender (line 20), and informs the receiver of the number of packets sent to it (line 21). In addition to the functional requirements of Ether, there may be non-functional requirements. For example, the Imote2 radio offers a theoretical maximum transfer speed of 250 kbps. When considering only the useful data payload (goodput), this is reduced to about 125 kbps.
We now extend RCD to support communication protocols. Figure 6 shows the model of TDMA protocol implementation. TDMA protocol defines a cycle, over which each node in the network has one or more chances to transmit a packet or a series of packets. If a node has data available to transmit during its alloted time slot, it may be sent immediately. Otherwise, packet sending is delayed until its next transmission slot. The periodic behavior of TDMA slot is handled by handleTDMASlot message server which sets and unsets inActivePeriod to show that whether the node is in its alloted time slot. Upon entering into it’s slot, a device checks for pending data to send (line 31) and schedules handleTDMASlot message to leave the slot (line 30). On the other hand, when CPU sends a packet (message) to a RCD, the message is added to the other pending packets which are waiting for the next alloted time slot. tdmaSlotSize is the predefined size of the tdma slots, and currentMessageWaitingTime is the waiting time of this message in the bag of its receiver.
Once a complete model of the distributed application has been created, the Afra model checking tool can verify whether the schedulability properties hold in all reachable states of the system. If there are any deadline violations, a counterexample will be produced, indicating the path—sequence of states from an initial configuration—that results in the violation. This information can be helpful with changing the system parameters, such as increasing the TDMA time slot length, to prevent such situations.
5 Experimental Results and a Real-World Case Study
This flexible data acquisition system can be configured to support real-time collection of high-frequency, multi-channel sensor data from up to 30 wireless smart sensors at frequencies up to 250 Hz. As it is designed for high-throughput sensing tasks that necessitate larger networks sizes with relatively high sampling rates, it falls into the class of data-intensive sensor network applications, where efficient resource utilization is critical, since it directly determines the achievable scalability (number of nodes) and fidelity (sampling frequency) of the data acquisition process. Configured on the basis of network size, associated sampling rate, and desired data delivery reliability, it allows for near-real-time acquisition of 108 data channels on up to 30 nodes—where each node may provide multiple sensor channels, such as 3-axis acceleration, temperature, or strain—with minimal data loss. In practice, these limits are determined primarily by the available bandwidth of the IEEE 802.15.4 wireless network and sample acquisition latency of the sensors. The accuracy of estimating safe limits for sampling and data transmission delays directly impacts the system’s efficiency.
To illustrate the applicability of this work, we considered applications where achieving the highest possible sampling rate that does not result in any missed deadline is desired. This is a very common requirement in WSAN applications in the SHMC domain in particular. We begin by setting the value of OnePacketTT to 7 ms (i.e., the maximum transmission time of this type of applications) and fixed the value of sensorTaskDelay, miscPeriod, and miscTaskDelay to some predefined values. In addition to the sampling rate, the number of nodes in the network and the packet size remain variable. By assuming different values for the number of nodes and the packet size, different maximum sampling rates are achieved, shown as a 3D surface in Fig. 7. As shown in the figure, higher sampling rates are possible when the buffer size is set to a larger number (there is more space for data in each packet). Similarly, increasing the number of nodes decreases the sampling rate: in competition among three different parameters of Fig. 7, the cases with the maximum buffer size (i.e., 9 data points) and minimum number of nodes (i.e., 1 node) results in the highest possible maximum sampling rates. Decreasing the buffer size or increasing the number of nodes, non-linearly reduces the maximum possible sampling rate.
The parameters used in our analysis of configurations were determined through a real-world installation of an SHMC application. Our results show that the current manually-optimized installation can be tuned to an even more optimized one: by changing the configuration, the performance of the system can be safely improved by another 7 %.
6 Related Work
Three different approaches have been used for analysis of WSANs: system simulation, analytical approach, and formal verification.
System Simulation. Simulation of WSAN applications is useful for their early design exploration. Simulation toolsets for WSANs have enabled modeling of networks , power consumption , and deployment environment . Simulators can adequately estimate performance of systems and sometimes detect conditions which lead to deadline violations. But even extensive simulation does not guarantee that deadline misses will never occur in the future . For WSAN applications with hard real-time requirements this is not satisfactory. Moreover, none of available simulators is suitable for the analysis WSAN application software.
Analytical Approach. A number of algorithms and heuristics have been suggested for schedulability analysis of real-time systems with periodic tasks and sporadic tasks with constraints, e.g. . Although these classic techniques are efficient in analyzing schedulability of real-time systems with periodic tasks and sporadic tasks, their lack of ability to model random tasks make them inappropriate for WSAN applications.
Formal Verification. Real-time model checking is an attractive approach for schedulability analysis with guarantees . Model checking tools systematically check whether a model satisfies a given property . The strength of model checking is not only in providing a rigorous correctness proof, but also in the ability to generate counter-examples, as diagnostic feedback in case a property is not satisfied. This information can be helpful to find flaws in the system. Norström et al. suggest an extension of timed automata to support schedulability analysis of real-time systems with random tasks . Feresman et al. studied an extension of timed automata which its main idea is to associate each location of timed automata with tasks, called task automata .
TIMES  is a toolset which is implemented based on the approach of Feresman et al.  for analysis of task automata using UPPAAL as back-end model checker. TIMES assumes that tasks are executed on a single processor. This assumption is the main obstacle against using TIMES for schedulability analysis of WSAN applications, which are real-time distributed applications. De Boer et al. in  presented a framework for schedulability analysis of real-time concurrent objects. This approach supports both multi-processor systems and random task definition, which are required for schedulability analysis of WSAN applications. But asynchronous communication among concurrent elements of WSAN application results in generation of complex behavioral interfaces which lead to a state space explosion even for small size examples.
Real-Time Maude is used in  for performance estimation and model checking of WSAN algorithms. The approach supports modeling of many details such as communication range and energy use. The approach requires some knowledge of rewrite logic. Our tool may be easier to use by engineers unfamiliar with rewriting logic: our language extends straight-forward C-like syntax with actor concurrency constructs and primitives for sensing and radio communication. This requires no formal methods experience from the WSAN application programmer, as the language and structure of the model closely mirror those of the real application.
We have shown one of the applications of real-time model checking method in analyzing schedulability and resource utilization of WSAN applications. WSAN applications are very sensitive to their configurations: the effects of even minor modifications to configurations must be analyzed. With little additional effort required on behalf of the application developer, our approach provides a much more accurate view of an WSAN application’s behavior and its interaction with the operating system and distributed middle-ware services than can be obtained by the sort of informal analysis or trial-and-error methods commonly in use today.
Our realistic—but admittedly limited—experimental results support the idea that the use of formal tools may result in more robust WSAN applications. This would greatly reduce development time as many potential problems with scheduling and resource utilization may be identified early.
An important direction for future research is the addition of probabilistic behavior analysis support to the tool. In many non-critical applications, infrequent scheduling violations may be considered a reasonable trade-off for increased efficiency in the more common cases. Development of a probabilistic extension is currently underway.
The work on this paper has been supported in part by the project “Timed Asynchronous Reactive Objects in Distributed Systems: TARO” (nr. 110020021) of the Icelandic Research Fund, by Air Force ResearchLaboratory and the Air Force Office of Scientific Research under agreement number FA8750-11-2-0084, and by National Science Foundation under grant number CCF-1438982. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The authors acknowledge the helpful comments by the anonymous referees and by Karl Palmskog.
- 1.Rebeca Formal Modeling Language. http://www.rebeca-lang.org/
- 2.Agha, G.A.: ACTORS - A Model of Concurrent Computation in Distributed Systems. MIT Press Series in Artificial Intelligence. MIT Press, Cambridge (1990)Google Scholar
- 4.Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
- 5.David, A., Illum, J., Larsen, K.G., Skou, A.: Model-based framework for schedulability analysis using UPPAAL 4.1. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems, pp. 93–119. CRC Press, Boca Raton (2010)Google Scholar
- 8.El-Hoiydi, A.: Spatial TDMA and CSMA with preamble sampling for low power ad hoc wireless sensor networks. In: Proceedings of the Seventh IEEE Symposium on Computers and Communications (ISCC 2002), 1–4 July 2002, Taormina, Italy, pp. 685–692. IEEE Computer Society (2002)Google Scholar
- 11.Hewitt, C., Bishop, P., Steiger, R.: A universal modular ACTOR formalism for artificial intelligence. In: Nilsson, N.J. (ed.) IJCAI, pp. 235–245. William Kaufmann (1973)Google Scholar
- 12.Hill, J., Szewczyk, R., Woo, A., Hollar, S., Culler, D., Pister, K.: System architecture directions for networked sensors. In: SIGPLAN Notices, vol. 35, pp. 93–104, November 2000Google Scholar
- 13.Illinois SHM Services Toolsuite. http://shm.cs.illinois.edu/software.html
- 17.Levis, P., Lee, N., Welsh, M., Culler, D.E.: TOSSIM: accurate and scalable simulation of entire tinyos applications. In Akyildiz, I.F., Estrin, D., Culler, D.E., Srivastava, M.B. (eds.), Proceedings of the 1st International Conference on Embedded Networked Sensor Systems, SenSys 2003, Los Angeles, California, USA, 5–7 November 2003, pp. 126–137. ACM (2003)Google Scholar
- 18.Linderman, L., Mechitov, K., Spencer, B.F.: TinyOS-based real-time wireless data acquisition framework for structural health monitoring and control. Struct. Control Health Monit. (2012)Google Scholar
- 20.Liu, J.W.S.: Real-Time Systems, 1st edn. Prentice Hall PTR, Upper Saddle River (2000)Google Scholar
- 21.Norström, C., Wall, A., Yi, W.: Timed automata as task models for event-driven systems. In: RTCSA, pp. 182–189. IEEE Computer Society (1999)Google Scholar
- 23.Polastre, J., Hill, J.L., Culler, D.E.: Versatile low power media access for wireless sensor networks. In: Stankovic et al. , pp. 95–107Google Scholar
- 24.Ren, S., Agha, G.: RTsynchronizer: language support for real-time specifications in distributed systems. In: Gerber, R., Marlowe, T.J. (eds.) Workshop on Languages, Compilers and Tools for Real-Time Systems, pp. 50–59. ACM (1995)Google Scholar
- 26.Sharifi, Z., Mohammadi, S., Sirjani, M.: Comparison of NoC routing algorithms using formal methods. In: Proceedings of PDPTA 2013 (2013, to be published)Google Scholar
- 27.Sharifi, Z., Mosaffa, M., Mohammadi, S., Sirjani, M.: Functional and performance analysis of network-on-chips using actor-based modeling and formal verification. In: ECEASST, vol. 66 (2013)Google Scholar
- 28.Shnayder, V., Hempstead, M., Chen, B.-R., Werner-Allen, G., Welsh, M.: Simulating the power consumption of large-scale sensor network applications. In: Stankovic et al. , pp. 188–200Google Scholar
- 29.Spencer Jr., B.F., Jo, H., Mechitov, K., Li, J., Sim, S.-H., Kim, R., Cho, S., Linderman, L., Moinzadeh, P., Giles, R., Agha, G.: Recent advances in wireless smart sensors for multi-scale monitoring and control of civil infrastructure. J. Civil Struct. Health Monit. 1–25 (2015)Google Scholar
- 30.Stankovic, J.A., Arora, A., Govindan, R. (eds.): Proceedings of the 2nd International Conference on Embedded Networked Sensor Systems, SenSys 2004, Baltimore, MD, USA, 3–5 November 2004. ACM (2004)Google Scholar
- 31.Sundresh, S., Kim, W.Y., Agha, G.: Sens: a sensor, environment and network simulator. In: Proceedings 37th Annual Simulation Symposium (ANSS-37 2004), 18–22 April 2004, Arlington, VA, USA, pp. 221–228. IEEE Computer Society (2004)Google Scholar