Static analysis by abstract interpretation of the quasi-synchronous composition of synchronous programs

We present a framework to graphically describe and analyze embedded systems which are built on asynchronously wired synchronous subsystems. Our syntax is close to electronic diagrams. In particular, it uses logic and arithmetic gates, connected by wires, and models synchronous subsystems as boxes containing these gates. In our approach, we introduce a continuous-time semantics, connecting each point of the diagram to a value, at any moment. We then describe an analysis derived from the abstract interpretation framework enabling to statically and automatically prove temporal properties of the diagrams we defined. We can prove, for example, that the output of a diagram cannot be equal to a given value in a given interval of time.