Mixing logics and rewards for the component-oriented specification of performance measures. (English) Zbl 1159.68020
Summary: Formal notations for system performance modeling need to be equipped with suitable notations for specifying performance measures. These companion notations have been traditionally based on reward structures and, more recently, on temporal logics. In this paper we propose an approach that combines logics and rewards, together with a definition mechanism that allows performance measures to be specified in a component-oriented way, thus facilitating the task for non-experts. The resulting Measure Specification Language (MSL) is interpreted both on action-labeled continuous-time Markov chains and on stochastic process algebras. The latter interpretation provides a compositional framework for performance-sensitive model manipulations and emphasizes the increased expressiveness with respect to traditional reward structures for implicit-state modeling notations.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Keywords:
continuous-time Markov chains; stochastic process algebra; reward structures; component oriented modeling; measure specification languageReferences:
| [1] | Acquaviva, A.; Aldini, A.; Bernardo, M.; Bogliolo, A.; Bontà, E.; Lattanzi, E., A methodology based on formal methods for predicting the impact of dynamic power management, (Formal Methods for Mobile Computing. Formal Methods for Mobile Computing, LNCS, vol. 3465 (2005)), 155-189 |
| [2] | Ajmone Marsan, M.; Balbo, G.; Conte, G.; Donatelli, S.; Franceschinis, G., Modelling with Generalized Stochastic Petri Nets (1995), John Wiley & Sons · Zbl 0843.68080 |
| [3] | Aldini, A.; Bernardo, M., On the usability of process algebra: An architectural view, Theoretical Computer Science, 335, 281-329 (2005) · Zbl 1080.68071 |
| [4] | Aldini, A.; Bernardo, M., Component-oriented specification of performance measures, (Proc. of the 4th Int. Workshop on Quantitative Aspects of Programming Languages, QAPL 2006. Proc. of the 4th Int. Workshop on Quantitative Aspects of Programming Languages, QAPL 2006, ENTCS, vol. 164 (2006)), 27-43 |
| [5] | Alur, R.; Henzinger, T. A., Reactive modules, (Proc. of the 11th Symp. on Logic in Computer Science, LICS 1996 (1996), IEEE-CS Press), 207-218 |
| [6] | Baier, C.; Katoen, J.-P.; Hermanns, H., Approximate symbolic model checking of continuous time Markov chains, (Proc. of the 10th Int. Conf. on Concurrency Theory, CONCUR 1999. Proc. of the 10th Int. Conf. on Concurrency Theory, CONCUR 1999, LNCS, vol. 1664 (1999)), 146-162 · Zbl 0934.03044 |
| [7] | Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J.-P., On the logical characterisation of performability properties, (Proc. of the 27th Int. Coll. on Automata, Languages and Programming, ICALP 2000. Proc. of the 27th Int. Coll. on Automata, Languages and Programming, ICALP 2000, LNCS, vol. 1853 (2000)), 780-792 · Zbl 0973.68014 |
| [8] | Balsamo, S.; Bernardo, M.; Simeoni, M., Performance evaluation at the software architecture level, (Formal Methods for Software Architectures. Formal Methods for Software Architectures, LNCS, vol. 2804 (2003)), 207-258 |
| [9] | M. Bernardo, TwoTowers 5.1 User Manual, http://www.sti.uniurb.it/bernardo/twotowers/; M. Bernardo, TwoTowers 5.1 User Manual, http://www.sti.uniurb.it/bernardo/twotowers/ |
| [10] | Bernardo, M.; Bravetti, M., Reward based congruences: Can we aggregate more?, (Proc. of the Joint Int. Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification, PAPM/PROBMIV 2001. Proc. of the Joint Int. Workshop on Process Algebra and Performance Modelling and Probabilistic Methods in Verification, PAPM/PROBMIV 2001, LNCS, vol. 2165 (2001)), 136-151 · Zbl 1007.68132 |
| [11] | Bernardo, M.; Bravetti, M., Performance measure sensitive congruences for Markovian process algebras, Theoretical Computer Science, 290, 117-160 (2003) · Zbl 1019.68065 |
| [12] | Bernardo, M.; Donatiello, L.; Ciancarini, P., Stochastic process algebra: From an algebraic formalism to an architectural description language, (Performance Evaluation of Complex Systems: Techniques and Tools. Performance Evaluation of Complex Systems: Techniques and Tools, LNCS, vol. 2459 (2002)), 236-260 · Zbl 1017.68579 |
| [13] | Ciardo, G.; Jones, R. L.; Miner, A. S.; Siminiceanu, R., SMART: Stochastic model analyzer for reliability and timing, (Tools of Int. Multiconference on Measurement, Modelling and Evaluation of Computer Communication Systems (2001)), 29-34 |
| [14] | Ciardo, G.; Muppala, J.; Trivedi, K. S., On the solution of GSPN reward models, Performance Evaluation, 12, 237-253 (1991) · Zbl 0754.60097 |
| [15] | Clark, G., Formalising the specification of rewards with PEPA, (Proc. of the 4th Workshop on Process Algebras and Performance Modelling, PAPM 1996 (1996), CLUT), 139-160 |
| [16] | Clark, G.; Gilmore, S.; Hillston, J., Specifying performance measures for PEPA, (Proc. of the 5th AMAST Int. Workshop on Formal Methods for Real Time and Probabilistic Systems, ARTS 1999. Proc. of the 5th AMAST Int. Workshop on Formal Methods for Real Time and Probabilistic Systems, ARTS 1999, LNCS, vol. 1601 (1999)), 211-227 |
| [17] | Courtney, T.; Daly, D.; Derisavi, S.; Gaonkar, S.; Griffith, M.; Lam, V.; Sanders, W. H., The Möbius modeling environment: Recent developments, (Proc. of the 1st Int. Conference on Quantitative Evaluation of Systems, QEST 2004 (2004), IEEE-CS Press), 328-329 |
| [18] | Haverkort, B. R.; Trivedi, K. S., Specification techniques for Markov reward models, Discrete Event Dynamic Systems: Theory and Applications, 3, 219-247 (1993) · Zbl 0777.68029 |
| [19] | Hermanns, H., (Interactive Markov Chains. Interactive Markov Chains, LNCS, vol. 2428 (2002)) · Zbl 1012.68142 |
| [20] | Hillston, J., A Compositional Approach to Performance Modelling (1996), Cambridge University Press |
| [21] | Howard, R. A., Dynamic Probabilistic Systems (1971), John Wiley & Sons · Zbl 0227.90031 |
| [22] | Katoen, J.-P.; Khattri, M.; Zapreev, I. S., A Markov reward model checker, (Proc. of the 2nd Int. Conference on Quantitative Evaluation of Systems, QEST 2005 (2005), IEEE-CS Press), 243-244 |
| [23] | Kwiatkowska, M.; Norman, G.; Pacheco, A., Model checking expected time and expected reward formulae with random time bounds, Computers & Mathematics with Applications, 51, 305-316 (2006) · Zbl 1104.68067 |
| [24] | Kwiatkowska, M.; Norman, G.; Parker, D., PRISM: Probabilistic symbolic model checker, (Proc. of the 12th Int. Conference on Modelling Techniques and Tools for Computer Performance Evaluation, TOOLS 2002. Proc. of the 12th Int. Conference on Modelling Techniques and Tools for Computer Performance Evaluation, TOOLS 2002, LNCS, vol. 2324 (2002)), 200-204 · Zbl 1047.68533 |
| [25] | Kleinrock, L., Queueing Systems (1975), John Wiley & Sons · Zbl 0334.60045 |
| [26] | Qureshi, M. A.; Sanders, W. H., Reward model solution methods with impulse and rate rewards: An algorithm and numerical results, Performance Evaluation, 20, 413-436 (1994) · Zbl 0941.68518 |
| [27] | Sanders, W. H.; Meyer, J. F., A unified approach for specifying measures of performance, dependability, and performability, Dependable Computing and Fault Tolerant Systems, 4, 215-237 (1991) |
| [28] | Stewart, W. J., Introduction to the Numerical Solution of Markov Chains (1994), Princeton University Press · Zbl 0821.65099 |
| [29] | Voeten, J. E., Temporal rewards for performance evaluation, (Proc. of the 8th Int. Workshop on Process Algebra and Performance Modelling, PAPM 2000 (2000), Carleton Scientific), 511-522 |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
