Formalizing timing diagrams as causal dependencies for verification purposes

Abstract

In this paper we investigate timing diagrams as a means to specify causal dependencies. We introduce a stylized graphical representation of timing diagrams for which we define a formal basis. Furthermore, we compare our approach with well-known approaches from the area of program verification and show the semantic relationships. The major aim we follow by this work is a seamless integration of hardware design and software development providing a common semantic basis e.g. for verification. Therefore, the semantic relationships to frameworks for program verification show that the combination of these approaches is a good starting point for further development. © Springer-Verlag Berlin Heidelberg 2000.