Model checking mobile stochastic logic. (English) Zbl 1159.68478
Summary: The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous work by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is to address key functional aspects of global computing such as distribution awareness, mobility, and security and their integration with performance and dependability guarantees. In this paper, we present MoSL\(^+\), an extension of MoSL, which incorporates some basic features of the Modal Logic for MObility (MoMo), a logic specifically designed for dealing with resource management and mobility aspects of concurrent behaviours. We also show how MoSL\(^+\) formulae can be model-checked against StoKlaim specifications. For this purpose, we show how existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC), can be exploited by using a front-end for StoKlaim that performs appropriate pre-processing of MoSL\(^+\) formulae. The proposed approach is illustrated by modelling and verifying a sample system.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
Keywords:
Stochastic process algebra; Mobility; Global computing; Stochastic logics; Stochastic model-checkingReferences:
| [1] | Alur, R.; Dill, D., A theory of timed automata, Theoretical Computer Science, 126, 183-235 (1994) · Zbl 0803.68071 |
| [2] | Aziz, A.; Sanwal, K.; Singhal, V.; Brayton, R., Model checking continuous time Markov chains, ACM Transactions on Computational Logic, 1, 1, 162-170 (2000) · Zbl 1365.68313 |
| [3] | Aziz, A.; Singhal, V.; Balarin, F., It usually works: The temporal logic of stochastic systems, (Proceedings of CAV 1995. Proceedings of CAV 1995, LNCS, vol. 939 (1995)), 155-165 |
| [4] | Baier, C.; Cloth, L.; Haverkort, B.; Kuntz, M.; Siegle, M., Model checking action- and state-labelled Markov chains, (2004 International Conference on Dependable Systems & Networks (2004), IEEE Computer Society Press), 701-710 |
| [5] | Baier, C.; Katoen, J.-P.; Hermanns, H., Approximate symbolic model checking of continuous-time Markov chains, (Baeten, J.; Mauw, S., Concur ’99. Concur ’99, LNCS, vol. 1664 (1999), Springer-Verlag), 146-162 · Zbl 0934.03044 |
| [6] | Bettini, L.; Bono, V.; De Nicola, R.; Ferrari, G.; Gorla, D.; Loreti, M.; Moggi, E.; Pugliese, R.; Tuosto, E.; Venneri, B., The Klaim project: Theory and practice, (Priami, C., Global Computing: Programming Environments, Languages, Security and Analysis of Systems. Global Computing: Programming Environments, Languages, Security and Analysis of Systems, LNCS, vol. 2874 (2003), Springer-Verlag), 88-150 · Zbl 1179.68027 |
| [7] | Bettini, L.; De Nicola, R.; Loreti, M., Formalizing properties of mobile agent systems, (Arbab, F.; Talcott, C., Coordination Models and Languages. Coordination Models and Languages, LNCS, vol. 2315 (2002), Springer-Verlag), 72-87 · Zbl 1053.68503 |
| [8] | Bianco, A.; de Alfaro, L., Model checking of probabalistic and nondeterministic systems, (Proceedings of FSTTCS 1995. Proceedings of FSTTCS 1995, LNCS, vol. 1026 (1995)), 499-513 · Zbl 1354.68167 |
| [9] | Boudol, G., ULM: A core programming model for global computing: (Extended abstract), (Schmidt, D. A., Programming Languages and Systems, 13th European Symposium on Programming. Programming Languages and Systems, 13th European Symposium on Programming, ESOP. Programming Languages and Systems, 13th European Symposium on Programming. Programming Languages and Systems, 13th European Symposium on Programming, ESOP, LNCS, vol. 2986 (2004), Springer-Verlag), 234-248 · Zbl 1126.68329 |
| [10] | Caires, L.; Cardelli, L., A spatial logic for concurrency (part I), Information and Computation, 186, 2, 194-235 (2003) · Zbl 1068.03022 |
| [11] | Cardelli, L., A language with distributed scope, (22nd Annual ACM Symposium on Principles of Programming Languages (1995), ACM), 286-297 |
| [12] | Cardelli, L., Abstractions for mobile computations, (Vitek, J.; Jensen, C., Secure Internet Programming. Secure Internet Programming, LNCS, vol. 1603 (1999), Springer-Verlag), 51-94 |
| [13] | Cardelli, L.; Gordon, A., Anytime, anywhere: Modal logics for mobile ambients, (Twentyseventh Annual ACM Symposium on Principles of Programming Languages (2000), ACM), 365-377 · Zbl 1323.68405 |
| [14] | Castagna, G.; Vitek, J., Seal: A framework for secure mobile computations, (Bal, H.; Belkhouche, B.; Cardelli, L., Internet Programming Languages. Internet Programming Languages, LNCS, vol. 1686 (1999), Springer-Verlag), 47-77 |
| [15] | de Alfaro, L., Temporal logics for the specification of performance and reliability, (Proceedings of STACS 1997. Proceedings of STACS 1997, LNCS, vol. 1200 (1997)), 165-176 · Zbl 1498.68155 |
| [16] | De Nicola, R.; Ferrari, G.; Pugliese, R., KLAIM: A kernel language for agents interaction and mobility, IEEE Transactions on Software Engineering. IEEE CS, 24, 5, 315-329 (1998) |
| [17] | R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, M. Massink, Klaimhttp://rap.dsi.unifi.it/ loreti/papers/TR062006.pdf; R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, M. Massink, Klaimhttp://rap.dsi.unifi.it/ loreti/papers/TR062006.pdf |
| [18] | R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, M. Massink, MoSLStoKlaimhttp://www1.isti.cnr.it/ Latella/MoSL.pdf; R. De Nicola, J.-P. Katoen, D. Latella, M. Loreti, M. Massink, MoSLStoKlaimhttp://www1.isti.cnr.it/ Latella/MoSL.pdf |
| [19] | De Nicola, R.; Katoen, J.-P.; Latella, D.; Massink, M., Towards a logic for performance and mobility, (Cerone, A.; Wiklicky, H., Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages. Proceedings of the Third Workshop on Quantitative Aspects of Programming Languages, QAPL 2005, Electronic Notes in Theoretical Computer Science, vol. 153 (2006), Elsevier Science Publishers B.V.), 161-175 |
| [20] | De Nicola, R.; Latella, D.; Massink, M., Formal modeling and quantitative analysis of KLAIM-based mobile systems, (Haddad, H.; Liebrock, L.; Omicini, A.; Wainwright, R.; Palakal, M.; Wilds, M.; Clausen, H., Applied Computing 2005. Proceedings of the 20th Annual ACM Symposium on Applied Computing (2005), Association for Computing Machinery — ACM), 428-435 |
| [21] | De Nicola, R.; Loreti, M., A modal logic for mobile agents, ACM Transactions on Computational Logic, 5, 1, 79-128 (2004) · Zbl 1367.68064 |
| [22] | De Nicola, R.; Loreti, M., MoMo: A modal logic for reasoning about mobility, (Proceedings of the Third International Symposium on Formal Methods for Components and Objects. Proceedings of the Third International Symposium on Formal Methods for Components and Objects, November 2004, Leiden, The Netherlands — FMCO 2004. Proceedings of the Third International Symposium on Formal Methods for Components and Objects. Proceedings of the Third International Symposium on Formal Methods for Components and Objects, November 2004, Leiden, The Netherlands — FMCO 2004, LNCS, vol. 3657 (2005), Springer-Verlag) · Zbl 1143.68364 |
| [23] | De Nicola, R.; Vaandrager, F., Action versus state based logics for transition systems, (Guessarian, I., Proceedings of LITP Spring School on Theoretical Computer Science. Proceedings of LITP Spring School on Theoretical Computer Science, LNCS, vol. 469 (1990), Springer-Verlag), 407-419 |
| [24] | Fantechi, A.; Gnesi, S.; Mazzarini, G., How much expressive are LOTOS expressions?, (Quemada, J.; Manas, J.; Thomas, M., Formal Description Techniques — III (1991), North-Holland Publishing Company) |
| [25] | Ferrari, G.; Gnesi, S.; Montanari, U.; Pistore, M., A model-checking verification environment for mobile processes, ACM Transactions on Software Engineering and Methodology, 12, 4, 440-473 (2003) |
| [26] | Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Aspects of Computing. The International Journal of Formal Methods, 6, 5, 512-535 (1994) · Zbl 0820.68113 |
| [27] | Hart, S.; Sharir, M., Probabilistic temporal logics for finite and bounded models, (De Millo, R., 16th Annual ACM Symposium on Theory of Computing (1984), Association for Computing Machinery — ACM), 1-13 |
| [28] | Hermanns, H.; Herzog, U.; Katoen, J.-P., Process algebra for performance evaluation, Theoretical Computer Science, 274, 1-2, 43-87 (2002) · Zbl 0992.68149 |
| [29] | H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, M. Siegle, Model checking stochastic process algebra, Technical Report IMMD7-2/00, Univ. of Nuernberg, 2000; H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, M. Siegle, Model checking stochastic process algebra, Technical Report IMMD7-2/00, Univ. of Nuernberg, 2000 · Zbl 1043.68594 |
| [30] | Hermanns, H.; Katoen, J.-P.; Meyer-Kayser, J.; Siegle, M., Towards model checking stochastic process algebra, (Grieskamp, W.; Santen, T.; Stoddart, B., Integrated Formal Methods — IFM 2000. Integrated Formal Methods — IFM 2000, LNCS, vol. 1945 (2000), Springer-Verlag), 420-439 · Zbl 1043.68594 |
| [31] | Hermanns, H.; Katoen, J.-P.; Meyer-Kayser, J.; Siegle, M., A tool for model-checking Markov chains, International Journal on Software Tools for Technology Transfer, 4, 2, 153-172 (2003) |
| [32] | Hillston, J., Process algebras for quantitative analysis, (IEEE Symposium on Logic in Computer Science (2005), IEEE, Computer Society Press), 239-248 |
| [33] | Katoen, J.-P.; Khattri, M.; Zapreev, I., A Markov reward model checker, (Second International Conference on the Quantitative Evaluation of Systems. Second International Conference on the Quantitative Evaluation of Systems, QEST’05 (2005), IEEE Computer Society Press), 243-244 |
| [34] | Kulkarni, V., Modeling and Analysis of Stochastic Systems (1995), Chapman & Hall · Zbl 0866.60004 |
| [35] | Kwiatkowska, M.; Norman, G.; Parker, D., Probabilistic symbolic model checking using PRISM: A hybrid approach, International Journal on Software Tools for Technology Transfer, 6, 2, 128-142 (2004) |
| [36] | Merz, S.; Wirsing, M.; Zappe, J., A spatio-temporal logic for the specification and refinement of mobile systems, (Pezzé, M., Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, FASE 2003. Fundamental Approaches to Software Engineering. Fundamental Approaches to Software Engineering, FASE 2003, LNCS, vol. 2621 (2003), Springer-Verlag), 87-101 · Zbl 1032.03028 |
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.
