3.7.1.5 Assertions

3.7.1.5 Assertions

Our assertion annotation language includes assertions for defining deadlock freeness, state reachability, and temporal properties. In PAT, System is a default keyword which represents the LTS of the input NesC application. The following describe the syntax and usage of each type of assertion, as well as the BNF of defining an assertion in PAT.

(A) Deadlock Freeness Checking (Nontermination Checking)
Deadlock freeness (also called nontermination) is an critical and desirable property of most sensor network applications, since scuh applications are always expected to run unattendedly for a long period like months or even years.

Syntax of Deadlock Freeness/Nontermination Checking

#assert System deadlockfree (#assert System nonterminate)

(B) State Reachability Checking
State reachability checking is to verify whether a certain state can be reached within finite steps of execution.

Syntax of State Reachability Checking

#assert System reaches State;

A state is defined in the following syntax, by a logical formula on variables of components.
The following defines a state with the name State.

Syntax for difining a state

#define State ; // ¦· is a logical formula

Notice that in the following BNF, v statnds for a component-level variable (e.g. LedsC.led0 in BlinkApp Example), and c is either a constant value or another variable.

BNF for logical formula

::= T                      true
                  | F                      false
                  | !                 negation
                  | &&    conjunction
                  | | |      disjunction
                  | v == c              relational equal
                  | v != c               relational inequal
                  | v < c                relational less than
                  | v <= c              relational less than or equal to
                  | v > c                relational greater than
                  | v >= c              relational greater than or equal to

An example of state reachability checking is as follows.

Defining a state led1ON

#define led1ON LedsC.led1 == 1;

Checking reachability

#assert System reaches led1ON;

(C) Temporal Property Checking
A temporal property is specified by a linear temporal logic (LTL) formula, the syntax of temporal property and LTL formula are described in the following tables, respectively.

Syntax of Temporal Property Checking

#assert System |= ;

Notice that (States U Actions) is the union of States, i.e. the set of states defined in by user using the format in (B), and Actions, i.e. the set of actions.

(D) Grammar Rules of Assertions
Defining an assertion in PAT follows the BNF shown below:

assertionExpr : '#' 'assert' VAR '|=' ltlExpr ';'
                         | '#' 'assert' VAR 'deadlockfree' ';'
                         | '#' 'assert' VAR 'reaches' VAR ';'
                         | '#' 'assert' VAR 'reaches' eventExpr ';' ;
eventExpr : eventEle ('.' eventEle)+ ;
eventEle : BOOL | ERRORT | VAR | ZERO | NATURAL | '[' | ']' ;
ltlExpr : (ltlTokenExpr)+ ;
ltlTokenExpr : eventExpr | ltlOprExpr;
ltlOprExpr : ltlOprEle | valueExpr ;
valueExpr : VAR | ZERO | NATURAL ;
ltlOprEle : '(' | ')' | '[]' | '<>' | '&&' | '||' | '->' | '!' | '<->' | '/\\' | '\\/' ;
BOOL : 'TRUE' | 'FALSE' ;
ERRORT : 'SUCCESS' | 'FAIL' | 'ESIZE' | 'ECANCEL' | 'EOFF' | 'EBUSY'
                  | 'EINVAL' | 'ERETRY'| 'ERESERVE' | 'EALREADY' | 'ENOMEM' | 'ENOACK' | 'ELAST' ;
VAR : ('a'..'z'|'A'..'Z'|'_') ('a'..'z'|'A'..'Z'|'0'..'9'|'_')* ;
ZERO : '0';
NATURAL : ('1'..'9')('0'..'9')* ;

Defining a state led1ON	#define led1ON LedsC.led1 == 1;
Checking reachability	#assert System reaches led1ON;