# 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

In general, axiomatic semantics is the nicest form of semantics, but is difficult to obtain for anything but the most simple languages, and subject of much current research. Denotational semantics is a vague term, if you mean domain theoretic semantics, then I advise against it. In general using operational semantics is easy and natural, especially if you use state-based SOS (structural operational semantics). The fact that you already have a translation into C is a strong indication that this would work in your case, because C can be seen as a state-based formalism.

Indeed your translation into C is a formal semantics of your sensor network language, albeit a painfully detailed one. So I guess you want a formal description that isto omit some level of detail (e.g. integers are 'real' mathematical integers and not some kind of finite modulo arithmetic). For this state-based SOS tends to be ideal.

-
You think I should work in the specified sensor network language? or feel that I have to work more at the generated code in C?. –  Claudio Biale Feb 21 '13 at 13:09
@ClaudioBiale it depends on you and what you are trying to achieve. If you want to communicate with other people, then using C might not be helpful since few people voluntarily read code. A more abstract, less detailed presentation could be easier to understand. If you are just trying to clarify matters for yourself, writing an additional semantic account to accompany C code could be overkill. So there's no one answer to your question. –  Martin Berger Feb 21 '13 at 13:27
Thanks for your reply. I want to formalize the semantics of the sensor network language. I'll look previous work using structured operational semantics and try to apply it in this language. –  Claudio Biale Feb 21 '13 at 13:48
@ClaudioBiale That sounds like a good approach. –  Martin Berger Feb 21 '13 at 14:50

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.

-
Using the Backus-Naur form I describe the sintax of the language, but what type of approaches it is convenient to use to providing a formal semantics of this type of programming language (denotational, axiomatic or operational). –  Claudio Biale Feb 18 '13 at 21:47