Copyright ACM, 2000

SAC20002000 Como, Italy 2000

3

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.

Roel Bloo
Eindhoven University of Technology
Eindhoven, The Netherlands
Jozef Hooman
University of Nijmegen
Nijmegen, The Netherlands
Edwin de Jong
Hollandse Signaalapparaten B.V.
Hengelo, The Netherlands

edejong@signaal.nl

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. 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