Last ned (Gratis)

Abstrakt

Software today is often developed for deployment on different architectures.
In order to model and analyze the consequences of such deployment choices
at an early stage in software development, it seems desirable to capture
aspects of low-level deployment concerns in high-level models. In this
paper, we propose an integration of a generic cost model for resource
consumption with deployment components in timed ABS, an abstract
behavioral specification language for executable object-oriented models.
Deployment components reflect resource-restricted deployment scenarios,
and are parametric in their allocated resources. The cost model may be
adapted to specific resources such as concurrent processing capacities or
memory. The approach is demonstrated on an example of a web shop with a
cost model for concurrent processing resources. We use our simulation tool
to analyze system response time for given usage scenarios, depending on the
amount of resources allocated to the deployment components.

Referanser

[1] E. Albert, P. Arenas, S. Genaim, and G. Puebla. Closed-form upper bounds in static cost analysis. Journal of Automated Reasoning, 46:161–203, 2011.

[2] E. Albert, S. Genaim, M. Gómez-Zamalloa, E. B. Johnsen, R. Schlatte, and S. L. Tapia Tarifa. Simulating concurrent behaviors with worst-case cost bounds. In Proc. Formal Methods (FM 2011), LNCS 6664, pages 353–368. Springer, June 2011. [3] J. Armstrong. Programming Erlang: Software for a Concurrent World. Pragmatic Bookshelf, 2007.

[4] S. Balsamo, A. D. Marco, P. Inverardi, and M. Simeoni. Model-based performance prediction in software development: A survey. IEEE Transactions on Software Engineering, 30(5):295–310, 2004.

[5] A. Chakrabarti, L. de Alfaro, T. A. Henzinger, and M. Stoelinga. Resource interfaces. In Proc. 3rd Intl. Conf. on Embedded Software (EMSOFT’03), LNCS 2855, pages 117–133. Springer, 2003.

[6] P. Chalin, J. R. Kiniry, G. T. Leavens, and E. Poll. Beyond assertions: Advanced specification and verification with JML and ESC/Java2. In Proc. 4th Intl. Symp. on Formal Methods for Components and Objects (FMCO’04), LNCS 4111, pages 342–363. Springer, 2005.

[7] D. Clarke, et al. Modeling spatial and temporal variability with the HATS abstract behavioral modeling language. In Proc. 11th Intl. School on Formal Methods for the Design of Computer, Communication and Software Systems (SFM 2011), LNCS 6659, pages 417–457. Springer, 2011.

[8] M. Clavel, et al. All About Maude - A High-Performance Logical Framework, LNCS 4350. Springer, 2007.

[9] I. Epifani, C. Ghezzi, R. Mirandola, and G. Tamburrelli. Model evolution by runtime parameter adaptation. In Proc. ICSE, pages 111–121. IEEE, 2009.

[10] E. Fersman, P. Krcál, P. Pettersson, and W. Yi. Task automata: Schedulability, decidability and undecidability. Information and Computation, 205(8):1149–1172, 2007.

[11] N. E. Fuchs. Specifications are (preferably) executable. Software Engineering Journal, pages 323–334, Sept. 1992.

[12] P. Haller and M. Odersky. Scala actors: Unifying thread-based and event-based programming. Theoretical Computer Science, 410(2–3):202–220, 2009. [13] I. Hayes and C. Jones. Specifications are not (Necessarily) Executable. Software Engineering Journal, pages 330–338, November 1989.

[14] A. Hessel, K. G. Larsen, M. Mikucionis, B. Nielsen, P. Pettersson, and A. Skou. Testing real-time systems using UPPAAL. In Proc. Formal Methods and Testing, LNCS 4949, pages 77–117. Springer, 2008.

[15] M. M. Jaghoori, F. S. de Boer, T. Chothia, and M. Sirjani. Schedulability of asynchronous real-time concurrent objects. Journal of Logic and Algebraic Programming, 78(5):402–416, 2009.

[16] E. B. Johnsen, R. Hähnle, J. Schäfer, R. Schlatte, and M. Steffen. ABS: A core language for abstract behavioral specification. In Proc. Formal Methods for Components and Objects (FMCO 2010). To appear in LNCS. Springer, 2011. [17] E. B. Johnsen, O. Owe, R. Schlatte, and S. L. Tapia Tarifa. Dynamic resource reallocation between deployment components. In Proc. Formal Engineering Methods (ICFEM’10), LNCS 6447, pages 646–661. Springer, Nov. 2010. [18] E. B. Johnsen, O. Owe, R. Schlatte, and S. L. Tapia Tarifa. Validating timed models of deployment components with parametric concurrency. In Proc. Formal Verification of Object-Oriented Software (FoVeOOS’10), LNCS 6528, pages 46–60. Springer, 2011.

[19] J. Kramer. Is Abstraction the Key to Computing? Communications of the ACM, 50(4):37–42, 2007.

[20] D. B. Petriu and C. M. Woodside. An intermediate metamodel with scenarios and resources for generating performance models from UML designs. Software and System Modeling, 6(2):163–184, 2007.

[21] M. Verhoef, P. G. Larsen, and J. Hooman. Modeling and validating distributed embedded real-time systems with VDM++. In Proc. Formal Methods (FM’06), LNCS 4085, pages 147–162. Springer, 2006.

[22] A. Welc, S. Jagannathan, and A. Hosking. Safe futures for Java. In Proc. OOPSLA, pages 439–453. ACM Press, 2005.

[23] J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald. Formal Methods: Practice and Experience. ACM Computing Surveys, 41(4):1–36, October 2009.



Forrige artikkel      Neste artikkel