Formally describing a sensor network language I have a language for sensor networks (generates C code) and I want to define the formal semantics of it.

The language has this form:

{STATE name_state:
EVERY time
SELECT {variable [, variable] ...}
[SENDIF send_condition]
[CHANGEIF change_condition GOTO new_state];
} ...

START IN initial_state;



The initial state of the program is specified by the START IN instruction.
Each state is defined by the STATE instruction.
In the specification of each state the clauses EVERY and SELECT are compulsory and the clauses SENDIF and CHANGEIF are optional.
The CHANGEIF clause is only not specified when there is a single state.


What type of formal semantics is more convenient to use?
Backus-Naur form used to be popular for these purposes. Another possibility is Wirth syntax notation. You can find other possibilities in the "see also" section of the article on Backus-Naur form.