Abstract
In distributed computing, the leadership election has been used to distributively designate a node as the central controller (leader) of a network of nodes. The complexity of the algorithm arises due to the unawareness of every node of who the current leader is. After running the algorithm, however, a unique node in the network must be elected as the leader and recognized as so by the remaining nodes. In this paper, using CSP, we formalise the leadership election algorithm used by our industrial partner. Its verification is feasible only due to the use of a pattern based strategy that allows the verification to be carried out in a fully local manner. The pattern used here is novel and a further contribution of the paper. A refinement relation together with predicate abstraction is used to describe pattern conformance. The mechanisation of the behavioural conformance is carried out using FDR.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998)
Antonino, P.R.G., Oliveira, M.V.M., Sampaio, A.C.A., Kristensen, K.E., Bryans, J.W.: Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification — Extended version. Technical report, UFPE (2013), http://www.cin.ufpe.br/~prga2/tech/techNFM2014.html
Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting families of software systems with process algebras. ACM Transactions on Software Engineering and Methodology 11(4), 386–426 (2002)
Cheung, E., Chen, X., Hsieh, H., Davare, A., Sangiovanni-Vincentelli, A., Watanabe, Y.: Runtime deadlock analysis for system level design. Design Automation for Embedded Systems 13(4), 287–310 (2009)
Cheung, S., Kramer, J.: Context constraints for compositional reachability analysis. ACM Transactions on Software Engineering and Methodology 5(4), 334–377 (1996)
Formal Systems Ltd. FDR: User Manual and Tutorial, version 2.82 (2005)
Garcia-Molina, H.: Elections in a distributed computing system. IEEE Transactions on Computers C-31(1), 48–59 (1982)
He, J., Li, X., Liu, Z.: A theory of reactive components. Electronic Notes in Theoretical Computer Science 160, 173–195 (2006)
Plasil, F., Visnovsky, S.: Behavior protocols for software components. IEEE Transactions on Software Engineering 28(11), 1056–1076 (2002)
Ramos, R., Sampaio, A., Mota, A.: Systematic development of trustworthy component systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 140–156. Springer, Heidelberg (2009)
Ramos, R.T., Sampaio, A.C.A., Mota, A.C.: Conformance notions for the coordination of interaction components. Science of Computer Programming 75(5), 350–373 (2010)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice-Hall Series in Computer Science. Prentice-Hall (1998)
Roscoe, A.W., Brookes, S.D.: Deadlock analysis in networks of communicating processes. Distributed Computing (4), 209–230 (1991)
Roscoe, A.W., Dathi, N.: The pursuit of deadlock freedom. Information and Computation 75(3), 289–327 (1987)
Roscoe, A.W.: Understanding Concurrent Systems, 1st edn. Springer-Verlag New York, Inc., New York (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Antonino, P.R.G., Oliveira, M.M., Sampaio, A.C.A., Kristensen, K.E., Bryans, J.W. (2014). Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_3
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_3
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)