×

Integrating deployment architectures and resource consumption in timed object-oriented models. (English) Zbl 1304.68029

Summary: Software today is often developed for many deployment scenarios; the software may be adapted to sequential, concurrent, distributed, and even virtualized architectures. Since software performance can vary significantly depending on the target architecture, design decisions need to address which features to include and what performance to expect for different architectures. To make use of formal methods for these design decisions, system models need to range over deployment scenarios. For this purpose, it is desirable to lift aspects of low-level deployment to the abstraction level of the modeling language. This paper proposes an integration of deployment architectures in the Real-Time ABS language, with restrictions on processing resources. Real-Time ABS is a timed, abstract and behavioral specification language with a formal semantics and a Java-like syntax, that targets concurrent, distributed and object-oriented systems. A separation of concerns between execution cost at the object level and execution capacity at the deployment level makes it easy to compare the timing and performance of different deployment scenarios already during modeling. The language and associated simulation tool is demonstrated on examples and its semantics is formalized.

MSC:

68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Pohl, K.; Böckle, G.; Van Der Linden, F., Software product line engineering: foundations, principles, and techniques, (2005), Springer · Zbl 1075.68575
[2] Yacoub, S. M., Performance analysis of component-based applications, (Chastek, G. J., Proc. Second International Conference on Software Product Lines (SPLC’02), Lecture Notes in Computer Science, vol. 2379, (2002), Springer), 299-315 · Zbl 1045.68551
[3] Johnsen, E. B.; Hähnle, R.; Schäfer, J.; Schlatte, R.; Steffen, M., ABS: a core language for abstract behavioral specification, (Aichernig, B.; de Boer, F. S.; Bonsangue, M. M., Proc. 9th International Symposium on Formal Methods for Components and Objects (FMCO 2010), Lecture Notes in Computer Science, vol. 6957, (2011), Springer), 142-164
[4] Caromel, D.; Henrio, L., A theory of distributed object, (2005), Springer
[5] Johnsen, E. B.; Owe, O., An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 35-58, (2007)
[6] de Boer, F. S.; Clarke, D.; Johnsen, E. B., A complete guide to the future, (de Nicola, R., Proc. 16th European Symposium on Programming (ESOP’07), Lecture Notes in Computer Science, vol. 4421, (2007), Springer), 316-330
[7] Agha, G. A., ACTORS: A model of concurrent computations in distributed systems, (1986), The MIT Press Cambridge, Mass
[8] Haller, P.; Odersky, M., Scala actors: unifying thread-based and event-based programming, Theor. Comput. Sci., 410, 2-3, 202-220, (2009) · Zbl 1162.68396
[9] Armstrong, J., Programming Erlang: software for a concurrent world, (2007), Pragmatic Bookshelf
[10] Plotkin, G. D., A structural approach to operational semantics, J. Log. Algebr. Program., 60-61, 17-139, (2004) · Zbl 1082.68062
[11] Clarke, D.; Diakov, N.; Hähnle, R.; Johnsen, E. B.; Schaefer, I.; Schäfer, J.; Schlatte, R.; Wong, P. Y.H., Modeling spatial and temporal variability with the HATS abstract behavioral modeling language, (Bernardo, M.; Issarny, V., Proc. 11th Intl. School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM 2011), Lecture Notes in Computer Science, vol. 6659, (2011), Springer), 417-457
[12] (Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., All About Maude - A High-Performance Logical Framework, How to Specify, Program and Verify Systems in Rewriting Logic, Lecture Notes in Computer Science, vol. 4350, (2007), Springer) · Zbl 1115.68046
[13] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 73-155, (1992) · Zbl 0758.68043
[14] Johnsen, E. B.; Owe, O.; Schlatte, R.; Tapia Tarifa, S. L., Validating timed models of deployment components with parametric concurrency, (Beckert, B.; Marché, C., Proc. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS’10), Lecture Notes in Computer Science, vol. 6528, (2011), Springer), 46-60 · Zbl 1308.68037
[15] Johnsen, E. B.; Owe, O.; Schlatte, R.; Tapia Tarifa, S. L., Dynamic resource reallocation between deployment components, (Dong, J. S.; Zhu, H., Proc. International Conference on Formal Engineering Methods (ICFEM’10), Lecture Notes in Computer Science, vol. 6447, (2010), Springer), 646-661
[16] Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L., A formal model of object mobility in resource-restricted deployment scenarios, (Arbab, F.; Ölveczky, P., Proc. 8th International Symposium on Formal Aspects of Component Software (FACS 2011), Lecture Notes in Computer Science, vol. 7253, (2012), Springer), 185-202
[17] Bjørk, J.; de Boer, F. S.; Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L., User-defined schedulers for real-time concurrent objects, Innov. Syst. Softw. Eng., 9, 1, 29-43, (2013)
[18] Pierce, B. C., Types and programming languages, (2002), The MIT Press
[19] Larsen, K. G.; Pettersson, P.; Yi, W., UPPAAL in a nutshell, Int. J. Softw. Tools Technol. Transf., 1, 1-2, 134-152, (1997) · Zbl 1060.68577
[20] Albert, E.; Arenas, P.; Genaim, S.; Gómez-Zamalloa, M.; Puebla, G., COSTABS: a cost and termination analyzer for ABS, (Kiselyov, O.; Thompson, S., Proc. Workshop on Partial Evaluation and Program Manipulation (PEPM’12), (2012), ACM), 151-154
[21] Ölveczky, P. C.; Meseguer, J., Semantics and pragmatics of real-time maude, High.-Order Symb. Comput., 20, 1-2, 161-196, (2007) · Zbl 1115.68095
[22] Schäfer, J.; Poetzsch-Heffter, A., Jcobox: generalizing active objects to concurrent components, (European Conference on Object-Oriented Programming (ECOOP 2010), Lecture Notes in Computer Science, vol. 6183, (2010), Springer), 275-299
[23] Welc, A.; Jagannathan, S.; Hosking, A., Safe futures for Java, (Proc. Object Oriented Programming, Systems, Languages, and Applications (OOPSLA’05), (2005), ACM Press New York, NY, USA), 439-453
[24] Ahrendt, W.; Dylla, M., A system for compositional verification of asynchronous objects, Sci. Comput. Program., 77, 12, 1289-1309, (2012) · Zbl 1264.68050
[25] Albert, E.; Genaim, S.; Gómez-Zamalloa, M.; Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L., Simulating concurrent behaviors with worst-case cost bounds, (Butler, M.; Schulte, W., FM 2011, Lecture Notes in Computer Science, vol. 6664, (2011), Springer), 353-368
[26] Schlatte, R.; Johnsen, E. B.; Kazemeyni, F.; Tapia Tarifa, S. L., Models of rate restricted communication for concurrent objects, Electron. Notes Theor. Comput. Sci., 274, 67-81, (2011)
[27] Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L., A formal model of user-defined resources in resource-restricted deployment scenarios, (Beckert, B.; Damiani, F.; Gurov, D., Proc. International Conference on Formal Verification of Object-Oriented Software (FoVeOOS’11), Lecture Notes in Computer Science, vol. 7421, (2012), Springer), 196-213
[28] Albert, E.; de Boer, F.; Hähnle, R.; Johnsen, E. B.; Laneve, C., Engineering virtualized services, (Babar, M. A.; Dumas, M., 2nd Nordic Symposium on Cloud Computing & Internet Technologies (NordiCloud’13), (2013), ACM), 59-63
[29] Igarashi, A.; Kobayashi, N., Resource usage analysis, ACM Trans. Program. Lang. Syst., 27, 2, 264-313, (2005)
[30] Hennessy, M., A distributed pi-calculus, (2007), Cambridge University Press · Zbl 1125.68082
[31] Nicola, R. D.; Ferrari, G. L.; Montanari, U.; Pugliese, R.; Tuosto, E., A process calculus for QoS-aware applications, (Jacquet, J.-M.; Picco, G. P., Proc. 7th International Conference on Coordination Models and Languages (COORDINATION’05), Lecture Notes in Computer Science, vol. 3454, (2005), Springer), 33-48
[32] Barbanera, F.; Bugliesi, M.; Dezani-Ciancaglini, M.; Sassone, V., Space-aware ambients and processes, Theor. Comput. Sci., 373, 1-2, 41-69, (2007) · Zbl 1111.68011
[33] Lüttgen, G.; Vogler, W., Bisimulation on speed: a unified approach, Theor. Comput. Sci., 360, 1-3, 209-227, (2006) · Zbl 1097.68097
[34] Jain, R., The art of computer systems performance analysis, (1991), John Wiley & Sons, Inc.
[35] Bai, X.; Li, M.; Chen, B.; Tsai, W.-T.; Gao, J., Cloud testing tools, (Gao, J. Z.; Lu, X.; Younas, M.; Zhu, H., Proc. 6th Intl. Symposium on Service Oriented System Engineering (SOSE’11), (2011), IEEE), 1-12
[36] 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, Softw. Pract. Exp., 41, 1, 23-50, (2011)
[37] Nuñez, A.; Vázquez-Poletti, J.; Caminero, A.; Castañé, G.; Carretero, J.; Llorente, I., Icancloud: a flexible and scalable cloud infrastructure simulator, J. Grid Comput., 10, 185-209, (2012)
[38] Buyya, R.; Murshed, M., Gridsim: a toolkit for the modeling and simulation of distributed resource management and scheduling for grid computing, Concurr. Comput., Pract. Exp., 14, 1175-1220, (2002) · Zbl 1007.68630
[39] Calheiros, R. N.; Netto, M. A.; Rose, C. A.D.; Buyya, R., EMUSIM: an integrated emulation and simulation environment for modeling, evaluation, and validation of performance of cloud computing applications, Softw. Pract. Exp., 43, 5, 595-612, (2013)
[40] Calheiros, R. N.; Buyya, R.; De Rose, C. A.F., Building an automated and self-configurable emulation testbed for grid applications, Softw. Pract. Exp., 40, 5, 405-429, (2010)
[41] Deelman, E.; Singh, G.; Livny, M.; Berriman, G. B.; Good, J., The cost of doing science on the cloud: the montage example, (Proceedings of the Conference on High Performance Computing (SC’08), (2008), IEEE/ACM), 1-12
[42] Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L., Modeling resource-aware virtualized applications for the cloud in real-time ABS, (Aoki, T.; Tagushi, K., Proc. 14th International Conference on Formal Engineering Methods (ICFEM’12), Lecture Notes in Computer Science, vol. 7635, (2012), Springer), 71-86
[43] de Boer, F. S.; Hähnle, R.; Johnsen, E. B.; Schlatte, R.; Wong, P. Y.H., Formal modeling of resource management for cloud architectures: an industrial case study, (Paoli, F. D.; Pimentel, E.; Zavattaro, G., Proc. European Conference on Service-Oriented and Cloud Computing (ESOCC 2012), Lecture Notes in Computer Science, vol. 7592, (2012), Springer), 91-106
[44] Albert, E.; de Boer, F. S.; Hähnle, R.; Johnsen, E. B.; Schlatte, R.; Tapia Tarifa, S. L.; Wong, P. Y.H., Formal modeling and analysis of resource management for cloud architectures: an industrial case study using real-time ABS, Serv. Oriented Comput. Appl., (2014), in press
[45] Epifani, I.; Ghezzi, C.; Mirandola, R.; Tamburrelli, G., Model evolution by run-time parameter adaptation, (Proc. 31st International Conference on Software Engineering (ICSE’09), (2009), IEEE), 111-121
[46] Balsamo, S.; Marco, A. D.; Inverardi, P.; Simeoni, M., Model-based performance prediction in software development: a survey, IEEE Trans. Softw. Eng., 30, 5, 295-310, (2004)
[47] Vulgarakis, A.; Seceleanu, C. C., Embedded systems resources: views on modeling and analysis, (Proc. 32nd IEEE Intl. Computer Software and Applications Conference (COMPSAC’08), (2008), IEEE Computer Society), 1321-1328
[48] Chakrabarti, A.; de Alfaro, L.; Henzinger, T. A.; Stoelinga, M., Resource interfaces, (Alur, R.; Lee, I., Proc. Third International Conference on Embedded Software (EMSOFT’03), Lecture Notes in Computer Science, vol. 2855, (2003), Springer), 117-133
[49] Fersman, E.; Krcál, P.; Pettersson, P.; Yi, W., Task automata: schedulability, decidability and undecidability, Inf. Comput., 205, 8, 1149-1172, (2007) · Zbl 1121.68062
[50] Jaghoori, M. M.; de Boer, F. S.; Chothia, T.; Sirjani, M., Schedulability of asynchronous real-time concurrent objects, J. Log. Algebr. Program., 78, 5, 402-416, (2009) · Zbl 1188.68085
[51] de Boer, F. S.; Jaghoori, M. M.; Johnsen, E. B., Dating concurrent objects: real-time modeling and schedulability analysis, (Gastin, P.; Laroussinie, F., Proc. 21st Intl. Conf. on Concurrency Theory (CONCUR), Lecture Notes in Computer Science, vol. 6269, (2010), Springer), 1-18
[52] Koziolek, H., Performance evaluation of component-based software systems: a survey, Perform. Eval., 67, 8, 634-658, (2010)
[53] Smith, C. U.; Williams, L. G., Performance solutions: A practical guide to creating responsive, scalable software, (2002), Addison-Wesley
[54] Petriu, D. B.; Woodside, C. M., An intermediate metamodel with scenarios and resources for generating performance models from UML designs, Softw. Syst. Model., 6, 2, 163-184, (2007)
[55] Verhoef, M.; Larsen, P. G.; Hooman, J., Modeling and validating distributed embedded real-time systems with VDM++, (Misra, J.; Nipkow, T.; Sekerinski, E., Proceedings of the 14th International Symposium on Formal Methods (FM’06), Lecture Notes in Computer Science, vol. 4085, (2006), Springer), 147-162
[56] Reussner, R.; Schmidt, H. W.; Poernomo, I., Reliability prediction for component-based software architectures, J. Syst. Softw., 66, 3, 241-252, (2003)
[57] Becker, S.; Koziolek, H.; Reussner, R., The palladio component model for model-driven performance prediction, J. Syst. Softw., 82, 1, 3-22, (2009)
[58] Happe, L.; Buhnova, B.; Reussner, R., Stateful component-based performance models, Softw. Syst. Model., (2014), in press
[59] Albert, E.; Arenas, P.; Genaim, S.; Puebla, G.; Zanardini, D., Cost analysis of Java bytecode, (16th European Symposium on Programming (ESOP’07), Lecture Notes in Computer Science, vol. 4421, (2007), Springer), 157-172
[60] Gulwani, S.; Mehra, K. K.; Chilimbi, T. M., SPEED: precise and efficient static estimation of program computational complexity, (Shao, Z.; Pierce, B. C., Proc. 36th Symp. on Principles of Programming Languages (POPL’09), (2009), ACM), 127-139 · Zbl 1315.68095
[61] (Beckert, B.; Hähnleiba, R.; Schmitt, P. H., Verification of Object-Oriented Software. The KeY Approach, Lecture Notes in Artificial Intelligence, vol. 4334, (2007), Springer)
[62] Sen, K.; Viswanathan, M.; Agha, G., On statistical model checking of stochastic systems, (Etessami, K.; Rajamani, S. K., Proc. 17th International Conference on Computer Aided Verification (CAV’05), Lecture Notes in Computer Science, vol. 3576, (2005), Springer), 266-280 · Zbl 1081.68635
[63] David, A.; Larsen, K. G.; Legay, A.; Mikucionis, M.; Poulsen, D. B.; van Vliet, J.; Wang, Z., Statistical model checking for networks of priced timed automata, (Fahrenberg, U.; Tripakis, S., Proc. 9th Intl. Conf. on Formal Modeling and Analysis of Timed Systems (FORMATS’11), Lecture Notes in Computer Science, vol. 6919, (2011), Springer), 80-96 · Zbl 1348.68130
[64] AlTurki, M.; Meseguer, J., Pvesta: a parallel statistical model checking and quantitative analysis tool, (Corradini, A.; Klin, B.; Cîrstea, C., Proc. 4th International Conference on Algebra and Coalgebra in Computer Science (CALCO’11), Lecture Notes in Computer Science, vol. 6859, (2011), Springer), 386-392
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.