S-Net is a declarative coordination language rooted in stream processing with a runtime that automatically
distributes the computational units among available resources. It is conceived in response to the
change of processor development trend, from making the speed faster to embedding more cores. For performance
reasons, the S-Net compiler is responsible for generating some additional information, through
type inference, which is used by the runtime to make data delivery decisions. This requires the compiler
to be supported by a sound type system which can ensure that the program behaviour meets the
expectations of the language designers and the programmers.
However, due to S-Net's design principle of ease of use, the S-Net type system was believed to be
simple and was only informally documented. As we empirically tested the type inference implementation,
we gradually revealed the hidden complexity of the calculus behind the apparently easy-to-use language,
which was clearly beyond the capability of the informal type system. We then attempted several formulations
of the type system, each addressing more issues we have found, but a complete solution was still
missing. S-Net now urgently needs a formal type system with proofs of soundness.
We have identified a major issue which has been making it difficult to design a correct type system,
that is the type-semantics interdependency. In this thesis, we present a new design of the S-Net semantics
and type system with no type-semantics interdependency, in terms of a new language BL-Net, a reduced
S-Net which preserves only the type-related behaviour, which has an operational semantics reflecting
that of S-Net, and a type system with the soundness and completeness proof. Our contributions also
include a bridging solution to fit the new type system into the existing compiler structure.