Abstract
Modern distributed systems are often coupled with flexible architectures, composed of heterogenous components, and deployed on different execution nodes. Under such frameworks, connectors (or middlewares) are widely used to organize the separated components and make them functioning. Apparently, reliability of such systems highly depends on the correctness of their connectors. Reo is a channel-based coordination language where complex connectors are constructed from simpler ones through a compositional approach. In this paper, we propose a stochastic and real-time extension of Reo, including a set of new primitive channels and an expressive semantics named Stochastic Timed Automata for Reo (\(\text {STA}_r\)). With the support of \(\text {STA}_r\), different coordination scenarios in existing Reo extensions can be easily encoded, integrated, and analyzed.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
Proof can be found at https://github.com/liyi-david/ReoSTA.
References
The JANI specification of the jani-model format and the jani-interaction protocol. http://www.jani-spec.org/
Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(3), 329–366 (2004)
Arbab, F., Baier, C., de Boer, F.S., Rutten, J.J.M.M.: Models and temporal logical specifications for timed component connectors. Softw. Syst. Model. 6(1), 59–82 (2007)
Arbab, F., Chothia, T., Mei, R., Meng, S., Moon, Y.J., Verhoef, C.: From coordination to stochastic models of QoS. In: Field, J., Vasconcelos, V.T. (eds.) COORDINATION 2009. LNCS, vol. 5521, pp. 268–287. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02053-7_14
Baier, C.: Probabilistic models for Reo connector circuits. J. Univ. Comput. Sci. 11(10), 1718–1748 (2005)
Baier, C., Sirjani, M., Arbab, F., Rutten, J.: Modeling component connectors in Reo by constraint automata. Sci. Comput. Program. 61(2), 75–113 (2006)
Baier, C., Wolf, V.: Stochastic reasoning about channel-based component connectors. In: Ciancarini, P., Wiklicky, H. (eds.) COORDINATION 2006. LNCS, vol. 4038, pp. 1–15. Springer, Heidelberg (2006). https://doi.org/10.1007/11767954_1
Hahn, E.M., Hartmanns, A., Hermanns, H.: Reachability and reward checking for stochastic timed automata. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 70 (2014)
Hahn, E.M., Li, Y., Schewe, S., Turrini, A., Zhang, L.: iscasMc: a web-based probabilistic model checker. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 312–317. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-06410-9_22
Hartmanns, A.: Modest a unified language for quantitative models. In: Proceedings of FDL 2012, pp. 44–51. IEEE (2012)
Jongmans, S.S.T.Q., Arbab, F.: Overview of thirty semantic formalisms for Reo. Sci. Ann. Comput. Sci. 22(1), 201–251 (2012)
Li, H.: Introducing Windows Azure. Apress, Berkely (2009)
Meng, S.: Connectors as designs: the time dimension. In: Proceedings of TASE 2012, pp. 201–208. IEEE Computer Society (2012)
Meng, S., Arbab, F.: On resource-sensitive timed component connectors. In: Bonsangue, M.M., Johnsen, E.B. (eds.) FMOODS 2007. LNCS, vol. 4468, pp. 301–316. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72952-5_19
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)
Oliveira, N., Barbosa, L.S.: An enhanced model for stochastic coordination. Electron. Proc. Theor. Comput. Sci. 228, 35–45 (2016)
Pierro, A., Hankin, C., Wiklicky, H.: Probabilistic KLAIM. In: Nicola, R., Ferrari, G.-L., Meredith, G. (eds.) COORDINATION 2004. LNCS, vol. 2949, pp. 119–134. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24634-3_11
Priami, C.: Stochastic pi-calculus. Comput. J. 38(7), 578–589 (1995)
Acknowledgements
The work was partially supported by the National Natural Science Foundation of China under grant no. 61532019, 61202069 and 61272160.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Li, Y., Zhang, X., Ji, Y., Sun, M. (2017). Capturing Stochastic and Real-Time Behavior in Reo Connectors. In: Cavalheiro, S., Fiadeiro, J. (eds) Formal Methods: Foundations and Applications. SBMF 2017. Lecture Notes in Computer Science(), vol 10623. Springer, Cham. https://doi.org/10.1007/978-3-319-70848-5_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-70848-5_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-70847-8
Online ISBN: 978-3-319-70848-5
eBook Packages: Computer ScienceComputer Science (R0)