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?

• Are you after the formal semantics or a more formal way of describing the syntax? It sounds like the latter. – Dave Clarke Feb 18 '13 at 21:40
• See his comment to my answer, looks like he's interested in both. – Yuval Filmus Feb 18 '13 at 23:58
• Yuval Filmus, Dave Clarke I will describe the sintax using the Backus-Naur form and edit the question. – Claudio Biale Feb 19 '13 at 0:46
• Perhaps some sort of timed automaton model. – Dave Clarke Feb 19 '13 at 11:16
• Sounds suitable, from what information I have seen. – Dave Clarke Feb 21 '13 at 14:34