Modeling Communication Semantics for Distributed Systems in Event-B

• Fernando Luís Dotti PUCRS
• Leila Ribeiro UFRGS

DOI: https://doi.org/10.5753/wtf.2012.23083

Resumo

During the development of algorithms for distributed systems, one has to adopt clear assumptions about the semantics offered by the underlying communication platform in order to show that the algorithms under construction fulfill the expected liveness and safety properties. In this paper we propose a library of reusable formal specifications defining several classic communication semantics. The specification of each communication semantics is presented along with the proofs of the expected main properties of each model. The library was build using Event-B and properties were shown using the theorem proving approach with the Rodin system. While modeling a distributed application one can reuse models from the proposed library (by refinement or extension) without having to redo all the proofs related to the communication platform. Moreover, existing proofs can be used to show desired properties of the application.

Referências

Abrial, J. R. (2005). The B-Book: Assigning Programs to Meanings. Cambridge University Press.

Abrial, J.-R. (2010). Modeling in Event-B: System and Software Engineering. Cambridge University Press, New York, NY, USA, 1st edition.

Birman, K. P. (1996). Building secure and reliable network applications. Manning Publications, USA.

Bryans, J., Fitzgerald, J., Romanovsky, A., and Roth, A. (2009). Formal modelling and analysis of business information applications with fault tolerant middleware. In Proceedings of the 2009 14th IEEE International Conference on Engineering of Complex

Computer Systems, ICECCS ’09, pages 68–77. IEEE Computer Society.

DEPLOY Project. Event-b and the rodin platform. http://www.event-b.org/ (last accessed April 2nd 2012).

Hoang, T. S., Fürst, A., and Abrial, J.-R. (2009). Event-B patterns and their tool support. In Hung, D. V. and Krishnan, P., editors, SEFM, pages 210–219. IEEE Computer Society.

Hoare, C. A. R. (1985). Communicating Sequential Processes. Prentice Hall.

Holzmann, G. J. (1997). The model checker SPIN. IEEE Trans. on Soft. Eng., 23(5):279–295.

Lamport, L. (1978). Time, clocks and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565.

Laprie, J.-C., Randell, B., Avizienis, A., and Landwehr, C. (2004). Basic concepts and taxonomy of dependable and secure computing. IEEE Trans. Dependable Secur. Comput., 1(1):11–33.

Lynch, N. and Tuttle, M. (1989). An introduction to input/output automata. CWI-Quarterly, 2(3):219–246.

Milner, R. (1999). Communicating and mobile systems: the π-calculus. Cambridge University Press, USA.

Ribeiro, L., dos Santos, O. M., Dotti, F. L., and Foss, L. (2011). Correct transformation: From object-based graph grammars to promela. Science of Computer Programming, In Press, Corrected Proof:–.

Ricart, G. and Agrawala, A. K. (1981). An optimal algorithm for mutual exclusion in computer networks. Commun. ACM, 24(1):9–17.