SAC20002000 Como, Italy
Semantical Aspects of an Architecture for
Distributed Embedded SystemsThis research is
supported by the Technology Foundation STW (grant EIF.3959),
applied science division of NWO and the
technology programme of the Dutch Ministry of Economic Affairs.
Eindhoven University of Technology
Eindhoven, The Netherlands
University of Nijmegen
Nijmegen, The Netherlands
Edwin de Jong
Hollandse Signaalapparaten B.V.
Hengelo, The Netherlands
We investigate the formulation of a formal semantics for the
industrial software architecture Splice.
In this paper,
we present a set of basic Splice interaction primitives that is both powerful
and easy to implement.
We define a semantics for this language based on a conceptual
It is shown that the semantics is equivalent to an implementation-biased
semantics where each process has its own local dataspace and communication
is established by means of asynchronous message passing.
Hence, our language allows both convenient reasoning using a global
dataspace and efficient implementation by means of distributed dataspaces.
The equivalence result is checked mechanically by means of the interactive
theorem prover PVS.