Verifiable abstractions for contract-oriented systems. (English) Zbl 1353.68194
Summary: We address the problem of modelling and verifying contract-oriented systems, wherein distributed agents may advertise and stipulate contracts, but – differently from most other approaches to distributed agents – are not assumed to always respect them. A key issue is that the honesty property, which characterises those agents which respect their contracts in all possible execution contexts, is undecidable in general. The main contribution of this paper is a sound verification technique for honesty, targeted at agents modelled in a value-passing version of the calculus \(\mathrm{CO}_{2}\). To do that, we safely over-approximate the honesty property by abstracting from the actual values and from the contexts a process may be engaged with. Then, we develop a model-checking technique for this abstraction, we describe its implementation in Maude, and we discuss some experiments with it.
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
| 68Q42 | Grammars and rewriting systems |
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
References:
| [1] | Bartoletti, M.; Zunino, R., A calculus of contracting processes, (LICS (2010)), 332-341 |
| [2] | Mukhija, A.; Dingwall-Smith, A.; Rosenblum, D., QOS-aware service composition in Dino, (ECOWS (2007)), 3-12 |
| [3] | Bartoletti, M.; Tuosto, E.; Zunino, R., Contract-oriented computing in \(CO_2\), Sci. Ann. Comput. Sci., 22, 1, 5-60 (2012) · Zbl 1424.68097 |
| [4] | Bravetti, M.; Zavattaro, G., Towards a unifying theory for choreography conformance and contract compliance, (Software Composition (2007)), 34-50 |
| [5] | Honda, K.; Vasconcelos, V. T.; Kubo, M., Language primitives and type disciplines for structured communication-based programming, (ESOP. ESOP, LNCS, vol. 1381 (1998)), 22-138 |
| [6] | Honda, K.; Yoshida, N.; Carbone, M., Multiparty asynchronous session types, (POPL (2008), ACM), 273-284 · Zbl 1295.68150 |
| [7] | Castagna, G.; Gesbert, N.; Padovani, L., A theory of contracts for web services, ACM Trans. Program. Lang. Syst., 31, 5, 19:1-19:61 (2009) |
| [8] | van der Aalst, W. M.P.; Lohmann, N.; Massuthe, P.; Stahl, C.; Wolf, K., Multiparty contracts: agreeing and implementing interorganizational processes, Comput. J., 53, 1, 90-106 (2010) |
| [9] | Bartoletti, M.; Cimoli, T.; Pinna, G. M., Lending Petri nets and contracts, (FSEN. FSEN, LNCS, vol. 8161 (2013), Springer), 66-82 · Zbl 1434.68321 |
| [10] | Bartoletti, M.; Cimoli, T.; Pinna, G. M., Lending Petri nets, Sci. Comput. Program. (2015) · Zbl 1434.68321 |
| [11] | Bartoletti, M.; Cimoli, T.; Zunino, R., A theory of agreements and protection, (POST. POST, LNCS, vol. 7796 (2013), Springer), 186-205 · Zbl 1390.68066 |
| [12] | Bartoletti, M.; Cimoli, T.; Pinna, G. M.; Zunino, R., Contracts as games on event structures, J. Log. Algebr. Methods Programm. (2015), in press |
| [13] | Honda, K., Types for dyadic interaction, (CONCUR (1993)), 509-523 |
| [14] | Bocchi, L.; Honda, K.; Tuosto, E.; Yoshida, N., A theory of design-by-contract for distributed multiparty interactions, (CONCUR (2010)), 162-176 · Zbl 1287.68121 |
| [15] | Castagna, G.; Dezani-Ciancaglini, M.; Padovani, L., On global types and multi-party session, Log. Methods Comput. Sci., 8, 1 (2012) · Zbl 1238.68026 |
| [16] | Lange, J.; Tuosto, E., Synthesising choreographies from local session types, (CONCUR (2012)), 225-239 · Zbl 1364.68291 |
| [17] | Deniélou, P.-M.; Yoshida, N., Multiparty compatibility in communicating automata: characterisation and synthesis of global session types, (ICALP (2013)), 174-186 · Zbl 1334.68149 |
| [18] | Caires, L.; Pfenning, F., Session types as intuitionistic linear propositions, (CONCUR (2010)), 222-236 · Zbl 1287.68125 |
| [19] | Wadler, P., Propositions as sessions, J. Funct. Program., 24, 2-3, 384-418 (2014) · Zbl 1307.68025 |
| [20] | Gay, S. J.; Vasconcelos, V. T., Linear type theory for asynchronous session types, J. Funct. Program., 20, 1, 19-50 (2010) · Zbl 1185.68194 |
| [21] | Carbone, M.; Montesi, F.; Schürmann, C., Choreographies, logically, (CONCUR (2014)), 47-62 · Zbl 1417.68121 |
| [22] | Bernardi, G.; Hennessy, M., Using higher-order contracts to model session types, (CONCUR (2014)), 387-401 · Zbl 1417.68116 |
| [23] | Bartoletti, M.; Scalas, A.; Zunino, R., A semantic deconstruction of session types, (CONCUR (2014)), 402-418 · Zbl 1417.68115 |
| [24] | Corin, R.; Deniélou, P.-M.; Fournet, C.; Bhargavan, K.; Leifer, J. J., A secure compiler for session abstractions, J. Comput. Secur., 16, 5 (2008) |
| [25] | Yoshida, N.; Hu, R.; Neykova, R.; Ng, N., The scribble protocol language, (TGC (2013)), 22-41 |
| [26] | Neykova, R.; Yoshida, N., Multiparty session actors, (COORDINATION (2014)), 131-146 |
| [27] | Franco, J.; Vasconcelos, V. T., A concurrent programming language with refined session types, (SEFM Workshops: BEAT2 (2013)), 15-28 |
| [28] | Bartoletti, M.; Castellani, I.; Denilou, P.-M.; Dezani-Ciancaglini, M.; Ghilezan, S.; Pantovic, J.; Prez, J. A.; Thiemann, P.; Toninho, B.; Vieira, H. T., Combining behavioural types with security analysis, J. Log. Algebr. Methods Programm. (2015) · Zbl 1330.68045 |
| [29] | Gay, S. J.; Hole, M., Types and subtypes for client-server interactions, (ESOP (1999)), 74-90 |
| [31] | Barbanera, F.; de’Liguoro, U., Two notions of sub-behaviour for session-based client/server systems, (PPDP (2010)), 155-164 |
| [32] | Bartoletti, M.; Tuosto, E.; Zunino, R., On the realizability of contracts in dishonest systems, (COORDINATION. COORDINATION, LNCS, vol. 7274 (2012)), 245-260 · Zbl 1366.68198 |
| [33] | Bartoletti, M.; Scalas, A.; Tuosto, E.; Zunino, R., Honesty by typing, (FMOODS/FORTE. FMOODS/FORTE, LNCS, vol. 7892 (2013)), 305-320 |
| [34] | Bartoletti, M.; Murgia, M.; Scalas, A.; Zunino, R., The \(CO_2\) honesty checker (2015) |
| [35] | Bartoletti, M.; Cimoli, T.; Zunino, R., Compliance in behavioural contracts: a brief survey, (Programming Languages with Applications to Biology and Security. Programming Languages with Applications to Biology and Security, LNCS, vol. 9465 (2015), Springer International Publishing), 103-121 · Zbl 1434.68045 |
| [36] | Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J. F., Maude: specification and programming in rewriting logic, Theor. Comput. Sci., 285, 2, 187-243 (2002) · Zbl 1001.68059 |
| [37] | Eker, S.; Meseguer, J.; Sridharanarayanan, A., The Maude LTL model checker, Electron. Notes Theor. Comput. Sci., 71, 162-187 (2002) · Zbl 1272.68243 |
| [38] | Verdejo, A.; Martí-Oliet, N., Implementing CCS in Maude 2, WRLA 2002. WRLA 2002, Electron. Notes Theor. Comput. Sci.Rewriting Logic and Its Applications, 71, 282-300 (2002) |
| [39] | Meseguer, J., Rewriting as a unified model of concurrency, (CONCUR. CONCUR, LNCS, vol. 458 (1990)), 384-400 |
| [40] | Thati, P.; Sen, K.; Martí-Oliet, N., An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0, ENTCS, 71, 261-281 (2002) · Zbl 1272.68322 |
| [41] | Stehr, M.-O.; Meseguer, J.; Ölveczky, P. C., Rewriting logic as a unifying framework for Petri nets, (Unifying Petri Nets (2001)), 250-303 · Zbl 1017.68080 |
| [43] | Wirsing, M.; Eckhardt, J.; Mühlbauer, T.; Meseguer, J., Design and analysis of cloud-based architectures with KLAIM and Maude, (WRLA. WRLA, LNCS, vol. 7571 (2012)), 54-82 |
| [44] | Bruni, R.; Corradini, A.; Gadducci, F.; Lluch-Lafuente, A.; Vandin, A., Modelling and analyzing adaptive self-assembly strategies with Maude, (WRLA. WRLA, LNCS, vol. 7571 (2012)), 118-138 |
| [45] | Meseguer, J., Twenty years of rewriting logic, J. Log. Algebr. Program., 81, 7-8 (2012) · Zbl 1267.03043 |
| [46] | Lange, J.; Scalas, A., Choreography synthesis as contract agreement, (ICE (2013)), 52-67 · Zbl 1464.68252 |
| [47] | Bartoletti, M.; Lange, J.; Scalas, A.; Zunino, R., Choreographies in the wild, Sci. Comput. Program., 109, 36-60 (2015) |
| [48] | Bartoletti, M.; Cimoli, T.; Murgia, M.; Podda, A. S.; Pompianu, L., A contract-oriented middleware, (FACS. FACS, LNCS (2015), Springer) |
| [49] | Bartoletti, M.; Cimoli, T.; Murgia, M.; Podda, A. S.; Pompianu, L., Compliance and subtyping in timed session types, (FORTE (2015)), 161-177 · Zbl 1347.68025 |
| [50] | Saraswat, V. A.; Rinard, M. C., Concurrent constraint programming, (POPL (1990)), 232-245 |
| [51] | Buscemi, M. G.; Montanari, U., CC-Pi: a constraint-based language for specifying service level agreements, (ESOP (2007)), 18-32 · Zbl 1187.68063 |
| [52] | Chen, T.-C.; Bocchi, L.; Denilou, P.-M.; Honda, K.; Yoshida, N., Asynchronous distributed monitoring for multiparty session enforcement, (Bruni, R.; Sassone, V., Trustworthy Global Computing. Trustworthy Global Computing, Lecture Notes in Computer Science, vol. 7173 (2012), Springer: Springer Berlin, Heidelberg), 25-45 |
| [53] | Bocchi, L.; Chen, T.-C.; Demangeon, R.; Honda, K.; Yoshida, N., Monitoring networks through multiparty session types, (FORTE. FORTE, LNCS, vol. 7892 (2013), Springer), 50-65 |
| [54] | Ligatti, J.; Bauer, L.; Walker, D., Run-time enforcement of nonsafety policies, ACM Trans. Inf. Syst. Secur., 12, 3 (2009) |
| [55] | Bartoletti, M.; Zunino, R., On the decidability of honesty and of its variants, (WSFM-BEAT. WSFM-BEAT, LNCS (2015), Springer) |
| [56] | Takeuchi, K.; Honda, K.; Kubo, M., An interaction-based language and its typing system, (PARLE (1994)), 398-413 |
| [57] | Dezani-Ciancaglini, M.; de’Liguoro, U.; Yoshida, N., On progress for structured communications, (Trustworthy Global Computing. Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007 (2007)), 257-275, France, 2007, Revised Selected Papers |
| [58] | Bettini, L.; Coppo, M.; D’Antoni, L.; Luca, M. D.; Dezani-Ciancaglini, M.; Yoshida, N., Global progress in dynamically interleaved multiparty sessions, (CONCUR (2008)), 418-433 · Zbl 1160.68456 |
| [59] | Castagna, G.; Dezani-Ciancaglini, M.; Giachino, E.; Padovani, L., Foundations of session types, (PPDP (2009)), 219-230 |
| [60] | Coppo, M.; Dezani-Ciancaglini, M.; Padovani, L.; Yoshida, N., Inference of global progress properties for dynamically interleaved multiparty sessions, (COORDINATION (2013)), 45-59 |
| [61] | Carbone, M.; Montesi, F., Deadlock-freedom-by-design: multiparty asynchronous global programming, (POPL (2013)), 263-274 · Zbl 1301.68097 |
| [62] | Bartoletti, M.; Murgia, M.; Scalas, A.; Zunino, R., Modelling and verifying contract-oriented systems in Maude, (WRLA. WRLA, LNCS, vol. 8663 (2014)), 130-146 · Zbl 1366.68197 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
