1 User-specified properties wiring and writing

If a developer wishes to specify high-level properties, these take the form of nesC components providing the SimProperty interface, which has two commands: safetyPropertyCheck and livenessPropertyCheck, currently, T-Check can check multiple properties simultaneously. And the auxiliary "preprocessing" perl script can be applied to automatically wire property components into the application.

1.1 How to use preprocessing scrip?

Users may use the following instruction to automatically instrument some snippets of code.

./preprocessing [Application symbol] [A file containing the pairs of non-generic configuration and module]

[Application symbol] - Large-case symbol never used before in SimPropertyCheckC.nc component under the dir $TOSDIR/lib/tossim. If used, then the script will halt the running and warn the users that they should pick a new symbol name.

[A file containing pairs of configuration and module] - Each line in the file is composed of a pair of , Note that these two dirs must be expressed as a relative dir which uses $TOSROOT as reference.

Taking MultihopOscilloscope as example, users can use following command to automatically instrument code.

./preprocessing CTPPROPERTY propertyWiring.txt

It is better to express the symbol name in a large case way, and the number of configuration and module pairs in the propertyWiring.txt specifies the number of properties users want to provide

At the beginning, the script asks users to choose one from three options

Edit. If users never use the script to instrument the property-related code before, they should choose this option. Besides instrumenting necessary code into corresponding components, then script also implicitly backs up the modified components, i.e., suppose some code are automatically added into a component named "xxx.nc", then the original component file will be copied into a newly created file named "xxx.nc.bak".

Recover. As the name suggests, users can employ this option to recover the modified components to their original states.

Delete. If the users are satisfied with the instrumentation, then they can delete those backup files safely.

After running this command

(1) First, the following code will be instrumented into implementation part of SimPropertyCheckC.nc

    #ifdef CTPPROPERTY   
       components CtpP;
       SimPropertyCheckP.Property1 -> CtpP.Property1;
       SimPropertyCheckP.Property2 -> CtpP.Property2;
    #endif

(2) Then, the SimPropertyCheckP.nc will be established upon the SimPropertyCheckP-Master.nc file and number of properties users want to specify.

The following code will be added as uses parts, n denotes the number of property.

    uses interface SimProperty as Property1;
  	 ...
  	uses interface SimProperty as Propertyn;

The relatively complex code will be added into implementation part of SimPropertyCheckP.nc, and we will not show the concrete code here

(3) The following two snippets will be inserted into the provides part and implementation part of CtpP.nc respectively

 	
    #ifdef CTPPROPERTY
        interface SimProperty as Property1;
        interface SimProperty as Property2;
    #endif

 	
    #ifdef CTPPROPERTY
        Property1 = Router.Property1; //"Router" is the alias of generic module "CtpRoutingEngineP.nc"
        Property2 = Router.Property2;
    #endif

(4) At last, following two snippets will be inserted into the provides part and implementation part of CtpRoutingEngineP.nc

 	
    #ifdef CTPPROPERTY
        interface SimProperty as Property1;
        interface SimProperty as Property2;
    #endif

 	
    #ifdef CTPPROPERTY
      command bool Property1.safetyPropertyCheck() {
        return TRUE;
      }
      command bool Property1.livenessPropertyCheck() {
        return TRUE;
      }
      
      command bool Property2.safetyPropertyCheck() {
        return TRUE;
      }
      command bool Property2.livenessPropertyCheck() {
        return TRUE;
      }
    #endif

(5) At last, since T-Check concentrates on real-code checking, users should fill safetyPropertyCheck and livenessPropertyCheck with executable code, which is written upon variables defined in corresponding modules. Note that if the corresponding property is satisfied, then return TRUE; otherwise, return FALSE.

1.2 How to write the properties?

Users may refer to property examples which were all expressed in executable manner and checked by T-Check.

The property for single node application should be expressed like below:

      command bool SimProperty.livenessPropertyCheck() {
        return !receiveState.bufZeroLocked && !receiveState.bufOneLocked;
      }

The property for multiple nodes application can be written via following two modes:

(1). Sample liveness property for multi-nodes CTP with all motes' number starting from 0 and continuous

    	command bool SimProperty.livenessPropertyCheck() {
        int tmpMote = sim_node(), mote;
        for (mote = 0; mote < sim_simulated_mote_num(); mote++) {
           sim_set_node (mote);   //change to mote’s context
           if (sim_mote_forms_loop (mote)) {
             sim_set_node (tmpMote);
             return FALSE;
           }
        }
        sim_set_node (tmpMote);
        return TRUE;
      }

(2). Sample liveness property for multi-nodes CTP with all mote's number starting from 0 but non-continuous

    	command bool SimProperty.livenessPropertyCheck() {
        int tmpMote = sim_node(), mote;
        for (mote = 0; mote < sim_max_mote_num(); mote++) {
          if(sim_mote_status(mote) == ON) {
            sim_set_node (mote);  //change to mote’s context
            if(sim_mote_forms_loop (mote)) {
               sim_set_node (tmpMote);
               return FALSE;
            }
          }
        }
        sim_set_node (tmpMote);
        return TRUE;
      }

The main difference between above two modes concentrates on whether the mote's number is continuous or not. Note that sim_set_node(mote) function is critical for changing current context to specific mote's context.