{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T17:57:21Z","timestamp":1725818241955},"publisher-location":"Cham","reference-count":67,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319163093"},{"type":"electronic","value":"9783319163109"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-16310-9_3","type":"book-chapter","created":{"date-parts":[[2015,3,3]],"date-time":"2015-03-03T12:47:23Z","timestamp":1425386843000},"page":"107-159","source":"Crossref","is-referenced-by-count":9,"title":["Correctness of Service Components and Service Component Ensembles"],"prefix":"10.1007","author":[{"given":"Jacques","family":"Combaz","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Francesco","family":"Tiezzi","sequence":"additional","affiliation":[]},{"given":"Andrea","family":"Margheri","sequence":"additional","affiliation":[]},{"given":"Rosario","family":"Pugliese","sequence":"additional","affiliation":[]},{"given":"Jan","family":"Kofro\u0148","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"3_CR1","unstructured":"Intelligent robots for improving the quality of life, \n                    \n                      http:\/\/www.nccr-robotics.ch"},{"key":"3_CR2","unstructured":"PPL, \n                    \n                      http:\/\/bugseng.com\/products\/ppl\/"},{"key":"3_CR3","unstructured":"Uppaal, \n                    \n                      http:\/\/www.uppaal.org\/"},{"key":"3_CR4","unstructured":"Z3, \n                    \n                      http:\/\/research.microsoft.com\/en-us\/um\/redmond\/projects\/z3\/"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"172","DOI":"10.1007\/978-3-642-32885-5_13","volume-title":"Business Process Management","author":"R. Accorsi","year":"2012","unstructured":"Accorsi, R., Lehmann, A.: Automatic information flow analysis of business process models. In: Barros, A., Gal, A., Kindler, E. (eds.) BPM 2012. LNCS, vol.\u00a07481, pp. 172\u2013187. Springer, Heidelberg (2012)"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/3-540-48683-6_3","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1999","unstructured":"Alur, R.: Timed automata. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 8\u201322. Springer, Heidelberg (1999)"},{"key":"3_CR7","first-page":"157","volume-title":"RTSS","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L., Halbwachs, N., Wong-Toi, H.: An implementation of three algorithms for timing verification based on automata emptiness. In: RTSS, pp. 157\u2013166 (1992)"},{"issue":"2","key":"3_CR8","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Astefanoaei, L., Rayana, S.B., Bensalem, S., Bozga, M., Combaz, J.: Compositional invariant generation for timed systems. Tech. Rep. TR-2013-5, Verimag Research Report","DOI":"10.1007\/978-3-642-54862-8_18"},{"key":"3_CR10","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking (Representation and Mind Series). MIT Press, Cambridge (2008)"},{"key":"3_CR11","doi-asserted-by":"crossref","unstructured":"Basin, D., Doser, J., Lodderstedt, T.: Model driven security: from uml models to access control infrastructures. ACM Transactions on Software Engineering and Methodology\u00a015 (2006)","DOI":"10.1145\/1125808.1125810"},{"issue":"3","key":"3_CR12","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MS.2011.27","volume":"28","author":"A. Basu","year":"2011","unstructured":"Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.H., Sifakis, J.: Rigorous component-based design using the BIP framework. IEEE Software Special Edition \u2013 Software Components beyond Programming \u2013 from Routines to Services\u00a028(3), 41\u201348 (2011)","journal-title":"IEEE Software"},{"key":"3_CR13","doi-asserted-by":"crossref","DOI":"10.21236\/ADA023588","volume-title":"Secure computer system: Unified exposition and multics interpretation","author":"E.D. Bell","year":"1976","unstructured":"Bell, E.D., La Padula, J.L.: Secure computer system: Unified exposition and multics interpretation (1976)"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.-H.: Compositional verification for component-based systems and application. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"3_CR15","unstructured":"Bensalem, S., Boyer, B., Bozga, M., Legay, A.: Incremental generation of linear invariants for component-based systems. Tech. Rep. TR-2012-15, Verimag Research Report (2012), \n                    \n                      http:\/\/www-verimag.imag.fr\/TR\/TR-2012-15.pdf"},{"key":"3_CR16","volume-title":"FMCAD\u201910","author":"S. Bensalem","year":"2010","unstructured":"Bensalem, S., Bozga, M., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: Incremental component-based construction and verification using invariants. In: FMCAD\u201910 (2010)"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-34026-0_25","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"S. Bensalem","year":"2012","unstructured":"Bensalem, S., Bozga, M., Delahaye, B., Jegourel, C., Legay, A., Nouri, A.: Statistical model checking qoS properties of systems with SBIP. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part I. LNCS, vol.\u00a07609, pp. 327\u2013341. Springer, Heidelberg (2012)"},{"key":"3_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-540-88387-6_7","volume-title":"Automated Technology for Verification and Analysis","author":"S. Bensalem","year":"2008","unstructured":"Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.H.: Compositional verification for component-based systems and application. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 64\u201379. Springer, Heidelberg (2008)"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-642-20398-5_32","volume-title":"NASA Formal Methods","author":"S. Bensalem","year":"2011","unstructured":"Bensalem, S., Griesmayer, A., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: D-finder 2: Towards efficient correctness of incremental design. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 453\u2013458. Springer, Heidelberg (2011)"},{"key":"3_CR20","volume-title":"TASE","author":"S. Bensalem","year":"2010","unstructured":"Bensalem, S., Legay, A., Nguyen, T.H., Sifakis, J., Yan, R.: Incremental invariant generation for compositional design. In: TASE (2010)"},{"key":"3_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"614","DOI":"10.1007\/978-3-642-02658-4_45","volume-title":"Computer Aided Verification","author":"S. Bensalem","year":"2009","unstructured":"Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: A tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 614\u2013619. Springer, Heidelberg (2009)"},{"key":"3_CR22","first-page":"155","volume-title":"WEBIST","author":"A. Bertolino","year":"2012","unstructured":"Bertolino, A., Daoudagh, S., Lonetti, F., Marchetti, E.: The X-CREATE Framework - A Comparison of XACML Policy Testing Strategies. In: WEBIST, pp. 155\u2013160. SciTePress (2012)"},{"key":"3_CR23","first-page":"5003","volume-title":"American Control Conference (ACC)","author":"L.F. Bertuccelli","year":"2008","unstructured":"Bertuccelli, L.F., How, J.P.: Robust Markov decision processes using sigma point sampling. In: American Control Conference (ACC), 11-13 June 2008, pp. 5003\u20135008 (2008)"},{"key":"3_CR24","unstructured":"BIP \u2013 incremental component-based construction of real-time systems, \n                    \n                      www.bip-components.com"},{"issue":"2","key":"3_CR25","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/s10617-012-9091-0","volume":"17","author":"B. Bonakdarpour","year":"2013","unstructured":"Bonakdarpour, B., Bozga, M., Quilbeuf, J.: Model-based implementation of distributed systems with priorities. Design Autom. for Emb. Sys.\u00a017(2), 251\u2013276 (2013), doi:10.1007\/s10617-012-9091-0","journal-title":"Design Autom. for Emb. Sys."},{"key":"3_CR26","doi-asserted-by":"publisher","first-page":"4187","DOI":"10.1109\/IROS.2010.5649153","volume-title":"International Conference on Intelligent Robots and Systems (IROS), 2010 IEEE\/RSJ","author":"M. Bonani","year":"2010","unstructured":"Bonani, M., Longchamp, V., Magnenat, S., R\\\u2019etornaz, P., Burnier, D., Roulet, G., Vaussard, F., Bleuler, H., Mondada, F.: The MarXbot, a Miniature Mobile Robot Opening new Perspectives for the Collective-robotic Research. In: International Conference on Intelligent Robots and Systems (IROS), 2010 IEEE\/RSJ, pp. 4187\u20134193. IEEE Press, Los Alamitos (2010), \n                    \n                      http:\/\/mobots.epfl.ch\/"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-30564-1_1","volume-title":"Software Composition","author":"M. Bozga","year":"2012","unstructured":"Bozga, M., Jaber, M., Maris, N., Sifakis, J.: Modeling dynamic architectures using dy-bip. In: Gschwind, T., De Paoli, F., Gruhn, V., Book, M. (eds.) SC 2012. LNCS, vol.\u00a07306, pp. 1\u201316. Springer, Heidelberg (2012)"},{"issue":"4","key":"3_CR28","doi-asserted-by":"publisher","first-page":"708","DOI":"10.1109\/TII.2010.2069102","volume":"6","author":"M. Bozga","year":"2010","unstructured":"Bozga, M., Jaber, M., Sifakis, J.: Source-to-source architecture transformation for performance optimization in BIP. IEEE Trans. Industrial Informatics\u00a06(4), 708\u2013718 (2010), doi:10.1109\/TII.2010.2069102","journal-title":"IEEE Trans. Industrial Informatics"},{"key":"3_CR29","volume-title":"ASCENS Deliverable D1.5","author":"T. Bures","year":"2012","unstructured":"Bures, T., Gerostathopoulos, I., Horky, V., Keznikl, J., Kofron, J., Loreti, M., Plasil, F.: Language Extensions for Implementation-Level Conformance Checking. In: ASCENS Deliverable D1.5 (2012)"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35746-6_1","volume-title":"Tools for Practical Software Verification","author":"E.M. Clarke","year":"2012","unstructured":"Clarke, E.M., Klieber, W., Nov\u00e1\u010dek, M., Zuliani, P.: Model checking and the state explosion problem. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol.\u00a07682, pp. 1\u201330. Springer, Heidelberg (2012), doi:10.1007\/978-3-642-35746-6_1"},{"key":"3_CR31","volume-title":"Model checking","author":"E. Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., M\u00f8ller, M.H., Nyman, U., Ravn, A.P., Skou, A., Wasowski, A.: Compositional verification of real-time systems using Ecdar. STTT (2012)","DOI":"10.1007\/s10009-012-0237-y"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/978-3-319-16310-9_1","volume-title":"Software Engineering for Collective Autonomic Systems","author":"R. Nicola De","year":"2015","unstructured":"De Nicola, R., Latella, D., Lafuente, A.L., Loreti, M., Margheri, A., Massink, M., Morichetta, A., Pugliese, R., Tiezzi, F., Vandin, A.: The SCEL Language: Design, Implementation, Verification. In: Wirsing, M., H\u00f6lzl, M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems. LNCS, vol.\u00a08998, pp. 3\u201371. Springer, Heidelberg (2015)"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM pp. 504\u2013513 (1977)","DOI":"10.1145\/359636.359712"},{"key":"3_CR35","unstructured":"FACPL Website (2013), \n                    \n                      http:\/\/rap.dsi.unifi.it\/facpl\/"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1007\/978-3-540-24631-2_4","volume-title":"Foundations of Security Analysis and Design II","author":"R. Focardi","year":"2004","unstructured":"Focardi, R., Gorrieri, R., Martinelli, F.: Classification of security properties. In: Focardi, R., Gorrieri, R. (eds.) FOSAD 2001. LNCS, vol.\u00a02946, pp. 139\u2013185. Springer, Heidelberg (2004)"},{"key":"3_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"V. Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 317\u2013332. Springer, Heidelberg (2012)"},{"key":"3_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1007\/978-3-642-01465-9_14","volume-title":"Formal Aspects in Security and Trust","author":"S. Frau","year":"2009","unstructured":"Frau, S., Gorrieri, R., Ferigato, C.: Petri net security checker: Structural non-interference at work. In: Degano, P., Guttman, J.D., Martinelli, F. (eds.) FAST 2008. LNCS, vol.\u00a05491, pp. 210\u2013225. Springer, Heidelberg (2009)"},{"key":"3_CR39","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/SP.1982.10014","volume-title":"Proceedings of 1982 Symposium on Security and Privecy","author":"J.A. Goguen","year":"1982","unstructured":"Goguen, J.A., Meseguer, J.: Security policy and security models. In: Proceedings of 1982 Symposium on Security and Privecy, pp. 11\u201320. IEEE Computer Society Press, Los Alamitos (1982)"},{"issue":"2","key":"3_CR40","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1006\/inco.1994.1045","volume":"111","author":"T.A. Henzinger","year":"1994","unstructured":"Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput.\u00a0111(2), 193\u2013244 (1994), doi:10.1006\/inco.1994.1045","journal-title":"Inf. Comput."},{"key":"3_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/11734666_15","volume-title":"Security in Pervasive Computing","author":"D. Hutter","year":"2006","unstructured":"Hutter, D., Volkamer, M.: Information flow control to secure dynamic web service composition. In: Clark, J.A., Paige, R.F., Polack, F.A.C., Brooke, P.J. (eds.) SPC 2006. LNCS, vol.\u00a03934, pp. 196\u2013210. Springer, Heidelberg (2006)"},{"key":"3_CR42","unstructured":"Jones, C.B.: Specification and design of (parallel) programs. pp. 321\u2013332 (1983)"},{"key":"3_CR43","unstructured":"Java PathFinder, \n                    \n                      http:\/\/babelfish.arc.nasa.gov\/trac\/jpf\/"},{"key":"3_CR44","unstructured":"JPF-LTL: An extension to JPF for checking LTL, \n                    \n                      https:\/\/bitbucket.org\/michelelombardi\/jpf-ltl"},{"key":"3_CR45","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/286884.286890","volume-title":"Proceedings of the ACM Workshop on Role Based Access Control","author":"D.R. Kuhn","year":"1998","unstructured":"Kuhn, D.R.: Role based access control on mls systems without kernel changes. In: Proceedings of the ACM Workshop on Role Based Access Control, pp. 25\u201332 (1998)"},{"key":"3_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"3_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-642-34281-3_17","volume-title":"Formal Methods and Software Engineering","author":"S.-W. Lin","year":"2012","unstructured":"Lin, S.-W., Liu, Y., Hsiung, P.-A., Sun, J., Dong, J.S.: Automatic generation of provably correct embedded systems. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol.\u00a07635, pp. 214\u2013229. Springer, Heidelberg (2012)"},{"key":"3_CR48","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1109\/CSFW.2000.856936","volume-title":"Proceedings of the 13th IEEE workshop on Computer Security Foundations (CSFW \u201900)","author":"H. Mantel","year":"2000","unstructured":"Mantel, H.: Possibilistic definitions of security - an assembly kit. In: Proceedings of the 13th IEEE workshop on Computer Security Foundations (CSFW \u201900), p. 185. IEEE Computer Society Press, Los Alamitos (2000)"},{"key":"3_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/978-3-319-08260-8_6","volume-title":"Web Services and Formal Methods","author":"A. Margheri","year":"2014","unstructured":"Margheri, A., Masi, M., Pugliese, R., Tiezzi, F.: Developing and enforcing policies for access control, resource usage, and adaptation. In: Tuosto, E., Chun, O. (eds.) WS-FM 2013. LNCS, vol.\u00a08379, pp. 85\u2013105. Springer, Heidelberg (2014)"},{"key":"3_CR50","first-page":"404","volume-title":"UIC\/ATC","author":"A. Margheri","year":"2013","unstructured":"Margheri, A., Pugliese, R., Tiezzi, F.: Linguistic Abstractions for Programming and Policing Autonomic Computing Systems. In: UIC\/ATC, pp. 404\u2013409. IEEE Computer Society Press, Los Alamitos (2013)"},{"key":"3_CR51","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1109\/SECPRI.1988.8110","volume-title":"Proceedings of the 1988 IEEE conference on Security and privacy (SP\u201988)","author":"D. McCullough","year":"1988","unstructured":"McCullough, D.: Noninterference and the composability of security properties. In: Proceedings of the 1988 IEEE conference on Security and privacy (SP\u201988), pp. 177\u2013186. IEEE Computer Society Press, Los Alamitos (1988)"},{"key":"3_CR52","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1109\/RISP.1994.296590","volume-title":"Proceedings of the 1994 IEEE Symposium on Security and Privacy (SP \u201994)","author":"J. McLean","year":"1994","unstructured":"McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the 1994 IEEE Symposium on Security and Privacy (SP \u201994), p. 79. IEEE Computer Society Press, Los Alamitos (1994)"},{"issue":"4","key":"3_CR53","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1109\/TSE.1981.230844","volume":"7","author":"J. Misra","year":"1981","unstructured":"Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Transactions on Software Engineering\u00a07(4), 417\u2013426 (1981)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"3_CR54","unstructured":"OASIS XACML TC: eXtensible Access Control Markup Language (XACML) version 3.0 - Candidate OASIS Standard (September 2012)"},{"key":"3_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"471","DOI":"10.1007\/978-3-319-16310-9_15","volume-title":"Software Engineering for Collective Autonomic Systems","author":"C. Pinciroli","year":"2015","unstructured":"Pinciroli, C., Bonani, M., Mondada, F., Dorigo, M.: Adaptation and Awareness in Robot Ensembles: Scenarios and Algorithms. In: Wirsing, M., H\u00f6lzl, M., Koch, N., Mayer, P. (eds.) Software Engineering for Collective Autonomic Systems. LNCS, vol.\u00a08998, pp. 471\u2013494. Springer, Heidelberg (2015)"},{"issue":"4","key":"3_CR56","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s11721-012-0072-5","volume":"6","author":"C. Pinciroli","year":"2012","unstructured":"Pinciroli, C., Trianni, V., O\u2019Grady, R., Pini, G., Brutschy, A., Brambilla, M., Mathews, N., Ferrante, E., Caro, G.D., Ducatelle, F., Birattari, M., Gambardella, L.M., Dorigo, M.: Argos: a modular, parallel, multi-engine simulator for multi-robot systems. Swarm Intelligence\u00a06(4), 271\u2013295 (2012)","journal-title":"Swarm Intelligence"},{"key":"3_CR57","first-page":"123","volume-title":"Logics and Models of Concurrent Systems","author":"A. Pnueli","year":"1984","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K. (ed.) Logics and Models of Concurrent Systems, pp. 123\u2013144. Springer, New York (1984)"},{"key":"3_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"3_CR59","unstructured":"Rushby, J.: Noninterference, transitivity, and channel-control security policies. Tech. rep. (December 1992), \n                    \n                      http:\/\/www.csl.sri.com\/papers\/csl-92-2\/"},{"key":"3_CR60","doi-asserted-by":"crossref","unstructured":"Sabelfeld, A., Myers, A.C.: Language-based information-flow security. IEEE Journal on selected areas in communications\u00a021(1) (2003)","DOI":"10.1109\/JSAC.2002.806121"},{"issue":"1","key":"3_CR61","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1023\/A:1011553200337","volume":"14","author":"A. Sabelfeld","year":"2001","unstructured":"Sabelfeld, A., Sands, D.: A per model of secure information flow in sequential programs. Higher Order Symbol. Comput.\u00a014(1), 59\u201391 (2001)","journal-title":"Higher Order Symbol. Comput."},{"key":"3_CR62","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1145\/286884.286893","volume-title":"RBAC \u201998 Proceedings of the third ACM workshop on Role-based access control","author":"R. Sandhu","year":"1998","unstructured":"Sandhu, R., Munawer, Q.: How to do discretionary access control using roles. In: RBAC \u201998 Proceedings of the third ACM workshop on Role-based access control, pp. 47\u201354. ACM Press, New York (1998)"},{"key":"3_CR63","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/11596981_56","volume-title":"Computational Intelligence and Security","author":"J.-j. Shen","year":"2005","unstructured":"Shen, J.-j., Qing, S., Shen, Q., Li, L.: Covert channel identification founded on information flow analysis. In: Hao, Y., Liu, J., Wang, Y.-P., Cheung, Y.-m., Yin, H., Jiao, L., Ma, J., Jiao, Y.-C. (eds.) CIS 2005. LNCS (LNAI), vol.\u00a03802, pp. 381\u2013387. Springer, Heidelberg (2005)"},{"key":"3_CR64","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1145\/268946.268975","volume-title":"Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL \u201998)","author":"G. Smith","year":"1998","unstructured":"Smith, G., Volpano, D.: Secure information flow in a multi-threaded imperative language. In: Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL \u201998), pp. 355\u2013364. ACM Press, New York (1998)"},{"issue":"9","key":"3_CR65","doi-asserted-by":"publisher","first-page":"1382","DOI":"10.1109\/JPROC.2004.832969","volume":"92","author":"D.C. Verma","year":"2004","unstructured":"Verma, D.C.: Service level agreements on IP networks. Proceedings of the IEEE\u00a092(9), 1382\u20131388 (2004)","journal-title":"Proceedings of the IEEE"},{"key":"3_CR66","first-page":"243","volume-title":"FORTE","author":"W. Yi","year":"1994","unstructured":"Yi, W., Pettersson, P., Daniels, M.: Automatic verification of real-time communicating systems by constraint-solving. In: FORTE, pp. 243\u2013258 (1994)"},{"key":"3_CR67","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/SECPRI.1997.601322","volume-title":"Proceedings of the 1997 IEEE Symposium on Security and Privacy (SP \u201997)","author":"A. Zakinthinos","year":"1997","unstructured":"Zakinthinos, A., Lee, E.S.: A general theory of security properties. In: Proceedings of the 1997 IEEE Symposium on Security and Privacy (SP \u201997), p. 94. IEEE Computer Society Press, Los Alamitos (1997)"}],"container-title":["Lecture Notes in Computer Science","Software Engineering for Collective Autonomic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-16310-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T12:27:35Z","timestamp":1559132855000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-16310-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319163093","9783319163109"],"references-count":67,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-16310-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}