Heterogeneous and asynchronous networks of timed systems

We present a component algebra and an associated logic for heterogeneous timed systems that can be interconnected at run time. The components of the algebra are asynchronous networks of processes, where processes are sets of traces that model the behaviour of the software applications or devices that are interconnected and execute according to the clock granularity of the network node in which they are placed. The advantage of a trace-based model is that it abstracts from the specificities of the different classes of automata that can be chosen as models of implementations and characterises at a higher level the topological properties of the languages generated by such automata that support several compositionality results; in the paper, such properties are supported by a new time refinement relation and its related closure operator. The main novelty and contribution of our theory lies in the fact that we do not assume that all network nodes have the same clock granularity and that interconnections can be established, at run time, among nodes with different clock granularities. We investigate conditions under which the interconnected processes can communicate and make progress, generating a collective non-empty behaviour, i.e., conditions that ensure that the interconnection is consistent. Those conditions can be verified at design time, thus allowing that systems can be interconnected at run time without further checking for compatibility; to the best of our knowledge, no other component algebra has been put forward for timed heterogeneous systems that does not require a-priory knowledge of their structure. Finally, we propose a logic that can support specifications for this component algebra and prove associated compositionality results.