Abstract
Parameterised Networks of Synchronised Automata (pNets) is a machine-oriented semantic formalism used for specifying and verifying the behaviour of distributed components or systems. In addition, it can be used to define the semantics of languages in the parallel and distributed computation area. Unlike other traditional process calculi, pNets only own one pNet node as an operator which composes all subnets running in parallel. Using this single synchronisation artifact, it is capable of expressing many operators or synchronisation mechanisms. In this paper, we explore a denotational semantics for parameterised networks. The denotational semantics of parameterised networks we investigate is based on the behaviours of their subnets. The behaviour of a subnet is determined by both its state and the actions it executes. Based on the traces of a set of subnets, the behaviour of a pNet consisting of those subnets can be deduced. A set of algebraic laws is also explored based on the denotational semantics.
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.
\(\{\{\!x_k\leftarrow e_k\!\}\}^{k\in K}\) is the parallel substitution operation.
- 2.
Card(A) returns the number of elements in the set A.
References
Arnold, A.: Finite Transition Systems - Semantics of Communicating Systems. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1994)
Barros, T., Ameur-Boulifa, R., Cansado, A., Henrio, L., Madelaine, E.: Behavioural models for distributed fractal components. Ann. des Télécommun. 64(1–2), 25–43 (2009)
Baude, F., Caromel, D., Dalmasso, C., Danelutto, M., Getov, V., Henrio, L., Pérez, C.: GCM: a grid extension to fractal for autonomous distributed components. Ann. des Télécommun. 64(1–2), 5–24 (2009)
Henrio, L., Madelaine, E., Zhang, M.: pNets: an expressive model for parameterised networks of processes. In: 23rd Euromicro International Conference on Parallel, Distributed, and Network-Based Processing, PDP 2015, Turku, Finland, March 4–6, 2015, pp. 492–496 (2015)
Henrio, L., Madelaine, E., Zhang, M.: A theory for the composition of concurrent processes. In: Albert, E., Lanese, I. (eds.) FORTE 2016. LNCS, vol. 9688, pp. 175–194. Springer, Heidelberg (2016). doi:10.1007/978-3-319-39570-8_12
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall International Series in Computer Science. Prentice Hall, Upper Saddle River (1998)
Koymans, R., Shyamasundar, R., de Roever, W., Gerth, R., Arun-Kumar, S.: Compositional semantics for real-time distributed computing. Inf. Comput. 79(3), 210–256 (1988)
Milner, R.: Communication and Concurrency. Prentice-Hall Inc., Upper Saddle River (1989)
Nierstrasz, O.: Piccola - a small composition language. In: Object-Oriented Technology, ECOOP 1999, Workshop Reader, ECOOP 1999 Workshops, Panels, and Posters, Lisbon, Portugal, June 14–18, 1999, Proceedings, p. 317 (1999)
Rajan, A., Bavan, S., Abeysinghe, G.: Semantics for a distributed programming language using SACS and weakest pre-conditions. In: International Conference on Advanced Computing and Communications, ADCOM 2006, pp. 434–439, December 2006
Schmitt, A., Stefani, J.-B.: The Kell calculus: a family of higher-order distributed process calculi. In: Priami, C., Quaglia, P. (eds.) GC 2004. LNCS, vol. 3267, pp. 146–178. Springer, Heidelberg (2005). doi:10.1007/978-3-540-31794-4_9
Acknowledgment
This work was partially funded by the Associated Team FM4CPS between INRIA and ECNU, Shanghai. It was also supported by the Danish National Research Foundation and the National Natural Science Foundation of China (No. 61361136002) for the Danish-Chinese Center for Cyber Physical Systems, National Natural Science Foundation of China (Grant No. 61321064), Shanghai Collaborative Innovation Center of Trustworthy Software for Internet of Things (No. ZF1213) and Doctoral Fund of Ministry of Education of China (No. 20120076130003).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Li, S., Madelaine, E. (2017). A Denotational Semantics for Parameterised Networks of Synchronised Automata. In: Bowen, J., Zhu, H. (eds) Unifying Theories of Programming. UTP 2016. Lecture Notes in Computer Science(), vol 10134. Springer, Cham. https://doi.org/10.1007/978-3-319-52228-9_5
Download citation
DOI: https://doi.org/10.1007/978-3-319-52228-9_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-52227-2
Online ISBN: 978-3-319-52228-9
eBook Packages: Computer ScienceComputer Science (R0)