Abstract
We introduce a method to elicit and to structure using Event B, processes interacting with ad hoc dynamic architecture. A Group Communication System is used as the investigation support. The method takes account of the evolving structure of the interacting processes; it guides the user to structure the abstract system that models his/her requirements. The method also integrates property verification using both theorem proving and model checking. A B specification of a GCS is built using the proposed approach and its stated properties are verified using a B theorem prover and a B model checker.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B Book. Cambridge University Press, Cambridge (1996)
Abrial, J.-R.: Extending B without Changing it (for developping distributed systems). In: Habrias, H. (ed.) Proc. of the 1st Conf. on the B method, France, pp. 169–190 (1996)
Abrial, J.-R., Cansell, D., Mery, D.: Formal Derivation of Spanning Trees Algorithms. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 457–476. Springer, Heidelberg (2003)
Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)
B-Core. B-Toolkit. UK, consulted in 2006 (2006), http://www.b-core.com
Back, R.J., Kurki-Suonio, R.: Decentralisation of Process Nets with Centralised Control. In: Proc. of the 2nd ACM SIGACT-SIGOPS Symp. on Principles of Distributed Computing, pp. 131–142 (1983)
Bickford, M., Kreitz, C., Van Renesse, R., Constable, R.: An Experiment in Formal Design Using Meta-Properties. In: DISCEX, vol. 02, pp. 100–107. IEEE Computer Society, Los Alamitos (2001)
Birman, K., van Renesse, R.: Reliable Distributed Computing with the Isis Toolkit. IEEE Computer Society Press, Los Alamitos (1994)
Butler, M., Walden, M.: Distributed System Development in B. In: Habrias, H. (ed.) Proc. of the 1st Conference on the B method, France, pp. 155–168 (1996)
Cansell, D., Gopalakrishnan, G., Jones, M., Mery, D.: Incremental Proof of the Producer/Consumer Property for the PCI Protocol. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 22–41. Springer, Heidelberg (2002)
Chockler, G.V., Keidar, I., Vitenberg, R.: Group Communication Specifications: a Comprehensive Study. ACM Comput. Surv. 33(4), 427–469 (2001)
ClearSy. Atelier B V3.6. Steria, Aix-en-Provence, France, consulted in 2006 (2006), http://www.clearsy.com
Dolev, D., Malki, D.: The Design of the Transis System. In: Birman, K.P., Mattern, F., Schiper, A. (eds.) Dagstuhl Seminar 1994. LNCS, vol. 938. Springer, Heidelberg (1995)
Powel, D. (Guest ed.): Special Issue on Group Communications Systems. Communications of the ACM, 39(4) (1996)
Constable, R.L., et al.: Implementing Mathematics with the Nuprl Proof Developemnt System. Prentice Hall, Englewood Cliffs (1986)
Hayden, M., Van Renesse, R.: Optimizing Layered Communication Protocols. In: HPDC 1997: Proceedings of the 6th International Symposium on High Performance Distributed Computing (HPDC 1997), Washington, DC, USA, p. 169. IEEE Computer Society, Los Alamitos (1997)
Hickey, J., Lynch, N., van Renesse, R.: Specifications and Proofs for Ensemble Layers. In: Cleaveland, W.R. (ed.) ETAPS 1999 and TACAS 1999. LNCS, vol. 1579, pp. 119–133. Springer, Heidelberg (1999)
Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855–874. Springer, Heidelberg (2003)
Leuschel, M., Turner, E.: Visualizing Larger State Spaces in ProB. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 6–23. Springer, Heidelberg (2005)
ISO LOTOS. A Formal Description Technique Based on The Temporal Ordering of Observational Behaviour. International Organisation for Standardization - Information Processing Systems - Open Systems Interconnection, Geneva, International Standard 8807 (1988)
Lynch, N., Tuttle, M.: Hierarchical Correctness Proofs for Distributed Algorithms (1987)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, D.: A Calculus of Mobile Processes. Journal of Information and Computation 100 (1992)
Roscoe, A.W.: The Theory and Practice of concurrency. Prentice-Hall, Englewood Cliffs (1998)
van Renesse, R., Birman, K.P., Maffeis, S.: Horus: a Flexible Group Communication System. Commun. ACM 39(4), 76–83 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Attiogbé, J.C. (2006). Multi-process Systems Analysis Using Event B: Application to Group Communication Systems. In: Liu, Z., He, J. (eds) Formal Methods and Software Engineering. ICFEM 2006. Lecture Notes in Computer Science, vol 4260. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11901433_36
Download citation
DOI: https://doi.org/10.1007/11901433_36
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-47460-9
Online ISBN: 978-3-540-47462-3
eBook Packages: Computer ScienceComputer Science (R0)