Reactive types

Abstract

Synchronous languages, such as SIGNAL, are best suited for the design of dependable real-time systems. Synchronous languages enable a very high-level specification and an extremely modular implementation of complex systems by structurally decomposing them into elementary synchronous processes. Separate compilation in reactive languages is however made a difficult issue by global safety requirements. We give a simple and effective account to the separate compilation of reactive systems by introducing a specification as type paradigm for reactive languages: reactive types. Just as data-types describe the structure of data in conventional languages, reactive types describe the structure of interaction in synchronous languages. We define an inference system for determining reactive types in the SIGNAL language and show how to reconstruct adequate compile-time information on reactive programs by means of such specifications.