{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,24]],"date-time":"2025-10-24T08:02:28Z","timestamp":1761292948345},"publisher-location":"Berlin, Heidelberg","reference-count":34,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642334269"},{"type":"electronic","value":"9783642334276"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-33427-6_7","type":"book-chapter","created":{"date-parts":[[2012,8,23]],"date-time":"2012-08-23T09:38:39Z","timestamp":1345714719000},"page":"91-106","source":"Crossref","is-referenced-by-count":12,"title":["Formal Modeling of Resource Management for Cloud Architectures: An Industrial Case Study"],"prefix":"10.1007","author":[{"given":"Frank S.","family":"de Boer","sequence":"first","affiliation":[]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[]},{"given":"Einar Broch","family":"Johnsen","sequence":"additional","affiliation":[]},{"given":"Rudolf","family":"Schlatte","sequence":"additional","affiliation":[]},{"given":"Peter Y. H.","family":"Wong","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Agha, G.A.: ACTORS: A Model of Concurrent Computations in Distributed Systems. MIT Press (1986)","DOI":"10.7551\/mitpress\/1086.001.0001"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Albert, E., Arenas, P., Genaim, S., G\u00f3mez-Zamalloa, M., Puebla, G.: COSTABS: a cost and termination analyzer for ABS. In: Proc. Partial Evaluation and Program Manipulation (PEPM 2012), pp. 151\u2013154. ACM (2012)","DOI":"10.1145\/2103746.2103774"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-540-40903-8_6","volume-title":"Formal Modeling and Analysis of Timed Systems","author":"T. Amnell","year":"2004","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES: A Tool for Schedulability Analysis and Code Generation of Real-time Systems. In: Larsen, K.G., Niebert, P. (eds.) FORMATS 2003. LNCS, vol.\u00a02791, pp. 60\u201372. Springer, Heidelberg (2004)"},{"key":"7_CR4","unstructured":"Armstrong, J.: Programming Erlang. Pragmatic Bookshelf (2007)"},{"key":"7_CR5","doi-asserted-by":"crossref","unstructured":"Bai, X., Li, M., Chen, B., Tsai, W.-T., Gao, J.: Cloud testing tools. In: Proc. Service Oriented System Engineering (SOSE 2011), pp. 1\u201312. IEEE (2011)","DOI":"10.1109\/SOSE.2011.6139087"},{"issue":"9","key":"7_CR6","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C. Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Comm. ACM\u00a053(9), 76\u201385 (2010)","journal-title":"Comm. ACM"},{"issue":"1-2","key":"7_CR7","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.tcs.2006.11.017","volume":"373","author":"F. Barbanera","year":"2007","unstructured":"Barbanera, F., Bugliesi, M., Dezani-Ciancaglini, M., Sassone, V.: Space-aware ambients and processes. TCS\u00a0373(1-2), 41\u201369 (2007)","journal-title":"TCS"},{"key":"7_CR8","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rk, J., de Boer, F.S., Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: User-defined schedulers for real-time concurrent objects. Innovations in Systems and Software Engineering (to appear, available online, 2012)","DOI":"10.1007\/s11334-012-0184-5"},{"issue":"10","key":"7_CR9","doi-asserted-by":"publisher","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H.C. Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H.C., D\u2019Argenio, P.R., Hermanns, H., Katoen, J.-P.: MODEST: A Compositional Modeling Formalism for Hard and Softly Timed Systems. IEEE Trans. Software Eng.\u00a032(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Software Eng."},{"issue":"9","key":"7_CR10","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/1995376.1995396","volume":"54","author":"P. Bouyer","year":"2011","unstructured":"Bouyer, P., Fahrenberg, U., Larsen, K.G., Markey, N.: Quantitative analysis of real-time systems using priced timed automata. Comm. ACM\u00a054(9), 78\u201387 (2011)","journal-title":"Comm. ACM"},{"key":"7_CR11","unstructured":"Bruno, E.J., Bollella, G.: Real-Time Java Programming: With Java RTS. Prentice Hall (2009)"},{"issue":"6","key":"7_CR12","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1016\/j.future.2008.12.001","volume":"25","author":"R. Buyya","year":"2009","unstructured":"Buyya, R., Yeo, C.S., Venugopal, S., Broberg, J., Brandic, I.: Cloud computing and emerging IT platforms: Vision, hype, and reality for delivering computing as the 5th utility. Future Generation Computer Systems\u00a025(6), 599\u2013616 (2009)","journal-title":"Future Generation Computer Systems"},{"key":"7_CR13","unstructured":"Calheiros, R.N., Netto, M.A., Rose, C.A.F.D., Buyya, R.: EMUSIM: an integrated emulation and simulation environment for modeling, evaluation, and validation of performance of cloud computing applications. Software: Practice and Experience (to appear, available online, 2012)"},{"issue":"1","key":"7_CR14","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1002\/spe.995","volume":"41","author":"R.N. Calheiros","year":"2011","unstructured":"Calheiros, R.N., Ranjan, R., Beloglazov, A., Rose, C.A.F.D., Buyya, R.: CloudSim: a toolkit for modeling and simulation of cloud computing environments and evaluation of resource provisioning algorithms. Software, Practice and Experience\u00a041(1), 23\u201350 (2011)","journal-title":"Software, Practice and Experience"},{"key":"7_CR15","unstructured":"Caromel, D., Henrio, L.: A Theory of Distributed Objects. Springer (2005)"},{"key":"7_CR16","doi-asserted-by":"crossref","unstructured":"Chander, A., Espinosa, D., Islam, N., Lee, P., Necula, G.C.: Enforcing resource bounds via static verification of dynamic checks. ACM TOPLAS\u00a029(5) (2007)","DOI":"10.1145\/1275497.1275503"},{"key":"7_CR17","unstructured":"Douglass, B.P.: Real Time UML \u2013 Advances in the UML for Real-Time Systems. Addison-Wesley (2004)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Foster, H., Emmerich, W., Kramer, J., Magee, J., Rosenblum, D.S., Uchitel, S.: Model checking service compositions under resource constraints. In: Proc. European Software Engineering Conf. and Intl. Symp. on Foundations of Software Engineering (ESEC\/FSE 2007), pp. 225\u2013234. ACM (2007)","DOI":"10.1145\/1287624.1287657"},{"key":"7_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","volume-title":"Formal Methods for Components and Objects","author":"E.B. Johnsen","year":"2011","unstructured":"Johnsen, E.B., H\u00e4hnle, R., Sch\u00e4fer, J., Schlatte, R., Steffen, M.: ABS: A Core Language for Abstract Behavioral Specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2011. LNCS, vol.\u00a06957, pp. 142\u2013164. Springer, Heidelberg (2011)"},{"issue":"1","key":"7_CR20","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/s10270-006-0011-2","volume":"6","author":"E.B. Johnsen","year":"2007","unstructured":"Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling\u00a06(1), 35\u201358 (2007)","journal-title":"Software and Systems Modeling"},{"key":"7_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-642-16901-4_42","volume-title":"Formal Methods and Software Engineering","author":"E.B. Johnsen","year":"2010","unstructured":"Johnsen, E.B., Owe, O., Schlatte, R., Tapia Tarifa, S.L.: Dynamic Resource Reallocation between Deployment Components. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol.\u00a06447, pp. 646\u2013661. Springer, Heidelberg (2010)"},{"key":"7_CR22","series-title":"LNCS","volume-title":"Proc. Formal Engineering Methods (ICFEM 2012)","author":"E.B. Johnsen","year":"2012","unstructured":"Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Modeling Resource-Aware Virtualized Applications for the Cloud in Real-Time ABS. In: Proc. Formal Engineering Methods (ICFEM 2012). LNCS. Springer, Heidelberg (to appear, 2012)"},{"key":"7_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-18070-5_4","volume-title":"Formal Verification of Object-Oriented Software","author":"E.B. Johnsen","year":"2011","unstructured":"Johnsen, E.B., Owe, O., Schlatte, R., Tapia Tarifa, S.L.: Validating Timed Models of Deployment Components with Parametric Concurrency. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol.\u00a06528, pp. 46\u201360. Springer, Heidelberg (2011)"},{"issue":"4","key":"7_CR24","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1232743.1232745","volume":"50","author":"J. Kramer","year":"2007","unstructured":"Kramer, J.: Is abstraction the key to computing? Comm. ACM\u00a050(4), 36\u201342 (2007)","journal-title":"Comm. ACM"},{"issue":"1-2","key":"7_CR25","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Intl. Journal on Software Tools for Technology Transfer\u00a01(1-2), 134\u2013152 (1997)","journal-title":"Intl. Journal on Software Tools for Technology Transfer"},{"issue":"5","key":"7_CR26","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1145\/1506409.1506426","volume":"52","author":"E.A. Lee","year":"2009","unstructured":"Lee, E.A.: Computing needs time. Comm. ACM\u00a052(5), 70\u201379 (2009)","journal-title":"Comm. ACM"},{"issue":"3","key":"7_CR27","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1145\/1065887.1065891","volume":"27","author":"L. Moreau","year":"2005","unstructured":"Moreau, L., Queinnec, C.: Resource aware programming. ACM TOPLAS\u00a027(3), 441\u2013476 (2005)","journal-title":"ACM TOPLAS"},{"key":"7_CR28","unstructured":"Netjes, M., van der Aalst, W.M., Reijers, H.A.: Analysis of resource-constrained processes with Colored Petri Nets. In: Proc. Practical Use of Coloured Petri Nets and CPN Tools (CPN 2005), DAIMI 576. University of Aarhus (2005)"},{"key":"7_CR29","doi-asserted-by":"publisher","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.: iCanCloud: A flexible and scalable cloud infrastructure simulator. Journal of Grid Computing\u00a010, 185\u2013209 (2012), doi:10.1007\/s10723-012-9208-5","journal-title":"Journal of Grid Computing"},{"issue":"2","key":"7_CR30","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/s10270-006-0026-8","volume":"6","author":"D.B. Petriu","year":"2007","unstructured":"Petriu, D.B., Woodside, C.M.: An intermediate metamodel with scenarios and resources for generating performance models from UML designs. Software and System Modeling\u00a06(2), 163\u2013184 (2007)","journal-title":"Software and System Modeling"},{"key":"7_CR31","doi-asserted-by":"crossref","unstructured":"Sgroi, M., Lavagno, L., Watanabe, Y., Sangiovanni-Vincentelli, A.: Synthesis of embedded software using free-choice Petri nets. In: Proc. Design Automation Conference (DAC 1999), pp. 805\u2013810. ACM (1999)","DOI":"10.1145\/309847.310073"},{"key":"7_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11813040_11","volume-title":"FM 2006: Formal Methods","author":"M. Verhoef","year":"2006","unstructured":"Verhoef, M., Larsen, P.G., Hooman, J.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol.\u00a04085, pp. 147\u2013162. Springer, Heidelberg (2006)"},{"key":"7_CR33","doi-asserted-by":"crossref","unstructured":"Vulgarakis, A., Seceleanu, C.C.: Embedded systems resources: Views on modeling and analysis. In: Proc. Computer Software and Applications Conference (COMPSAC 2008), pp. 1321\u20131328. IEEE (2008)","DOI":"10.1109\/COMPSAC.2008.215"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-642-31762-0_5","volume-title":"Formal Verification of Object-Oriented Software","author":"P.Y.H. Wong","year":"2012","unstructured":"Wong, P.Y.H., Diakov, N., Schaefer, I.: Modelling Adaptable Distributed Object Oriented Systems Using the HATS Approach: A Fredhopper Case Study. In: Beckert, B., Damiani, F., Gurov, D. (eds.) FoVeOOS 2011. LNCS, vol.\u00a07421, pp. 49\u201366. Springer, Heidelberg (2012)"}],"container-title":["Lecture Notes in Computer Science","Service-Oriented and Cloud Computing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-33427-6_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,12]],"date-time":"2020-07-12T21:06:23Z","timestamp":1594587983000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-33427-6_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642334269","9783642334276"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-33427-6_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}