3.7.1 Language Reference

3.7.1 Language Reference

In this section, we illustrate the language features of NesC, including the concepts of interface, module, and configuration. In addition, the TinyOS library is discussed, which is provided in PAT as hardware abstractions and system services for NesC programs. Further, the assertion annotation language which is used to specify various properties as verification goal is presented.

3.7.1.1 Drawing a Sensor Network
A graphical editor is provided for

drawing a sensor network
editing each sensor to configure the NesC program running on it
editing verification goals (i.e., assertions)

3.7.1.2 The NesC Language
The extention of NesC programs ".nc" is supported here. In addition, users are allowed to provide ".h" files within their NesC source code files. We tried to provide the most convenience for users such that NesC programmers can easily put the same code that is to run on real hardware to be analyzed and verified by our tool.

3.7.1.3 TinyOS Library
A NesC program always invokes functions implemented by TinyOS, thus it is necessary to simulate the functions provided by TinyOS. We studied the source code of TinyOS as well as supporting documents, and have manually provided a subset of the components and interfaces pre-defined by TinyOS, which is to be used during the analysis and verification of NesC programs. We are now in the progress to automatically generate a complete library covering all components and interfaces of TinyOS.

3.7.1.4 Semantic Model
The semantic model (LTS) of a NesC application is generated in PAT, based on the language features of NesC and the execution model of TinyOS.

3.7.1.5 Assertions
The verification of NesC programs requires users to input properties in terms of assertions in our tool. Currently, we have supports for verifying three kinds of assertions: deadlock freeness, state reachability, and temporal properties.