{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,19]],"date-time":"2026-02-19T07:16:13Z","timestamp":1771485373244,"version":"3.50.1"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2013,12,1]],"date-time":"2013-12-01T00:00:00Z","timestamp":1385856000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["SOCA"],"published-print":{"date-parts":[[2014,12]]},"DOI":"10.1007\/s11761-013-0148-0","type":"journal-article","created":{"date-parts":[[2013,11,30]],"date-time":"2013-11-30T07:22:51Z","timestamp":1385796171000},"page":"323-339","source":"Crossref","is-referenced-by-count":50,"title":["Formal modeling and analysis of resource management for cloud architectures: an industrial case study using Real-Time ABS"],"prefix":"10.1007","volume":"8","author":[{"given":"Elvira","family":"Albert","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frank S.","family":"de Boer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rudolf","family":"Schlatte","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S. Lizeth","family":"Tapia Tarifa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter Y. H.","family":"Wong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2013,12,1]]},"reference":[{"key":"148_CR1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/1086.001.0001","volume-title":"ACTORS: a model of concurrent computations in distributed systems","author":"GA Agha","year":"1986","unstructured":"Agha GA (1986) ACTORS: a model of concurrent computations in distributed systems. MIT Press, Cambridge, MA"},{"key":"148_CR2","doi-asserted-by":"crossref","unstructured":"Albert E, Arenas P, Genaim S, G\u00f3mez-Zamalloa M, Puebla G (2011) Cost analysis of concurrent OO programs. In: The 9th Asian symposium on programming languages and systems (APLAS\u201911), LNCS, vol 7078. Springer, Berlin, pp 238\u2013254","DOI":"10.1007\/978-3-642-25318-8_19"},{"key":"148_CR3","doi-asserted-by":"crossref","unstructured":"Albert E, Arenas P, Genaim S, G\u00f3mez-Zamalloa M, Puebla G (2012) COSTABS: a cost and termination analyzer for ABS. In: Kiselyov O, Thompson S (eds) Proceedings of the workshop on partial evaluation and program manipulation (PEPM\u201912). ACM, pp 151\u2013154","DOI":"10.1145\/2103746.2103774"},{"key":"148_CR4","doi-asserted-by":"crossref","unstructured":"Albert E, Arenas P, Genaim S, Puebla G, Zanardini D (2012) Cost analysis of object-oriented bytecode programs. TCS 413(1):142\u2013159","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"148_CR5","doi-asserted-by":"crossref","unstructured":"Albert E, de Boer F, H\u00e4hnle R, Johnsen EB, Laneve C (2013) Engineering virtualized services. In: Babar MA, Dumas M (eds) Proceedings of the 2nd nordic symposium on cloud computing & internet technologies (NordiCloud\u201913). ACM, pp 59\u201363","DOI":"10.1145\/2513534.2513545"},{"key":"148_CR6","doi-asserted-by":"crossref","unstructured":"Albert E, Bubel R, Genaim S, H\u00e4hnle R, Puebla G, Rom\u00e1n-D\u00edez G (2011) Verified resource guarantees using COSTA and KeY. In: ACM SIGPLAN workshop on partial evaluation and semantics-based program manipulation (PEPM\u201911). ACM Press","DOI":"10.1145\/1929501.1929513"},{"key":"148_CR7","doi-asserted-by":"crossref","unstructured":"Albert E, Genaim S, G\u00f3mez-Zamalloa M, Johnsen EB, Schlatte R, Tapia Tarifa SL (2011) Simulating concurrent behaviors with worst-case cost bounds. In: Butler M, Schulte W (eds) FM 2011, LNCS, vol 6664. Springer, Berlin, pp 353\u2013368","DOI":"10.1007\/978-3-642-21437-0_27"},{"key":"148_CR8","doi-asserted-by":"crossref","unstructured":"Albert E, \u00d8stvold BM, Rojas JM (2012) Automated extraction of abstract behavioural models from JMS applications. In: Formal methods for industrial critical systems (FMICS\u201912), LNCS, vol 7437. Springer, Berlin, pp 16\u201331","DOI":"10.1007\/978-3-642-32469-7_2"},{"key":"148_CR9","unstructured":"Amnell T, Fersman E, Mokrushin L, Pettersson P, Yi W (2003) TIMES: a tool for schedulability analysis and code generation of real-time systems. In: Larsen KG, Niebert P (eds) Proceeding of the first international workshop on formal modeling and analysis of timed systems (FORMATS 2003), LNCS, vol 2791. Springer, Berlin, pp 60\u201372"},{"key":"148_CR10","unstructured":"Armstrong J (2007) Programming Erlang: software for a concurrent world. Pragmatic Bookshelf (2007)"},{"key":"148_CR11","doi-asserted-by":"crossref","unstructured":"Bai X, Li M, Chen B, Tsai WT, Gao J (2011) Cloud testing tools. In: Gao JZ, Lu X, Younas M, Zhu H (eds) Proceedings of the 6th international symposium on service oriented system engineering (SOSE\u201911). IEEE, pp 1\u201312","DOI":"10.1109\/SOSE.2011.6139087"},{"issue":"9","key":"148_CR12","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier C, Haverkort BR, Hermanns H, Katoen JP (2010) Performance evaluation and model checking join forces. Commun ACM 53(9):76\u201385","journal-title":"Commun ACM"},{"issue":"1\u20132","key":"148_CR13","first-page":"41","volume":"373","author":"F Barbanera","year":"2007","unstructured":"Barbanera F, Bugliesi M, Dezani-Ciancaglini M, Sassone V (2007) Space-aware ambients and processes. TCS 373(1\u20132):41\u201369","journal-title":"Space-aware ambients and processes. TCS"},{"key":"148_CR14","doi-asserted-by":"crossref","unstructured":"Benoy F, King A (1997) Inferring argument size relationships with CLP(R). In: Proceedings of the LOPSTR\u201997, LNCS, vol 1207. Springer, Berlin, pp 204\u2013223","DOI":"10.1007\/3-540-62718-9_12"},{"key":"148_CR15","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rk J, de Boer FS, Johnsen EB, Schlatte R, Tapia Tarifa SL (2012) User-defined schedulers for real-time concurrent objects. Innov Syst Softw Eng 9(1):29\u201343","DOI":"10.1007\/s11334-012-0184-5"},{"issue":"10","key":"148_CR16","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"HC Bohnenkamp","year":"2006","unstructured":"Bohnenkamp HC, D\u2019Argenio PR, Hermanns H, Katoen JP (2006) MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans Softw Eng 32(10):812\u2013830","journal-title":"IEEE Trans Softw Eng"},{"issue":"9","key":"148_CR17","doi-asserted-by":"crossref","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P Bouyer","year":"2011","unstructured":"Bouyer P, Fahrenberg U, Larsen KG, Markey N (2011) Quantitative analysis of real-time systems using priced timed automata. Commun ACM 54(9):78\u201387","journal-title":"Commun ACM"},{"key":"148_CR18","volume-title":"Real-Time Java Programming: with Java RTS","author":"EJ Bruno","year":"2009","unstructured":"Bruno EJ, Bollella G (2009) Real-Time Java Programming: with Java RTS. Prentice Hall PTR, Englewood Cliffs, NJ"},{"issue":"6","key":"148_CR19","doi-asserted-by":"crossref","first-page":"599","DOI":"10.1016\/j.future.2008.12.001","volume":"25","author":"R Buyya","year":"2009","unstructured":"Buyya R, Yeo CS, Venugopal S, Broberg J, Brandic I (2009) Cloud computing and emerging IT platforms: vision, hype, and reality for delivering computing as the 5th utility. Future Gener Comput Syst 25(6):599\u2013616","journal-title":"Future Gener Comput Syst"},{"key":"148_CR20","doi-asserted-by":"crossref","unstructured":"Calheiros RN, Netto MA, Rose CAD, Buyya R (2012) EMUSIM: an integrated emulation and simulation environment for modeling, evaluation, and validation of performance of cloud computing applications. Softw Pract Exp 43(5):595\u2013612","DOI":"10.1002\/spe.2124"},{"issue":"1","key":"148_CR21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1002\/spe.995","volume":"41","author":"RN Calheiros","year":"2011","unstructured":"Calheiros RN, Ranjan R, Beloglazov A, Rose CAFD, Buyya R (2011) CloudSim: a toolkit for modeling and simulation of cloud computing environments and evaluation of resource provisioning algorithms. Softw Pract Exp 41(1):23\u201350","journal-title":"Softw Pract Exp"},{"key":"148_CR22","volume-title":"A theory of distributed objects","author":"D Caromel","year":"2005","unstructured":"Caromel D, Henrio L (2005) A theory of distributed objects. Springer, Berlin"},{"key":"148_CR23","doi-asserted-by":"crossref","unstructured":"Chander A, Espinosa D, Islam N, Lee P, Necula GC (2007) Enforcing resource bounds via static verification of dynamic checks. ACM ToPLaS 29(5), art no 28","DOI":"10.1145\/1275497.1275503"},{"key":"148_CR24","doi-asserted-by":"crossref","unstructured":"de Boer FS, H\u00e4hnle R, Johnsen EB, Schlatte R, Wong PYH (2012) Formal modeling of resource management for cloud architectures: an industrial case study. In: Paoli FD, Pimentel E, Zavattaro G (eds) Proceedings of the European conference on service-oriented and cloud computing (ESOCC 2012), LNCS, vol 7592. Springer, Berlin, pp 91\u2013106","DOI":"10.1007\/978-3-642-33427-6_7"},{"key":"148_CR25","volume-title":"Real Time UML\u2014advances in the UML for Real-Time systems","author":"BP Douglass","year":"2004","unstructured":"Douglass BP (2004) Real Time UML\u2014advances in the UML for Real-Time systems, 3rd edn. Addison-Wesley, Reading, MA","edition":"3"},{"key":"148_CR26","unstructured":"ESOCC panel discussion (2012) Global management in service-oriented and cloud computing: challenges and open issues. In: European conference on service-oriented and cloud computing (ESSOC)"},{"key":"148_CR27","doi-asserted-by":"crossref","unstructured":"Foster H, Emmerich W, Kramer J, Magee J, Rosenblum DS, Uchitel S (2007) Model checking service compositions under resource constraints. In: Crnkovic I, Bertolino A (eds) Proceeding of the 6th joint meeting of the European software engineering Conference and the ACM SIGSOFT international symposium on foundations of software engineering (ESEC\/FSE\u201907). ACM, pp 225\u2013234","DOI":"10.1145\/1287624.1287657"},{"key":"148_CR28","doi-asserted-by":"crossref","unstructured":"Gulwani S, Mehra KK, Chilimbi TM (2009) Speed: precise and efficient static estimation of program computational complexity. In: POPL. ACM, pp 127\u2013139","DOI":"10.1145\/1594834.1480898"},{"key":"148_CR29","doi-asserted-by":"crossref","unstructured":"Hoffmann J, Hofmann M (2010) Amortized resource analysis with polynomial potential. In: The 19th European symposium on programming (ESOP\u201910), LNCS, vol 6012. Springer, Berlin, pp 287\u2013306","DOI":"10.1007\/978-3-642-11957-6_16"},{"key":"148_CR30","doi-asserted-by":"crossref","unstructured":"Johnsen EB, H\u00e4hnle R, Sch\u00e4fer J, Schlatte R, Steffen M (2011) ABS: a core language for abstract behavioral specification. In: Aichernig B, de Boer FS, Bonsangue MM (eds) Proceeding of the 9th international symposium on formal methods for components and objects (FMCO 2010), LNCS, vol 6957. Springer, Berlin, pp 142\u2013164","DOI":"10.1007\/978-3-642-25271-6_8"},{"issue":"1","key":"148_CR31","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10270-006-0011-2","volume":"6","author":"EB Johnsen","year":"2007","unstructured":"Johnsen EB, Owe O (2007) An asynchronous communication model for distributed concurrent objects. Softw Syst Model 6(1):35\u201358","journal-title":"Softw Syst Model"},{"key":"148_CR32","doi-asserted-by":"crossref","unstructured":"Johnsen EB, Owe O, Schlatte R, Tapia Tarifa SL (2010) Dynamic resource reallocation between deployment components. In: Dong JS, Zhu H (eds) Proceedings of the international conference on formal engineering methods (ICFEM\u201910), LNCS, vol 6447. Springer, Berlin, pp 646\u2013661","DOI":"10.1007\/978-3-642-16901-4_42"},{"key":"148_CR33","unstructured":"Johnsen EB, Owe O, Schlatte R, Tapia Tarifa SL (2011) Validating timed models of deployment components with parametric concurrency. In: Beckert, B March\u00e9 C (eds) Proceedings of the international conference on formal verification of Object-Oriented software (FoVeOOS\u201910), LNCS, vol 6528. Springer, Berlin, pp 46\u201360"},{"key":"148_CR34","doi-asserted-by":"crossref","unstructured":"Johnsen EB, Schlatte R, Tapia Tarifa SL (2012) Modeling resource-aware virtualized applications for the cloud in Real-Time ABS. In: Aoki T, Tagushi K (eds) Proceedings of the 14th international conference on formal engineering methods (ICFEM\u201912), LNCS, vol 7635. Springer, Berlin, pp 71\u201386","DOI":"10.1007\/978-3-642-34281-3_8"},{"key":"148_CR35","doi-asserted-by":"crossref","unstructured":"Kirner R, Puschner PP (2005) Classification of WCET analysis techniques. In: ISORC. IEEE Computer Society, pp 190\u2013199","DOI":"10.1109\/ISORC.2005.19"},{"issue":"4","key":"148_CR36","doi-asserted-by":"crossref","first-page":"36","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J Kramer","year":"2007","unstructured":"Kramer J (2007) Is abstraction the key to computing? Commun ACM 50(4):36\u201342","journal-title":"Commun ACM"},{"issue":"1\u20132","key":"148_CR37","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen KG, Pettersson P, Yi W (1997) UPPAAL in a nutshell. Int J Softw Tools Technol Transf 1(1\u20132):134\u2013152","journal-title":"Int J Softw Tools Technol Transf"},{"issue":"5","key":"148_CR38","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1145\/1506409.1506426","volume":"52","author":"EA Lee","year":"2009","unstructured":"Lee EA (2009) Computing needs time. Commun ACM 52(5):70\u201379","journal-title":"Commun ACM"},{"key":"148_CR39","doi-asserted-by":"crossref","unstructured":"Moreau L, Queinnec C (2005) Resource aware programming. ACM ToPLaS 27(3):441\u2013476","DOI":"10.1145\/1065887.1065891"},{"key":"148_CR40","unstructured":"Netjes M, van der Aalst WM, Reijers HA (2005) Analysis of resource-constrained processes with Colored Petri Nets. In: Jensen K (ed) Proceedings of the sixth workshop on the practical use of coloured petri nets and CPN tools (CPN 2005), DAIMI, vol 576. University of Aarhus"},{"key":"148_CR41","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/s10723-012-9208-5","volume":"10","author":"A Nu\u00f1ez","year":"2012","unstructured":"Nu\u00f1ez A, V\u00e1zquez-Poletti J, Caminero A, Casta\u00f1\u00e9 G, Carretero J, Llorente I (2012) iCanCloud: A flexible and scalable cloud infrastructure simulator. J Grid Comput 10:185\u2013209","journal-title":"J Grid Comput"},{"issue":"2","key":"148_CR42","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/s10270-006-0026-8","volume":"6","author":"DB Petriu","year":"2007","unstructured":"Petriu DB, Woodside CM (2007) An intermediate metamodel with scenarios and resources for generating performance models from UML designs. Softw Syst Model 6(2):163\u2013184","journal-title":"Softw Syst Model"},{"key":"148_CR43","doi-asserted-by":"crossref","unstructured":"Sgroi M, Lavagno L, Watanabe Y, Sangiovanni-Vincentelli A (1999) Synthesis of embedded software using free-choice Petri nets. In: Proceedings of the 36th ACM\/IEEE design automation conference (DAC\u201999). ACM, pp 805\u2013810","DOI":"10.1145\/309847.310073"},{"key":"148_CR44","doi-asserted-by":"crossref","unstructured":"Verhoef M, Larsen PG, Hooman J (2006) Modeling and validating distributed embedded real-time systems with VDM++. In: Misra J, Nipkow T, Sekerinski E (eds) Proceedings of the 14th international symposium on formal methods (FM\u201906), LNCS, vol 4085. Springer, pp 147\u2013162","DOI":"10.1007\/11813040_11"},{"key":"148_CR45","doi-asserted-by":"crossref","unstructured":"Vulgarakis A, Seceleanu CC (2008) Embedded systems resources: views on modeling and analysis. In: Proceeding of the 32nd IEEE international computer software and applications conference (COMPSAC\u201908). IEEE Computer Society, pp 1321\u20131328","DOI":"10.1109\/COMPSAC.2008.215"},{"key":"148_CR46","doi-asserted-by":"crossref","unstructured":"Wilhelm R, Engblom J, Ermedahl A, Holsti N, Thesing S, Whalley DB, Bernat G, Ferdinand C, Heckmann R, Mitra T, Mueller F, Puaut I, Puschner PP, Staschulat J, Stenstr\u00f6m P (2008) The worst-case execution-time problem\u2014overview of methods and survey of tools. ACM Trans Embed Comput Syst 7(3)","DOI":"10.1145\/1347375.1347389"},{"issue":"5","key":"148_CR47","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/s10009-012-0250-1","volume":"14","author":"PYH Wong","year":"2012","unstructured":"Wong PYH, Albert E, Muschevici R, Proen\u00e7a J, Sch\u00e4fer J, Schlatte R (2012) The ABS tool suite: modelling, executing and analysing distributed adaptable object-oriented systems. Int J Softw Tools Technol Transf (STTT) 14(5):567\u2013588","journal-title":"Int J Softw Tools Technol Transf (STTT)"},{"key":"148_CR48","doi-asserted-by":"crossref","unstructured":"Wong PYH, Diakov N, Schaefer I (2012) Modelling distributed adaptable object oriented systems using HATS approach: a fredhopper case study (invited paper). In: 2nd international conference on formal verification of object-oriented software, LNCS, vol 7421. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-31762-0_5"}],"container-title":["Service Oriented Computing and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-013-0148-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11761-013-0148-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11761-013-0148-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,8,11]],"date-time":"2020-08-11T02:46:05Z","timestamp":1597113965000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11761-013-0148-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,12,1]]},"references-count":48,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,12]]}},"alternative-id":["148"],"URL":"https:\/\/doi.org\/10.1007\/s11761-013-0148-0","relation":{},"ISSN":["1863-2386","1863-2394"],"issn-type":[{"value":"1863-2386","type":"print"},{"value":"1863-2394","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,12,1]]}}}