Main Article Content
The formal description of the observation-based computation model is stated using the formalism of transition systems, where real time is handled as a dedicated variable. As a first result, this approach allows to focus on specifying time constraints attached to data and to postpone task and communication scheduling matters. At this level of abstraction, the designer has to specify time properties about the timeline of data such as their freshness, stability, latency… As a second result, a verification of the global consistency of the specified system can be automatically performed. The verification process can start either from the timed properties (e.g. the period) of data inputs or from the timed requirements of data outputs (e.g. the latency). Lastly, communication protocols and task scheduling strategies can be derived as a refinement towards an actual implementation.