A Module Language for Typing SIGNAL Programs by Contracts

Yann Glouche (1) , Thierry Gautier (1) , Paul Le Guernic (1) , Jean-Pierre Talpin (1)

1 ESPRESSO - Synchronous programming for the trusted component-based engineering of embedded systems and mission-critical systems

Chapter 5, on "A Module Language for Typing SIGNAL Programs by Contracts", brings up the polychronous model of computation to present a means to modularly and compositionally support assumption-guarantee reasoning in that framework. Contract-based design has become a popular reasoning concept in which contracts are used to negotiate the correctness of assumptions made on th definition of a component at the point where it is used and provides guarantees to its environment. The chapter first elaborates formal foundations by defining a Boolean algebra of contracts in a trace-theoretical framework. Based on that contracts algebra, a general-purpose module language is then specified. The algebra and module system are instantiated to the framework of the synchronous data-flow language Signal. This presentation is illustrated with the specification of a protocol for Loosely Time-Triggered Architectures (LTTA).

Domaines: Informatique et langage [cs.CL]

Yann Glouche, Thierry Gautier, Paul Le Guernic, Jean-Pierre Talpin. A Module Language for Typing SIGNAL Programs by Contracts. Sandeep K. Shukla and Jean-Pierre Talpin. Synthesis of Embedded Software, Springer, pp.147-171, 2010, ⟨10.1007/978-1-4419-6400-7_5⟩. ⟨hal-00554322⟩