Article ID Journal Published Year Pages File Type
434135 Science of Computer Programming 2014 18 Pages PDF
Abstract

•Constructive semantic framework over a complete domain for imperative and declarative synchronous languages.•First executable small-step operational semantics of polychronous data-flow languages.•Characterization of program correctness (determinism, endochrony) by fixpoint properties.

The synchronous paradigm provides a logical abstraction of time for reactive system design which allows automatic synthesis of embedded systems that behave in a predictable, timely, and reactive manner. According to the synchrony hypothesis, a synchronous model reacts to inputs by generating outputs that are immediately made available to the environment. While synchrony greatly simplifies the design of complex systems in general, it can sometimes lead to causal cycles. In these cases, constructiveness is a key property to guarantee that the output of each reaction can still be always algorithmically determined.Polychrony deviates from perfect synchrony by using a partially ordered, i.e., a relational model of time. It encompasses the behaviors of (implicitly) multi-clocked data-flow networks of synchronous modules and can analyze and synthesize them as GALS systems or Kahn process networks (KPNs).In this paper, we present a unified constructive semantic framework using structured operational semantics, which encompasses both the constructive behavior of synchronous modules and the multi-clocked behavior of polychronous networks. Along the way, we define the very first executable operational semantics of the polychronous language Signal.

Related Topics
Physical Sciences and Engineering Computer Science Computational Theory and Mathematics
Authors
, , , , ,