×

zbMATH — the first resource for mathematics

A calculus of quality for robustness against unreliable communication. (English) Zbl 1337.68041
Summary: A main challenge in the development of distributed systems is to ensure that the components continue to behave in a reasonable manner even when communication becomes unreliable. We propose a process calculus, the quality calculus, for programming software components where it becomes natural to plan for default behaviour in case the ideal behaviour fails due to unreliable communication and thereby to increase the quality of service offered by the system. The development is facilitated by a SAT-based robustness analysis to determine whether or not the code is vulnerable to unreliable communication. The framework is illustrated on the design of a fragment of a wireless sensor network, and is substantiated by formal proofs of correctness of the analysis, which relate the original reduction semantics of the calculus to a new semantics with explicit substitutions.

MSC:
68M14 Distributed systems
68Q55 Semantics in the theory of computing
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Software:
COWS; Linda; z3
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Ahuja, Sudhir; Carriero, Nicholas; Gelernter, David, Linda and friends, Computer, 19, 8, 26-34, (1986)
[2] Amadio, Roberto M., An asynchronous model of locality, failure and process mobility, (Coordination, Lect. Notes Comput. Sci., vol. 1282, (1997), Springer), 374-391
[3] Anand, Madhukar; Ives, Zachary; Lee, Insup, Quantifying eavesdropping vulnerability in sensor networks, (DMSN, (2005), ACM), 3-9
[4] Scientific Computing Associates, Linda: User’s guide and reference manual, (1995), Scientific Computing Associates
[5] Bengtson, Jesper; Johansson, Magnus; Parrow, Joachim; Victor, Björn, Psi-calculi: a framework for mobile processes with nominal data and logic, Log. Methods Comput. Sci., 7, 1, (2011) · Zbl 1213.68399
[6] Berger, Martin, Basic theory of reduction congruence for two timed asynchronous pi-calculi, (CONCUR, Lect. Notes Comput. Sci., vol. 3170, (2004), Springer), 115-130 · Zbl 1099.68064
[7] Berger, Martin; Honda, Kohei, The two-phase commitment protocol in an extended pi-calculus, Electron. Notes Theor. Comput. Sci., 39, 1, 21-46, (2000) · Zbl 1260.68258
[8] Berry, Gerard; Boudol, Gerard, The chemical abstract machine, (POPL, (1990), ACM), 81-94 · Zbl 0747.68013
[9] Bettini, Lorenzo; Bono, Viviana; De Nicola, Rocco; Ferrari, Gian Luigi; Gorla, Daniele; Loreti, Michele; Moggi, Eugenio; Pugliese, Rosario; Tuosto, Emilio; Venneri, Betti, The klaim project: theory and practice, (Global Computing, Lect. Notes Comput. Sci., vol. 2874, (2003), Springer), 88-150 · Zbl 1179.68027
[10] Boreale, Michele; Bruni, Roberto; Caires, Luís; De Nicola, Rocco; Lanese, Ivan; Loreti, Michele; Martins, Francisco; Montanari, Ugo; Ravara, António; Sangiorgi, Davide; Vasconcelos, Vasco Thudichum; Zavattaro, Gianluigi, SCC: a service centered calculus, Web Serv. Form. Methods, 38-57, (2006)
[11] Bruni, Roberto, Calculi for service-oriented computing, (SFM, Lect. Notes Comput. Sci., vol. 5569, (2009), Springer), 1-41
[12] Chang, Richard; Jiang, Guofei; Ivancic, Franjo; Sankaranarayanan, Sriram; Shmatikov, Vitaly, Inputs of coma: static detection of denial-of-service vulnerabilities, (CSF’09, (2009), IEEE), 186-199
[13] Dahl, O. J.; Dijkstra, E. W.; Hoare, C. A.R., Structured programming, (1972), Academic Press Ltd. · Zbl 0267.68001
[14] Mendonça de Moura, Leonardo; Bjørner, Nikolaj, Z3: an efficient SMT solver, (TACAS, Lect. Notes Comput. Sci., vol. 4963, (2008), Springer), 337-340
[15] Mendonça de Moura, Leonardo; Bjørner, Nikolaj, Satisfiability modulo theories: introduction and applications, Commun. ACM, 54, 9, 69-77, (2011)
[16] Engelfriet, Joost; Gelsema, Tjalling, A new natural structural congruence in the pi-calculus with replication, Acta Inform., 40, 385-430, (2004) · Zbl 1057.03022
[17] Ferrari, GianLuigi; Montanari, Ugo; Quaglia, Paola, A pi-calculus with explicit substitutions: the late semantics, (MFCS’94, Lect. Notes Comput. Sci., vol. 841, (1994), Springer), 342-351
[18] Francalanza, Adrian; Hennessy, Matthew, A theory of system behaviour in the presence of node and link failures, (CONCUR, Lect. Notes Comput. Sci., vol. 3653, (2005), Springer), 368-382 · Zbl 1134.68340
[19] Deepak Garg; Lal, Akash; Prasad, Sanjiva, Effective chemistry for synchrony and asynchrony, (IFIP TCS, (2004), Kluwer), 479-492 · Zbl 1088.68641
[20] Gligor, Virgil, A note on the denial-of-service problem, (S&P, (1983), IEEE), 139-149
[21] Gligor, Virgil, A note on denial-of-service in operating systems, IEEE Trans. Softw. Eng., 10, 3, 320-324, (1984)
[22] Guidi, Claudio; Lucchi, Roberto; Gorrieri, Roberto; Busi, Nadia; Zavattaro, Gianluigi, Sock: a calculus for service oriented computing, (ICSOC, Lect. Notes Comput. Sci., vol. 4294, (2006), Springer), 327-338
[23] Lapadula, Alessandro; Pugliese, Rosario; Tiezzi, Francesco, A calculus for orchestration of web services, (De Nicola, R., ESOP’07, Lect. Notes Comput. Sci., (2007), Springer) · Zbl 1187.68070
[24] Malik, Sharad; Zhang, Lintao, Boolean satisfiability from theoretical hardness to practical success, Commun. ACM, 52, 8, 76-82, (2009)
[25] Berger, Martin, An interview with Robin milner, (Short Contributions from the Workshop on Algebraic Process Calculi: The First Twenty Five Years and Beyond (PA’05), BRICS Notes Ser., (2005)), 35-45
[26] Meadows, Catherine, A cost-based framework for analysis of denial of service in networks, J. Comput. Secur., 9, 1, 143-164, (2001)
[27] Milner, Robin, A calculus of communicating systems, Lect. Notes Comput. Sci., vol. 92, (1980), Springer · Zbl 0452.68027
[28] Milner, Robin, Functions as processes, (Automata, Languages and Programming, Lect. Notes Comput. Sci., vol. 443, (1990), Springer), 167-180 · Zbl 0766.68036
[29] Milner, Robin, Communicating and mobile systems: the pi-calculus, (1999), Cambridge University Press · Zbl 0942.68002
[30] Nielson, Hanne; Nielson, Flemming; Kreiker, Jörg; Pilegaard, Henrik, From explicit to symbolic types for communication protocols in CCS, (Formal Modeling: Actors, Open Systems, Biological Systems, Lect. Notes Comput. Sci., vol. 7000, (2011), Springer), 74-89
[31] Riis Nielson, Hanne; Nielson, Flemming, Probabilistic analysis of the quality calculus, (FMOODS/FORTE, Lect. Notes Comput. Sci., vol. 7892, (2013), Springer), 258-272 · Zbl 1390.68484
[32] Riis Nielson, Hanne; Nielson, Flemming, Safety versus security in the quality calculus, (TPFM, Lect. Notes Comput. Sci., vol. 8051, (2013), Springer), 285-303 · Zbl 1390.68484
[33] Riis Nielson, Hanne; Nielson, Flemming; Vigo, Roberto, A calculus for quality, (FACS’12, Lect. Notes Comput. Sci., vol. 7684, (2013), Springer), 188-204 · Zbl 1337.68041
[34] Parrow, Joachim, An introduction to the π-calculus, (Bergstra, J. A.; Ponse, A.; Smolka, S. A., Handbook of Process Algebra, (2001), Elsevier), 479-544 · Zbl 1035.68071
[35] Pilegaard, Henrik; Nielson, Flemming; Riis Nielson, Hanne, Pathway analysis for bioambients, J. Log. Algebr. Program., 77, 92-130, (2008) · Zbl 1147.92002
[36] Riely, James; Hennessy, Matthew, A typed language for distributed mobile processes (extended abstract), (POPL, (1998), ACM), 378-390
[37] Riely, James; Hennessy, Matthew, Distributed processes and location failures, Theor. Comput. Sci., 266, 1-2, 693-735, (2001) · Zbl 0989.68007
[38] Sangiorgi, Davide; Walker, David, The pi-calculus - A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[39] Vigo, Roberto; Nielson, Flemming; Riis Nielson, Hanne, Broadcast, denial-of-service, and secure communication, (iFM, Lect. Notes Comput. Sci., vol. 7940, (2013)), 410-427
[40] Vigo, Roberto; Nielson, Flemming; Riis Nielson, Hanne, Automated generation of attack trees, (CSF’14, (2014), IEEE), 337-350
[41] Vigo, Roberto; Nielson, Flemming; Riis Nielson, Hanne, Uniform protection for multi-exposed targets, (FORTE, Lect. Notes Comput. Sci., vol. 8461, (2014), Springer), 182-198
[42] Wang, Shuling; Nielson, Flemming; Riis Nielson, Hanne, Denial-of-service security attack in the continuous-time world, (FORTE, Lect. Notes Comput. Sci., vol. 8461, (2014), Springer), 149-165
[43] Zeng, Kebin; Nielson, Flemming; Riis Nielson, Hanne, The stochastic quality calculus, (Coordination, Lect. Notes Comput. Sci., vol. 8459, (2014), Springer), 179-193 · Zbl 1454.68079
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.