Abstraction of polychronous dataflow specifications into mode-automata

For reactive embedded software - designed by composing existing reactive components - ensuring correctness is not straightforward. The possibility of deadlock across components, mismatch in temporal behaviors at the connected interface signals, etc., could lead to non-reactivity or subtle bugs. Behavioral interface theories have been proposed for checking compatibility of components when reactive modules are being composed. Depending on the models of computation, various intermediate notions of behavioral interfaces may be defined. In the case of polychronous components, the clock relations and the data dependencies at the interfaces are usually used for checking compatibility. However, if the behavior of a component is time variant, these abstractions are insufficient to establish correctness of composition. To capture time varying behavior, we propose to add an automaton based abstraction based on predicates abstraction. This paper describes the extraction of the abstraction, along with proofs of equivalence and the description of a practical implementation of the technique.