A Data Oriented Approach for Real-Time Systems

Tanguy Le Berre (1, 2) , Philippe Mauran (2) , Gérard Padiou (2) , Philippe Quéinnec (2)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 ENSEEIHT - Ecole Nationale Supérieure d'Electrotechnique, d'Electronique, d'Informatique, d'Hydraulique et de Télécommunications

Distributed real-time systems often have to maintain the temporal validity of data. In this paper we present a modelling framework centered on data where a so-called observation relation represents and abstracts the interactions between variables. An observation is a relation between variables, an image and its sources, where the image values depend on past values of the sources. The system architecture is seen as a set of observation relations describing the flow of values between variables. The observation relations are parametrized with timed constraints that limit the time shift between the variables and specify the availability of timely sound values. At this level of abstraction, the designer gives a specification of the system based on timed properties about the timeline of data such as their freshness, latency etc. We proceed to an analysis of the feasibility of such a specification and we formally analyze the correctness of an implementation with respect to a specification. In order to prove the feasibility of an observationbased model, we build a finite state transition system which is bi-similar to the specification. The existence of an infinite execution in this system proves the feasibility of the specification. Possible implementations are described as a set of interacting components which control the flow of values in the system. A finite system is built to prove the correctness of the implementation by model checking

Domaines: Réseaux et télécommunications [cs.NI]

Tanguy Le Berre, Philippe Mauran, Gérard Padiou, Philippe Quéinnec. A Data Oriented Approach for Real-Time Systems. 17th International Conference on Real-Time and Network Systems, Oct 2009, Paris, France. pp.147-158. ⟨inria-00442001⟩