Formal verification of replication on a distributed data space architecture

ABSTRACT

We investigate the formal verification of safety-critical systems on top of the distributed data space architecture Splice. In Splice each component has its own local data space which can be kept small using keys, time stamps and selective over-writing. We use two complementary formal tools: first the µCRL tool set for a rapid investigation of alternatives by a limited verification with state space exploration techniques; next the most promising solutions are verified in general by means of the interactive theorem prover of PVS. These formal techniques are used to investigate transparent replication of certain components on top of Splice. We prove that a convenient solution can be obtained by means of a slight extension of the write primitive of Splice.

REFERENCES

• 1: J. Bergstra and J. Klop. Algebra of communicating processes with abstraction. TCS, 37(1):77-121, 1985.
• 2: Stefan Blom , Wan Fokkink , Jan Friso Groote , Izak van Langevelde , Bert Lisser , Jaco van de Pol, µCRL: A Toolset for Analysing Algebraic Specifications, Proceedings of the 13th International Conference on Computer Aided Verification, p.250-254, July 18-22, 2001
• 3: Roel Bloo , Jozef Hooman , Edwin de Jong, Semantical aspects of an architecture for distributed embedded systems, Proceedings of the 2000 ACM symposium on Applied computing, p.149-155, March 2000, Como, Italy [doi>10.1145/335603.335731]
• 4: M. Boasson, Control systems software. IEEE Trans. on Automatic Control, 38(7):1094-1106, July 1993.
• 5: Marcello M. Bonsangue , Joost N. Kok , G. Zavattaro, Comparing coordination models based on shared distributed replicated data, Proceedings of the 1999 ACM symposium on Applied computing, p.156-165, February 28-March 02, 1999, San Antonio, Texas, United States [doi>10.1145/298151.298226]
• 6: Nadia Busi , Roberto Gorrieri , Gianluigi Zavattaro, Process Calculi for Coordination: From Linda to JavaSpaces, Proceedings of the 8th International Conference on Algebraic Methodology and Software Technology, p.198-212, May 20-27, 2000
• 7: Nicholas Carriero , David Gelernter, How to write parallel programs: a first course, MIT Press, Cambridge, MA, 1990
• 8: Paul Dechering , Edwin de Jong, Transparent Object Replication: A Formal Model, Proceedings of the Fifth International Workshop on Object-Oriented Real-Time Dependable Systems, p.43, November 18-19, 1999
• 9: Paul Dechering , Edwin de Jong , Rix Groenboom , Jan Tijmen Udding, Formalization of a Software Architecture for Embedded Systems: A Process Algebra for SPLICE, Proceedings of the Thirty-Second Annual Hawaii International Conference on System Sciences-Volume 3, p.3050, January 05-08, 1999
• 10: Paul Dechering , Izak van Langevelde, On the Verification of Coordination, Proceedings of the 4th International Conference on Coordination Languages and Models, p.335-340, September 11-13, 2000
• 11: Jean-Claude Fernandez , Hubert Garavel , Alain Kerbrat , Laurent Mounier , Radu Mateescu , Mihaela Sighireanu, CADP - A Protocol Validation and Verification Toolbox, Proceedings of the 8th International Conference on Computer Aided Verification, p.437-440, August 03, 1996
• 12: Wan Fokkink , W. Fokkink , W. Brauer , G. Rozenberg , A. Salomaa, Introduction to Process Algebra, Springer-Verlag New York, Inc., Secaucus, NJ, 2000
• 13: Eric Freeman , Ken Arnold , Susanne Hupfer, JavaSpaces Principles, Patterns, and Practice, Addison-Wesley Longman Ltd., Essex, UK, 1999
• 14: Rob J. van Glabbeek , W. Peter Weijland, Branching time and abstraction in bisimulation semantics, Journal of the ACM (JACM), v.43 n.3, p.555-600, May 1996 [doi>10.1145/233551.233556]
• 15: J. Groote and M. Reniers. Algebraic process verification. In J. Bergstra et al., editor, Handbook of Process Algebra, chapter 17. Elsevier, 2001.
• 16: Ulrich Hannemann , Jozef Hooman, Formal Design of Real-Time Components on a Shared Data Space Architecture, Proceedings of the 25th International Computer Software and Applications Conference on Invigorating Software Development, p.143-150, October 08-12, 2001
• 17: Jozef Hooman, Correctness of Real Time Systems by Construction, Proceedings of the Third International Symposium Organized Jointly with the Working Group Provably Correct Systems on Formal Techniques in Real-Time and Fault-Tolerant Systems, p.19-40, September 19-23, 1994
• 18: J. Hooman and J. van de Pol. Verifying replication on a distributed shared data space with time stamps. In Proc. 2nd Workshop on Embedded Systems, pages 107-120. STW, Utrecht, NL, 2001.
• 19: R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
• 20: Sam Owre , John Rushby , Natarajan Shankar , Friedrich von Henke, Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS, IEEE Transactions on Software Engineering, v.21 n.2, p.107-125, February 1995 [doi>10.1109/32.345827]
• 21: J. C. Pol, Expressiveness of basic splice, CWI (Centre for Mathematics and Computer Science), Amsterdam, The Netherlands, 2000

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Reliability, Verification

Keywords:
coordination, data space architecture, formal verification, model-checking, theorem proving