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.

StackExchange Computer Science Q#9902, answer score: 2