Note: [] Address for correspondence: Dipartimento di Informatica, University of Pisa, Corso Italia 40, 56125 Pisa, Italy
Abstract: In synchronous programming, programs can be perceived as purely sequential, and parallelism is only a logical concept useful to develop programs in a modular way. Classical semantics for synchronous languages interpret programs as sequential input/output finite state machines (i/o FSMs) where concurrency disappears. We argue that semantics where concurrency is reflected can be useful at least for improving hardware implementation, verification, and design of model-based schedulers. So, these semantics should not “compete” with the classical ones but should offer different, although consistent, views of programs, each supporting a particular task in their development. In order to define semantics reflecting concurrency, well established techniques adopted to define “truly concurrent” semantics for asynchronous languages could be applied. In this paper, we consider as a prototype of the class of synchronous languages the language Esterel, which is gaining use in a wide variety of applications. Then, following a method proposed by Degano and Priami to give semantics for asynchronous process algebras, we develop a semantic framework in which one can define different, although consistent, semantics of Esterel programs. The idea is to define a very concrete model of the language from which more abstract models can be recovered by means of suitable abstraction functions. We define a proved transition system (PTS) as the most concrete model of Esterel. We show that the classical interpretation in FSMs can be recovered from the PTS by a suitable abstraction function, namely we show that our most concrete semantics is consistent with the classical one. Then, from proved trees obtained by unfolding parts of the PTS, we abstract locality trees and enabling trees. We show how locality trees can be used to improve the hardware implementation of the language, namely to remove redundant latches generated by the compiler. Finally, we show how enabling trees can be used to improve the verification phase, namely to isolate program parts which actually cause the violation of a certain property.
