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.