Semantical Aspects of an Architecture for
Distributed Embedded Systems
Roel Bloo,
Jozef Hooman
and Edwin de Jong
Appeared in: Proceedings of the 2000 ACM Symposium on Applied
Computing (SAC 2000), Como, Italy, ACM, Volume 1, pages 149-155, 2000.
ABSTRACT
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
global dataspace.
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.
This result is checked mechanically by means of the interactive
theorem prover
PVS.
Hence, our language allows both convenient reasoning using a global
dataspace and efficient implementation by means of distributed dataspaces.
Since the semantics is denotational, it forms a solid basis
for the formulation of a compositional verification method.
Postscript
Dump file, for PVS version 2.3
Postscript of CS-Report 00-04; an
extended version that appeared as Technical Report at the
Eindhoven University of Technology.