Copyright ACM, 2000
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.
Copyright 2000 ACM
Permission to make digital or hard copies of all or part of this work for
personal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy
otherwise, to republish, to post on servers or to redistribute to lists,
requires prior specific permission and or fee.
SAC 2000 March 19-21 Como, Italy
(c) 2000 ACM 1-58113-239-5/00/003>...>$5.00