Equivalent Semantic Models for a Distributed Dataspace Architecture

  • Jozef Hooman
  • Jaco van de Pol
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2852)


The general aim of our work is to support formal reasoning about components on top of the distributed dataspace architecture Splice. To investigate the basic properties of Splice and to support compositional verification, we have defined a denotational semantics for a basic Splice-like language. To increase the confidence in this semantics, also an operational semantics has been defined which is shown to be equivalent to the denotational one using the theorem prover PVS. A verification framework based on the denotational semantics is applied to an example of top-down development and transparent replication.


Data Item Time Stamp Local Storage Operational Semantic Sequential Composition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [BdJ97]
    Boasson, M., de Jong, E.: Software architecture for large embedded systems. In: IEEE Workshop on Middleware for Distributed Real-Time Systems and Services (1997)Google Scholar
  2. [BHdJ00]
    Bloo, R., Hooman, J., de Jong, E.: Semantical aspects of an architecture for distributed embedded systems. In: Proc. of the 2000 ACM Symposium on Applied Computing (SAC 2000), vol. 1, pp. 149–155. ACM press, New York (2000)CrossRefGoogle Scholar
  3. [BKBdJ98]
    Bonsangue, M.M., Kok, J.N., Boasson, M., de Jong, E.: A software architecture for distributed control systems and its transition system semantics. In: Proc. of the 1998 ACM Symposium on Applied Computing (SAC 1998), pp. 159–168. ACM press, New York (1998)CrossRefGoogle Scholar
  4. [BKZ99]
    Bonsangue, M.M., Kok, J.N., Zavattaro, G.: Comparing coordination models based on shared distributed replicated data. In: Proc. of the 1999 ACM Symposium on Applied Computing (SAC 1999). ACM Press, New York (1999)Google Scholar
  5. [Boa93]
    Boasson, M.: Control systems software. IEEE Transactions on Automatic Control 38(7), 1094–1106 (1993)CrossRefMathSciNetGoogle Scholar
  6. [dRdBH+01]
    de Roever, W.P., de Boer, F., Hannemann, U., Hooman, J., Lakhnech, Y., Poel, M., Zwiers, J.: Concurrency Verification, Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)zbMATHGoogle Scholar
  7. [FHA99]
    Freeman, E., Hupfer, S., Arnold, K.: JavaSpaces: Principles, Patterns, and Practice. Addison-Wesley, Reading (1999)Google Scholar
  8. [Gel85]
    Gelernter, D.: Genarative communication in Linda. Transactions on Programming Languages and Systems 7(1), 80–112 (1985)zbMATHCrossRefGoogle Scholar
  9. [HH02]
    Hannemann, U., Hooman, J.: Formal reasoning about real-time components on a data-oriented architecture. In: Proc. of 6th World Multiconference on Systemics, Cybernetics and Informatics (SCI 2002), vol. XI, pp. 313–318 (2002)Google Scholar
  10. [Hoo94]
    Hooman, J.: Correctness of real time systems by construction. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 19–40. Springer, Heidelberg (1994)Google Scholar
  11. [HvdP02]
    Hooman, J., van de Pol, J.: Formal verification of replication on a distributed data space architecture. In: Proc. of the 2002 ACM Symposium on Applied Computing (SAC 2002), pp. 351–358 (2002)Google Scholar
  12. [Jon83]
    Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Transactions on Programming Languages and Systems 5(4), 596–619 (1983)zbMATHCrossRefGoogle Scholar
  13. [Lam78]
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Communications of the ACM 21(7), 558–565 (1978)zbMATHCrossRefGoogle Scholar
  14. [MC81]
    Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Transactions on Software Engineering 7(7), 417–426 (1981)CrossRefMathSciNetGoogle Scholar
  15. [OSRSC01]
    Owre, S., Shankar, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide. SRI International, Computer Science Laboratory, Menlo Park, CA, version 2.4 edn. (December 2001),

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Jozef Hooman
    • 1
    • 2
  • Jaco van de Pol
    • 2
  1. 1.University of NijmegenNijmegenThe Netherlands
  2. 2.CWI AmsterdamThe Netherlands

Personalised recommendations