×

zbMATH — the first resource for mathematics

A monotone framework for CCS. (English) Zbl 1387.68172
Summary: The calculus of communicating systems, CCS, was introduced by R. Milner [Communicating and mobile systems: the \(\pi\)-calculus. Cambridge: Cambridge University Press (1999; Zbl 0942.68002)] as a calculus for modelling concurrent systems. Subsequently several techniques have been developed for analysing such models in order to get further insight into their dynamic behaviour. In this paper, we present a static analysis for approximating the control structure embedded within the models. We formulate the analysis as an instance of a monotone framework and thus draw on techniques that often are associated with the efficient implementation of classical imperative programming languages. We show how to construct a finite automaton that faithfully captures the control structure of a CCS model. Each state in the automaton records a multiset of the enabled actions and appropriate transfer functions are developed for transforming one state into another. A classical worklist algorithm governs the overall construction of the automaton and its termination is ensured using techniques from abstract interpretation.

MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Honda K, Vasconcelos VT, Kubo M. Language primitives and type discipline for structured communication-based programming. In: Programming languages and systems (ESOP). Lecture notes in computer science, vol. 1381. Berlin: Springer; 1998. p. 122-38.
[2] Neubauer M, Thiemann P. An implementation of session types. In: Practical aspects of declarative languages (PADL). Lecture notes in computer science, vol. 3057. Berlin: Springer; 2004. p. 56-70.
[3] Vasconcelos VT, Ravara A, Gay SJ. Session types for functional multithreading. In: CONCUR—concurrency theory. Lecture notes in computer science, vol. 3170. Berlin: Springer; 2004. p. 497-511. · Zbl 1099.68677
[4] Bodei, C.; Degano, P.; Nielson, F.; Riis Nielson, H., Static analysis for the \(\pi\)-calculus with applications to security, Information and computation, 168, 68-92, (2001) · Zbl 1007.68118
[5] Braghin, C.; Cortesi, A.; Luccio, F.L.; Focardi, R.; Piazza, C., Nesting analysis of mobile ambients, Computer languages, systems and structures, 30, 3-4, 207-230, (2004) · Zbl 1072.68066
[6] Nielson, F.; Riis Nielson, H.; Hansen, R.R., Validating firewalls using flow logics, Theoretical computer science, 283, 2, 381-418, (2002) · Zbl 1016.68003
[7] Riis Nielson, H.; Nielson, F., Shape analysis for mobile ambients, Nordic journal of computing, 8, 233-275, (2001) · Zbl 0985.68039
[8] Riis Nielson H, Nielson F, Buchholtz M. Security for mobility. In: Focardi R, Gorrieri R, editors. Foundations of security analysis and design II. Lecture notes in computer science, vol. 2946. Berlin: Springer; 2004. p. 207-66. · Zbl 1202.68173
[9] Bodei, C.; Buchholtz, M.; Degano, P.; Nielson, F.; Riis Nielson, H., Static validation of security protocols, Journal of computer security, 13, 347-390, (2005)
[10] Bodei, C.; Degano, P.; Riis Nielson, H.; Nielson, F., Flow logic for dolev – yao secrecy in cryptographic processes, Future generation computer systems, 18, 6, 747-756, (2002) · Zbl 1046.68048
[11] Buchholz, M.; Riis Nielson, H.; Nielson, F., A calculus for control flow analysis of security protocols, International journal of information security, 2, 145-167, (2004)
[12] Nanz, S.; Hankin, C., A framework for security analysis of mobile wireless networks, Theoretical computer science, 367, 1-2, 203-227, (2006) · Zbl 1153.68322
[13] Nielson, F.; Riis Nielson, H.; Seidl, H., Cryptographic analysis in cubic time, Electronic notes of theoretical computer science, 62, 7-23, (2002) · Zbl 1268.94029
[14] Milner, R., Communicating and mobile systems: the pi-calculus, (1999), Cambridge University Press Cambridge · Zbl 0942.68002
[15] Cousot, P.; Cousot, R., Systematic design of program analysis frameworks, (), 269-282 · Zbl 0788.68094
[16] Nielson F, Riis Nielson H, Hankin CL. Principles of program analysis. Berlin: Springer; 1999 [Second printing. Berlin: Springer; 2005]. · Zbl 1069.68534
[17] Sagiv M, Reps T, Wilhelm R. Parametric shape analysis via 3-valued logic. In: Symposium on principles of programming languages (POPL). New York: ACM Press; 1999. p. 105-18.
[18] Riis Nielson H, Nielson F. Data flow analysis for CCS. In: Program analysis and compilation, theory and practice. Lecture notes in computer science, vol. 4444. Berlin: Springer; 2007. p. 311-27. · Zbl 1149.68361
[19] Riis Nielson H, Nielson F. A flow-sensitive analysis of privacy properties. In: Proceedings of computer security foundations symposium (CSF), 2007. IEEE Computer Society; 2007. p. 249-64. · Zbl 1149.68361
[20] Regev, A.; Panina, E.M.; Silverman, W.; Cardelli, L.; Shapiro, E., Bioambients: an abstraction for biological compartments, Theoretical computer science, 325, 1, 141-167, (2004) · Zbl 1069.68569
[21] Cardelli, L.; Gordon, A.D., Mobile ambients, Theoretical computer science, 240, 1, 177-213, (2000) · Zbl 0954.68108
[22] Pilegaard, H.; Nielson, F.; Riis Nielson, H., Pathway analysis for bioambients, Journal of logic and algebraic programming, 77, 92-130, (2008) · Zbl 1147.92002
[23] Riis Nielson H, Nielson F, Pilegaard H. Spatial analysis of BioAmbients. In: Proceedings of the SAS’04. Lecture notes in computer science. Berlin: Springer; 2004. p. 69-83. · Zbl 1104.68420
[24] Nanz S, Nielson F, Riis Nielson H. Topology-dependent abstractions of broadcast networks. In: CONCUR 2007—concurrency theory, 18th international conference. Lecture notes in computer science, vol. 4703. Berlin: Springer; 2007. p. 226-40. · Zbl 1151.68322
[25] Bettini L, Bono V, De Nicola R, Ferrari G, Gorla D, Loreti M, Moggi M, Pugliese R, Tuosto E, Venneri B. The Klaim project: theory and practice. In: Proceedings of the IST/FET international workshop on global computing: programming environments, languages, security and analysis of systems (GC’03). Lecture notes in computer science, vol. 2874. Berlin: Springer; 2003. · Zbl 1179.68027
[26] Nanz S, Nielson F, Riis Nielson H. Modal abstractions of concurrent behaviour. In: Proceedings of the SAS’08. Lecture notes in computer science, vol. 5079. Berlin: Springer; 2008. p. 159-73. · Zbl 1149.68407
[27] De Nicola R, Vaandrager FW. Action versus state based logics for transition systems. In: Proceedings of the LITP spring school on semantics of systems of concurrent processes. Lecture notes in computer science, vol. 469, 1990. p. 407-19.
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.