Formal Model for Program Analysis



This chapter presents the main intermediate representations that serve for the analysis of clocks and data dependencies in programs. A Signal program is a formal specification that is basically composed of equations describing relations for both values and clocks of the signals involved. This essence of the language allows one to mathematically reason on the properties of such a specification. The reasoning framework allowed by Signal is the algebraic domain  ∕ 3, the set of integers modulo 3. The intrinsic properties of this domain typically enable one to deal efficiently with clock properties in Signal programs. Section 8.1 presents the encoding of Signal constructs in  ∕ 3 (Le Guernic and Gautier in Advanced Topics in Data-Flow Computing, Prentice Hall, pp. 413–438, 1991). Then, Sect. 8.2 deals with the representation of the data dependencies expressed by Signal programs using a specific directed dependency graph.


Veri Undersampling 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Le Borgne M, Marchand H, Rutten É, Samaan M (2001) Formal verification of Signal programs: Application to a Power Transformer Station Controller. Science of Computer Programming 41(1):85–104MATHCrossRefGoogle Scholar
  2. 2.
    Le Guernic P, Gautier T (1991) Data-flow to von Neumann: the Signal approach. In: Gaudiot J-L, Bic L (eds) Advanced Topics in Data-Flow Computing. Prentice-Hall, Englewood Cliffs, NJ, pp 413–438Google Scholar
  3. 3.
    Wadge WW (1979) An Extensional treatment of dataflow deadlock. In: Kahn G (ed) Semantics of Concurrent Computation, LNCS vol 70. Springer-Verlag, London, UK, pp 285–299CrossRefGoogle Scholar

Copyright information

© Springer-Verlag New York 2010

Authors and Affiliations

  1. 1.CNRS - UMR 8022 (LIFL)INRIA Lille - Nord Europe Parc scientifique de la Haute BorneVilleneuve d’AscqFrance

Personalised recommendations