Semantical aspects of an architecture for distributed embedded systems
Roel Bloo, Jozef Hooman, Edwin D. de Jong · 2000
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. 1. INTRODUCTION This introduction contains an overview of the general context of our research, an informal explanation of the Splice architecture and the aims of the work described here. 1.1 Context of the research Our research concerns the construction o...