3.7.1.3 TinyOS Library

3.7.1.3 TinyOS Library

TinyOS is implemented in NesC, as a set of interfaces and components, which abstract hardware services and are necessary for NesC programs to execute correctly. TinyOS is the platform which NesC programs are running upon. It provides hardware interfaces and services including display(LED), timing(Clock & Alarm), data transfer(UART), sensing(Photo, Temperature, ADC) and communications(Message, Packet, Byte, RFM), as NesC interfaces and components.

TinyOS handles hardware services and its source code traverses a multiple-level hierarchy with a number of components. And the bottom components/interfaces program on chips directly, the semantics of which is quite different from high-level ones. Currently, PAT focuses on the high-level behaviors of NesC applications and we have high confidence on the reliability and correctness of TinyOS, assuming it is always correct. Therefore, PAT comes out with a static library of NesC processes abstracting and modeling the behaviors of components implemented by TinyOS. In summary, several strategies and assumptions are taken into account during modeling hardware services provided by TinyOS.

Firstly, component variables are introduced to model states of certain hardware, although in real TinyOS those variables do not exist. This is justified in that component variables are private and local, and introducing extra component variables will not bring forth variable conflicts in the whole NesC program. For example, component LedsC is an interface to turn on or off leds of a sensor node, and three component variables are introduced to model the state (ON or OFF) of three leds respectively. As for commands such as leds.led0On(), leds.led0Off() and others, which are turning on or off certain leds, they are modeled as NesC processes composed of an assignment updating the value of corresponding component variables.

Secondly, system logics of hardware services are highly abstracted, because of the assumption that hardware has few errors. Moreover, our approach aims at helping NesC programmers to understand their code more easily, to whom TinyOS serves like a black-box. Therefore, for commands that implement straightforward hardware behaviors but are presented in complicated NesC code, we make them compact and abstract with processes updating related states and signaling corresponding events, denoting the completion of hardware request. For example, command AMSend.send() is modeled as process P = (post sendDone; return SUCCESS), where post sendDone posts a task (sendDone()) which simply signals the event AMSend.sendDone().

Thirdly, process Wait models the behaviors of Timers.
For example, command Timer.startPeriodic(50) is modeled as:

while(timer == start){Wait[50]; (signal~Timer.fired())}

which signals the event Timer.fired() every 50 time units. is used here to model the fact that exactly at the end of 50 time units, the fired event is signaled.

Currently, PAT has only provided a subset of interfaces and components of TinyOS, as shown in the bellow table.

    Service     Interfaces     Components

Initialization

Boot, Init

MainC

Timing

Timer, Alarm

TimerMilliC

Packet

PacketAcknowledgements,
      AMPacket, Packet, CollectionPacket

ActiveMessageC,
      SerialActiveMessageC,

Communication

Send, Receive

AMSenderC, AMReceiverC

Leds

Display

LedsC

Sensing

Read,

DemoSensorC,

Control

SplitControl, StdControl, RootControl

MainC

Data Structure

Queue, Pool

--

Service	Interfaces	Components
Initialization	Boot, Init	MainC
Timing	Timer, Alarm	TimerMilliC
Packet	PacketAcknowledgements, AMPacket, Packet, CollectionPacket	ActiveMessageC, SerialActiveMessageC,
Communication	Send, Receive	AMSenderC, AMReceiverC
Leds	Display	LedsC
Sensing	Read,	DemoSensorC,
Control	SplitControl, StdControl, RootControl	MainC
Data Structure	Queue, Pool	--