Abstract:

ET-LOTOS is an extension of LOTOS allowing the modelling of time-sensitive systems (i.e. systems whose behaviour is influenced by the passing of time). It is designed to be a "user friendly" formalism permitting the description of time dependent mechanisms in a clean and elegant manner, without having to resort to "tricks" and complex constructs. The counterpart of this rich expressive capability is that "undesirable" behaviours can be specified as well. For example, some processes cannot progress in time. Others enter in "zeno" divergences: they progress towards a certain time without ever reaching it. Other unrealistic behaviours are in fact desired features of the language: e.g. the possibility to perform consecutive actions at a same time instant is a useful abstraction. Test has already been studied for other timed formalisms. However it was always under restrictive hypothesis withdrawing precisely the "unrealistic" behaviours evoked above. Then, this is where our contribution takes place. We present fully abstract characterisations of may- and must-test in ET-LOTOS, taking into account all the possible behaviours, and we show how to derive them from the semantics of the processes, i.e. from their LTS.