Relaxing Synchronous Composition with Clock Abstraction

International audienceClocks defined as ultimately periodic infinite binary words were introduced to model features which are usually not considered in synchronous languages such as communication delay or the composition through bounded buffers. Clock abstraction are a simple mean allowing to reason in average on those clocks. These features are an important concern in hardware design. This work presents a new abstraction for clocks whose properties have been proven with the COQ proof assistant