Abstract
The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous works by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is addressing key functional aspects of network aware programming such as distribution awareness, mobility and security and to guarantee their integration with performance and dependability guarantees. In this paper we present SoSL, a variant of MoSL, designed for dealing with specific features of Service-Oriented Computing (SOC). We also show how SoSL formulae can be model-checked against systems descriptions expressed with MarCaSPiS, a process calculus designed for addressing quantitative aspects of SOC. In order to perform actual model checking, we rely on a dedicated front-end that uses existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC).
This work has been partially sponsored by the project Sensoria, IST-2005-016004.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoret. Comput. Sci. 126, 183–235 (1994)
Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking Continuous Time Markov Chains. ACM Transactions on Computational Logic 1(1), 162–170 (2000)
Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Transactions on Software Engineering 29(6), 524–541 (2003)
Boreale, M., Bruni, R., De Nicola, R., Loreti, M.: Sessions and pipelines for structured service programming. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 19–38. Springer, Heidelberg (2008)
Brinksma, E., Hermanns, H.: Process Algebra and Markov Chains. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol. 2090, pp. 183–231. Springer, Heidelberg (2001)
Caires, L., Cardelli, L.: A spatial logic for concurrency (part I). Information and Computation 186(2), 194–235 (2003)
Cardelli, L., Gordon, A.: Anytime, anywhere: modal logics for mobile ambients. In: Twentyseventh Annual ACM Symposium on Principles of Programming Languages, pp. 365–377. ACM, New York (2000)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Logic of Programs, pp. 52–71 (1981)
De Nicola, R., Katoen, J.P., Latella, D., Loreti, M., Massink, M.: Model checking mobile stochastic logic. Theoretical Computer Science 382(1), 42–70 (2007)
De Nicola, R., Latella, D., Loreti, M., Massink, M.: MarCaSPiS: a Markovian Extension of a Calculus for Services. Electronic Notes in Theoretical Computer Science 229(4), 11–26 (2009)
De Nicola, R., Latella, D., Loreti, M., Massink, M.: On a Uniform Framework for the Definition of Stochastic Process Languages. In: Alpuente, M., Cook, B., Joubert, C. (eds.) FMICS 2009. LNCS, vol. 5825, pp. 9–25. Springer, Heidelberg (2009)
De Nicola, R., Latella, D., Loreti, M., Massink, M.: Rate-Based Transition Systems for Stochastic Process Calculi. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009. LNCS, vol. 5556, pp. 435–446. Springer, Heidelberg (2009)
De Nicola, R., Loreti, M.: A modal logic for mobile agents. ACM Transactions on Computational Logic 5(1), 79–128 (2004)
De Nicola, R., Loreti, M.: Multiple-Labelled Transition Systems for nominal calculi and their logics. Mathematical Structures in Computer Science 18(1), 107–143 (2008)
De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Fantechi, A., Gnesi, S., Lapadula, A., Mazzanti, F., Pugliese, R., Tiezzi, F.: A model checking approach for verifying cows specifications. In: Fiadeiro, J.L., Inverardi, P. (eds.) FASE 2008. LNCS, vol. 4961, pp. 230–245. Springer, Heidelberg (2008)
Ferrari, G., Gnesi, S., Montanari, U., Pistore, M.: A model-checking verification environment for mobile processes. ACM Publications Home Page Transactions on Software Engineering and Methodology 12(4), 440–473 (2003)
Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing 6(5), 512–535 (1994)
Hart, S., Sharir, M.: Probabilistic Temporal Logics for Finite and Bounded Models. In: De Millo, R. (ed.) 16th Annual ACM Symposium on Theory of Computing, pp. 1–13. ACM, New York (1984) ISBN 0-89791-133-4
Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol. 1945, pp. 420–439. Springer, Heidelberg (2000)
Hillston, J.: A compositional approach to performance modelling. Distinguished Dissertation in Computer Science. Cambridge University Press, Cambridge (1996)
Katoen, J.-P., Khattri, M., Zapreev, I.: A Markov reward model checker. In: Second International Conference on the Quantitative Evaluation of Systems (QEST 2005), pp. 243–244 (2005) ISBN 0-7695-0418-3
Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic Symbolic Model Checking using PRISM: A Hybrid Approach. Software Tools and Technology Transfer 6(2), 128–142 (2004)
Merz, S., Wirsing, M., Zappe, J.: A spatio-temporal logic for the specification and refinement of mobile systems. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 87–101. Springer, Heidelberg (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
De Nicola, R., Latella, D., Loreti, M., Massink, M. (2011). SoSL: A Service-Oriented Stochastic Logic. In: Wirsing, M., Hölzl, M. (eds) Rigorous Software Engineering for Service-Oriented Systems. Lecture Notes in Computer Science, vol 6582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20401-2_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-20401-2_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20400-5
Online ISBN: 978-3-642-20401-2
eBook Packages: Computer ScienceComputer Science (R0)