{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,3]],"date-time":"2022-04-03T07:49:44Z","timestamp":1648972184700},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,4,29]],"date-time":"2014-04-29T00:00:00Z","timestamp":1398729600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2016,5]]},"DOI":"10.1007\/s10270-014-0411-7","type":"journal-article","created":{"date-parts":[[2014,4,28]],"date-time":"2014-04-28T07:05:10Z","timestamp":1398668710000},"page":"453-471","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Formalizing and verifying stochastic system architectures using Monterey Phoenix"],"prefix":"10.1007","volume":"15","author":[{"given":"Songzheng","family":"Song","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiexin","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mikhail","family":"Auguston","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jun","family":"Sun","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin Song","family":"Dong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tieming","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,4,29]]},"reference":[{"key":"411_CR1","doi-asserted-by":"crossref","unstructured":"Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed) Fundamental Approaches to Software Engineering (FASE), vol. 1382, pp. 21\u201337. Springer, Berlin","DOI":"10.1007\/BFb0053581"},{"issue":"3","key":"411_CR2","doi-asserted-by":"crossref","first-page":"213","DOI":"10.1145\/258077.258078","volume":"6","author":"R Allen","year":"1997","unstructured":"Allen, R., Garlan, D.: A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol. 6(3), 213\u2013249 (1997)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"411_CR3","doi-asserted-by":"crossref","unstructured":"Auguston, M.: Monterey phoenix, or how to make software architecture executable. In: Arora, S., Leavens, G.T. (eds.) OOPSLA Companion, pp. 1031\u20131040. ACM, NY, USA (2009)","DOI":"10.1145\/1639950.1640075"},{"issue":"5","key":"411_CR4","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1598732.1598733","volume":"34","author":"M Auguston","year":"2009","unstructured":"Auguston, M.: Software architecture built from behavior models. ACM SIGSOFT Softw. Eng. Notes 34(5), 1\u201315 (2009)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"411_CR5","unstructured":"Auguston, M., Whitcomb, C.: System architecture specification based on behavior models. In: Proceedings of the 15th ICCRTS Conference (International Command and Control Research and Technology Symposium), Santa Monica, CA, June 22\u201324 (2010)"},{"key":"411_CR6","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"411_CR7","doi-asserted-by":"crossref","unstructured":"Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State\/event-based software model checking. In: Leuschel, M., Wehrheim, H. (eds.) IFM, vol. 2999 of LNCS, pp. 128\u2013147. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24756-2_8"},{"key":"411_CR8","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"3","key":"411_CR9","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1016\/j.scico.2005.04.003","volume":"59","author":"F Corradini","year":"2006","unstructured":"Corradini, F., Inverardi, P., Wolf, A.L.: On relating functional specifications to architectural specifications: a case study. Sci. Comput. Program. 59(3), 171\u2013208 (2006)","journal-title":"Sci. Comput. Program."},{"key":"411_CR10","unstructured":"Garlan, D., Monroe, R.T., Wile, D.: Acme: an architecture description interchange language. In: Johnson, J.H. (ed.) CASCON, p. 7, IBM, Toronto (1997)"},{"key":"411_CR11","doi-asserted-by":"crossref","first-page":"666","DOI":"10.1145\/359576.359585","volume":"21","author":"CAR Hoare","year":"1978","unstructured":"Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21, 666\u2013677 (1978)","journal-title":"Commun. ACM"},{"issue":"4","key":"411_CR12","doi-asserted-by":"crossref","first-page":"373","DOI":"10.1109\/32.385973","volume":"21","author":"P Inverardi","year":"1995","unstructured":"Inverardi, P., Wolf, A.L.: Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE Trans. Softw. Eng. 21(4), 373\u2013386 (1995)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"411_CR13","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol. 11(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"411_CR14","doi-asserted-by":"crossref","unstructured":"Kim, J.S., Garlan, D.: Analyzing architectural styles with alloy. In : Proceedings of the ISSTA 2006 Workshop on Role of Software Architecture for Testing and Analysis, ROSATEA \u201906, pp. 70\u201380. ACM, New York (2006)","DOI":"10.1145\/1147249.1147259"},{"key":"411_CR15","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, Snowbird, vol. 6806, pp. 585\u2013591, Springer, Heidelberg (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"411_CR16","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: An analyzer for extended compositional process algebras. In: Sch\u00e4fer, W., Dwyer, M.B., Gruhn, V. (eds.) ICSE Companion, pp. 919\u2013920. ACM, Leipzig, Germany (2008)","DOI":"10.1145\/1370175.1370187"},{"key":"411_CR17","doi-asserted-by":"crossref","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Pat 3:aAn extensible architecture for building multi-domain model checkers. In: Dohi, T., Cukic, B. (eds.) ISSRE, pp. 190\u2013199. IEEE, Hiroshima, Japan (2011)","DOI":"10.1109\/ISSRE.2011.19"},{"key":"411_CR18","doi-asserted-by":"crossref","unstructured":"Mahony, B.P., Dong, J.S.: Blending object-Z and timed CSP: an introduction to TCOZ. In: Proceedings of the 20th International Conference on Software Engineering (ICSE 1998), pp. 95\u2013104 (1998)","DOI":"10.1109\/ICSE.1998.671106"},{"key":"411_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli. A.: The temporal logic of programs. In: Gruska, J. (ed.) FOCS, pp. 46\u201357. IEEE, Rhode Island, USA (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"411_CR20","volume-title":"The Theory and Practice of Concurrency","author":"AW Roscoe.","year":"1997","unstructured":"Roscoe., A.W.: The Theory and Practice of Concurrency. Prentice Hall PTR, Englewood Cliffs (1997)"},{"key":"411_CR21","volume-title":"Combinatorial Optimization: Polyhedra and Efficiency","author":"A Schrijver","year":"2003","unstructured":"Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Berlin (2003)"},{"issue":"3","key":"411_CR22","doi-asserted-by":"crossref","first-page":"134","DOI":"10.2307\/2683444","volume":"29","author":"S Selvin","year":"1975","unstructured":"Selvin, S.: On the monty hall problem (letter to the editor). Am. Stat. 29(3), 134 (1975)","journal-title":"Am. Stat."},{"issue":"1","key":"411_CR23","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1080\/00031305.1975.10479121","volume":"29","author":"S Selvin","year":"1975","unstructured":"Selvin, S.: A problem in probability (letter to the editor). Am. Stat. 29(1), 67\u201371 (1975)","journal-title":"Am. Stat."},{"key":"411_CR24","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5265-9","volume-title":"The Object-Z Specification Language","author":"G Smith","year":"2000","unstructured":"Smith, G.: The Object-Z Specification Language. Kluwer Academic Publisher, Dordrecht (2000)"},{"key":"411_CR25","volume-title":"The Z Notation: A Reference Manual","author":"JM Spivey","year":"1989","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice-Hall Inc., Upper Saddle River (1989)"},{"key":"411_CR26","first-page":"176","volume":"78","author":"M Stoelinga","year":"2002","unstructured":"Stoelinga, M.: An introduction to probabilistic automata. Bull. EATCS 78, 176\u2013198 (2002)","journal-title":"Bull. EATCS"},{"key":"411_CR27","doi-asserted-by":"crossref","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV, vol. 5643 of LNCS, pp. 709\u2013714. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-02658-4_59"},{"key":"411_CR28","doi-asserted-by":"crossref","unstructured":"Sun, J., Song, S.Z., Liu. Y.: Model checking hierarchical probabilistic systems. In: Dong, J.S., Zhu, H. (eds.) Formal Methods and Software Engineering, ICFEM, vol. 6447, pp. 388\u2013403. Springer, Berlin (2010).","DOI":"10.1007\/978-3-642-16901-4_26"},{"key":"411_CR29","doi-asserted-by":"crossref","unstructured":"Tan, L., Krings, A.: An adaptive N-variant software architecture for multi-core platforms: models and performance analysis. In: Proceedings of the International Conference on Computational Science and Its Applications, Part II (ICCSA\u201911), pp. 490\u2013505 (2011)","DOI":"10.1007\/978-3-642-21887-3_38"},{"key":"411_CR30","doi-asserted-by":"crossref","unstructured":"Zhang, J., Liu, Y., Auguston, M., Sun, J., Dong, J.S.: Using monterey phoenix to formalize and verify system architectures. In: Leung, K.R.P.H., Muenchaisri, P. (eds.) APSEC, pp. 644\u2013653. IEEE, Hong Kong, China (2012)","DOI":"10.1109\/APSEC.2012.60"},{"issue":"5","key":"411_CR31","doi-asserted-by":"crossref","first-page":"723","DOI":"10.1016\/j.jss.2009.11.709","volume":"83","author":"P Zhang","year":"2010","unstructured":"Zhang, P., Muccini, H., Li, B.: A classification and comparison of model checking software architecture techniques. J. Syst. Softw. 83(5), 723\u2013744 (2010)","journal-title":"J. Syst. Softw."}],"container-title":["Software & Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0411-7.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10270-014-0411-7\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-014-0411-7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,9]],"date-time":"2019-08-09T23:01:00Z","timestamp":1565391660000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10270-014-0411-7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,4,29]]},"references-count":31,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,5]]}},"alternative-id":["411"],"URL":"https:\/\/doi.org\/10.1007\/s10270-014-0411-7","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,4,29]]}}}