Abstract
Reference passing systems, like mobile and reconfigurable systems are common nowadays. The common feature of such systems is the possibility to form dynamic logical connections between the individual modules. However, such systems are very difficult to verify, as their logical structure is dynamic. Traditionally, decidable fragments of \(\pi \)-calculus, e.g. the well-known Finite Control Processes (FCP), are used for formal modelling of reference passing systems. Unfortunately, FCPs allow only ‘global’ concurrency between processes, and thus cannot naturally express scenarios involving ‘local’ concurrency inside a process, such as multicast. In this paper we propose Extended Finite Control Processes (EFCP), which are more convenient for practical modelling. Moreover, an almost linear translation of EFCPs to FCPs is developed, which enables efficient model checking of EFCPs.
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
Similar content being viewed by others
Notes
- 1.
Some existing tools like SPIN allow to send channels via channels; however, they do not allow dynamic creation of new channels, which is often essential in RPSs.
- 2.
Available from http://service-technology.org/tools/lola.
References
Kwiatkowska, M.Z., Rodden, T., Sassone, V. (eds.): From computers to ubiquitous computing by 2020. In: Proceedings of Philosophical Transactions of the Royal Society, vol. 366 (2008)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, part I. Inf. Comp. 100(1), 1–40 (1992)
Cardelli, L., Gordon, A.: Mobile ambients. In: Nivat, M. (ed.) Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science, vol. 1378, pp. 140–155. Springer, Heidelberg (1998)
Dam, M.: Model checking mobile processes. Inf. Comp. 129(1), 35–51 (1996)
Meyer, R., Khomenko, V., Hüchting, R.: A polynomial translation of \(\pi \)-calculus (FCP) to safe Petri nets. Logical Methods Comput. Sci. 9(3), 1–36 (2013)
Milner, R.: Communicating and Mobile Systems: the \(\pi \)-Calculus. CUP, New York (1999)
Sangiorgi, D., Walker, D.: The \(\pi \)-calculus: A Theory of Mobile Processes. CUP, New York (2001)
Meyer, R., Khomenko, V., Strazny, T.: A practical approach to verification of mobile systems using net unfoldings. Fundam. Inf. 94(3–4), 439–471 (2009)
Furber, S., Temple, S.: Neural systems engineering. In: Fulcher, J., Jain, L. (eds.) Computational Intelligence: A Compendium. Studies in Computational Intelligence, vol. 115, pp. 763–796. Springer, Heidelberg (2008)
Navaridas, J., Luján, M., Miguel-Alonso, J., Plana, L.A., Furber, S.: Understanding the interconnection network of SpiNNaker. In: Proceedings of the 23rd International Conference on Supercomputing, ICS 2009, pp. 286–295. ACM (2009)
Camara, J., Moreto, M., Vallejo, E., Beivide, R., Miguel-Alonso, J., Martinez, C., Navaridas, J.: Mixed-radix twisted torus interconnection networks. In: Parallel and Distributed Processing Symposium IPDPS, pp. 1–10. IEEE (2007)
Plana, L., Bainbridge, J., Furber, S., Salisbury, S., Yebin, S., Jian, W.: An on-chip and inter-chip communications network for the SpiNNaker massively-parallel neural net simulator. In: Second ACM IEEE International Symposium on Networks-on-Chip, 2008, NoCS 2008, pp. 215–216. IEEE Computer Society (2008)
Furber, S., Temple, S., Brown, A.: On-chip and inter-chip networks for modeling large-scale neural systems. In: Circuits and Systems, ISCAS Proceedings, pp. 21–24. IEEE (2006)
Rast, A., Yang, S., Khan, M., Furber, S.: Virtual synaptic interconnect using an asynchronous network-on-chip. In: Proceedings of Intelligence Joint Conference on Neural Networks (IJCNN2008), pp. 2727–2734. IEEE (2008)
Jin, X., Furber, S., Woods, J.: Efficient modelling of spiking neural networks on a scalable chip multiprocessor. In: Neural Networks, IJCNN World Congress on Computational Intelligence, pp. 2812–2819. IEEE (2008)
Asanovic, K., Beck, J., Feldman, J., Morgan, N., Wawrzynek, J.: A supercomputer for neural computation. In: Neural Networks, World Congress on Computational Intelligence, vol. 1, pp. 5–9. IEEE (1994)
Furber, S., Brown, A.: Biologically inspired massively parallel architectures computing beyond a million processors. In: Application of Concurrency to System Design, 2009, ACSD 2009, pp. 3–12. IEEE (2009)
Plana, L., Furber, S., Temple, S., Khan, M., Shi, Y., Wu, J., Yang, S.: A GALS infrastructure for a massively parallel multiprocessor. Des. Test Comput. IEEE 24(5), 454–463 (2007)
Farber, P., Asanovic, K.: Parallel neural network training on multi-spert. In: 3rd International Conference on Algorithms and Architectures for Parallel Processing, ICAPP, pp. 659–666. IEEE (1997)
Wu, J., Furber, S.: A multicast routing scheme for a universal spiking neural network architecture. Comput. J. 53(3), 280–288 (2010)
Puente, V., Gregorio, J.: Immucube: scalable fault-tolerant routing for \(k\)-ary \(n\)-cube networks. IEEE Trans. Parallel Distrib. Syst. 18(6), 776–788 (2007)
Puente, V., Izu, C., Beivide, R., Gregorio, J.A., Vallejo, F., Prellezo, J.M.: The adaptive bubble router. J. Parallel Distrib. Comput. 61(9), 1180–1208 (2001)
Gomez, M., Nordbotten, N., Flich, J., Lopez, P., Robles, A., Duato, J., Skeie, T., Lysne, O.: A routing methodology for achieving fault tolerance in direct networks. IEEE Trans. Comput. 55(4), 400–415 (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Khomenko, V., Germanos, V. (2015). Modelling and Analysis Mobile Systems Using \(\pi \)-calculus (EFCP). In: Koutny, M., Desel, J., Haddad, S. (eds) Transactions on Petri Nets and Other Models of Concurrency X. Lecture Notes in Computer Science(), vol 9410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48650-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-662-48650-4_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-48649-8
Online ISBN: 978-3-662-48650-4
eBook Packages: Computer ScienceComputer Science (R0)