## 3 CPN Models
### Application Models  
To understand how the application model is obtained, it is important to observe that applications written in nesC are event-driven in such way that the order the application executes is only partially defined at compile time (see Section 2.2.1) due to the occurrence of tasks and events (e.g., the arrival of a message sent by another WSN node). Hence, a modelling element, named _scheduler_, has been introduced to explicitly treat with the occurrence of these tasks or events, and serves as the key element in the application models. These features make the application model generic, allowing represent any nesC application independent from the hardware platform. Each application model is organized into CPN modules (see Section 2.1.1) and each module models nesC tasks, commands and events (see Section 2.2.1). Events that depends on the occurrence of an external factor (e.g., another WSN node sends a message), has a probability associated by the application developer that indicates the probability and time of this particular event occurs. Figure 11 shows a schematic view of the Application model. The _scheduler_ has the following basic elements: a function queue, five transitions (_scheduler_, _start_, _end_, _sleep_, _boot_) and two places (_in_, _out_). The tasks and events are stored in a queue and each one has associated an identifier and the time indicating when the task or event must occur. In this way, tasks or  
Figure 11: Schematic representation of the Application model. Figure 10: CPN Model of the function. events are removed from the queue based on this time, e.g., the queued function with shortest time is the next to occur. In the case two different functions have the same time, one first queued is the next to be triggered. The transition _scheduler_ acts as an orchestrator that defines the next transition (or module) to be triggered according to the time associated to the task or event. Additionally, the task or event that is type AC will be selected by the transition _scheduler_ and it can not preempt the execution SC. In other words, AC is executed like a SC (see Section 2.2.1). At this point, it is worth observing that the event _receive_ (see Section 3.1.5) is never putted in queue, as it depends on an external event (when a third-party message arrives in the note). We solved this problem by allowing the _scheduler_ to alternatively select an event from the queue and the event _receive_. Additionally, the radio should be enabled to run the module _receive_. The places _in_ and _out_ are sockets and identify the beginning and the end of activities, respectively. The place _in_ is also the starting point of the model, indicating that the first transition to be performed (the other transitions will be chosen by the transition _scheduler_). It worth observing that the combination of transition _scheduler_, that decides which activity should be performed, with the place _in_, starting point of the application model and beginning of activities, leads to a reversible model. In other words, the model will always return to the starting point of the model through the transition _scheduler_. In the case the queue is empty (no function is ready to be triggered), the transition _sleep_ is triggered indicating that the application does not need to execute any task. The transition _start_ is executed only once, it initializes all variables and puts the first function in the function queue. The transition _end_ indicates the end of the application execution and may be executed several times. The transitions _boot_, _timer_, _t\({}_{\_}\)_, and _t\({}_{\_}\)_ depend on the application being modelled. These transitions correspond to task or event implemented by the application and each transition serves as a bridge between the module _scheduler_ and the respective function module. For example, the transitions _boot_ and _timer_ represents the respective _boot_ and _timer_ module. The transition _t\({}_{\_}\)_ and _t\({}_{\_}\)_ represents other function (task or event) implemented by the application.