{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T14:48:10Z","timestamp":1761490090430,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471655"},{"type":"electronic","value":"9783319471662"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47166-2_56","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T18:07:34Z","timestamp":1475604454000},"page":"806-820","source":"Crossref","is-referenced-by-count":19,"title":["A Logic for the Statistical Model Checking of Dynamic Software Architectures"],"prefix":"10.1007","author":[{"given":"Jean","family":"Quilbeuf","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Everton","family":"Cavalcante","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Louis-Marie","family":"Traonouez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Flavio","family":"Oquendo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thais","family":"Batista","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"56_CR1","unstructured":"PLASMA-Lab. https:\/\/project.inria.fr\/plasma-lab\/"},{"issue":"2","key":"56_CR2","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/s10009-011-0212-z","volume":"14","author":"PA Abdulla","year":"2012","unstructured":"Abdulla, P.A., Jonsson, B., Nilsson, M., d\u2019Orso, J., Saksena, M.: Regular model checking for LTL(MSO). Int. J. Softw. Tools Technol. Transfer 14(2), 223\u2013241 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"56_CR3","doi-asserted-by":"crossref","unstructured":"Basso, A., Bolotov, A., Basukoski, A., Getov, V., Henrio, L., Urbanski, M.: Specification and verification of reconfiguration protocols in grid component systems. In: Proceedings of the 3rd IEEE Conference on Intelligent Systems (2006)","DOI":"10.1109\/IS.2006.348461"},{"key":"56_CR4","doi-asserted-by":"crossref","unstructured":"Cavalcante, E., Batista, T., Oquendo, F.: Supporting dynamic software architectures: from architectural description to implementation. In: Proceedings of the 12th Working IEEE\/IFIP Conference on Software Architecture, pp. 31\u201340. IEEE Computer Society, Washington, D.C. (2015)","DOI":"10.1109\/WICSA.2015.21"},{"key":"56_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"130","DOI":"10.1007\/978-3-319-09970-5_13","volume-title":"Software Architecture","author":"E Cavalcante","year":"2014","unstructured":"Cavalcante, E., Oquendo, F., Batista, T.: Architecture-based code generation: from $$\\pi $$ \u03c0 -ADL architecture descriptions to implementations in the go language. In: Avgeriou, P., Zdun, U. (eds.) ECSA 2014. LNCS, vol. 8627, pp. 130\u2013145. Springer, Heidelberg (2014)"},{"key":"56_CR6","series-title":"Lecture Notes in Computer Science","first-page":"806","volume-title":"ISoLA 2016","author":"E Cavalcante","year":"2016","unstructured":"Cavalcante, E., Quilbeuf, J., Traonouez, L.M., Oquendo, F., Batista, T., Legay, A.: Statistical model checking of dynamic software architectures. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part I. LNCS, vol. 9952, pp. 806\u2013820. Springer, Heidelberg (2016)"},{"issue":"4","key":"56_CR7","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1049\/ip-sen:20010558","volume":"148","author":"SM Cho","year":"2001","unstructured":"Cho, S.M., Kim, H.H., Cha, S.D., Bae, D.H.: Specification and validation of dynamic systems using temporal logic. IEE Proc. Softw. 148(4), 135\u2013140 (2001)","journal-title":"IEE Proc. Softw."},{"key":"56_CR8","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"issue":"1","key":"56_CR9","doi-asserted-by":"crossref","first-page":"34","DOI":"10.1007\/s100090200075","volume":"4","author":"JC Corbett","year":"2002","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J.: Robby: expressing checkable properties of dynamic systems: the Bandera specification language. Int. J. Softw. Tools Technol. Transfer 4(1), 34\u201356 (2002)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"56_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/978-3-642-27269-1_12","volume-title":"Formal Aspects of Component Software","author":"J Dormoy","year":"2012","unstructured":"Dormoy, J., Kouchnarenko, O., Lanoix, A.: Using temporal logic for dynamic reconfigurations of components. In: Barbosa, L.S., Lumpe, M. (eds.) FACS 2010. LNCS, vol. 6921, pp. 200\u2013217. Springer, Heidelberg (2012)"},{"key":"56_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-3-540-24622-0_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"T H\u00e9rault","year":"2004","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"issue":"301","key":"56_CR12","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities for sums of bounded random variables. J. Am. Stat. Assoc. 58(301), 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"56_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1007\/978-3-642-28756-5_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"C Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012)"},{"key":"56_CR14","series-title":"Lecture Notes in Computer Science","first-page":"218","volume-title":"Computational Methods in Systems Biology","author":"SK Jha","year":"2009","unstructured":"Jha, S.K., Clarke, E.M., Langmead, C.J., Legay, A., Platzer, A., Zuliani, P.: A Bayesian approach to model checking biological systems. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 218\u2013234. Springer, Heidelberg (2009)"},{"issue":"3","key":"56_CR15","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1109\/MS.2013.24","volume":"30","author":"Y Kim","year":"2013","unstructured":"Kim, Y., Choi, O., Kim, M., Baik, J., Kim, T.H.: Validating software reliability early through statistical model checking. IEEE Softw. 30(3), 35\u201341 (2013)","journal-title":"IEEE Softw."},{"issue":"4","key":"56_CR16","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/1276920.1276922","volume":"8","author":"S Laplante","year":"2007","unstructured":"Laplante, S., Lassaigne, R., Magniez, F., Peyronnet, S., de Rougemont, M.: Probabilistic abstraction for model checking: an approach based on property testing. ACM Trans. Comput. Logic 8(4), 20 (2007)","journal-title":"ACM Trans. Comput. Logic"},{"key":"56_CR17","volume-title":"Applied Probability and Statistics","author":"M Lefebvre","year":"2006","unstructured":"Lefebvre, M.: Applied Probability and Statistics. Springer, New York (2006)"},{"key":"56_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1007\/978-3-642-16612-9_11","volume-title":"Runtime Verification","author":"A Legay","year":"2010","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122\u2013135. Springer, Heidelberg (2010)"},{"issue":"4","key":"56_CR19","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1007\/s10009-015-0384-z","volume":"17","author":"A Legay","year":"2015","unstructured":"Legay, A., Viswanathan, M.: Statistical model checking: challenges and perspectives. Int. J. Softw. Tools Technol. Transfer 17(4), 369\u2013376 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"56_CR20","doi-asserted-by":"crossref","unstructured":"Magee, J., Kramer, J.: Dynamic structure in software architectures. In: Proceedings of the 4th ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 3\u201314. ACM, New York (1996)","DOI":"10.1145\/239098.239104"},{"issue":"2","key":"56_CR21","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/1118537.1118541","volume":"31","author":"R Mateescu","year":"2006","unstructured":"Mateescu, R., Oquendo, F.: $$\\pi $$ \u03c0 -AAL: an architecture analysis language for formally specifying and verifying structural and behavioural properties of software architectures. ACM SIGSOFT Softw. Eng. Notes 31(2), 1\u201319 (2006)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"56_CR22","doi-asserted-by":"crossref","unstructured":"Mazzara, M., Bhattacharyya, A.: On modelling and analysis of dynamic reconfiguration of dependable real-time systems. In: Proceedings of the Third International Conference on Dependability, pp. 173\u2013181 (2010)","DOI":"10.1109\/DEPEND.2010.33"},{"issue":"3","key":"56_CR23","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/986710.986728","volume":"29","author":"F Oquendo","year":"2004","unstructured":"Oquendo, F.: $$\\pi $$ \u03c0 -ADL: an architecture description language based on the higher-order typed $$\\pi $$ \u03c0 -calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT Softw. Eng. Notes 29(3), 1\u201314 (2004)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"56_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logics of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, pp. 46\u201357. IEEE Computer Society, Washington, D.C. (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"56_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"56_CR26","volume-title":"Software Architecture: Foundations, Theory, and Practice","author":"RN Taylor","year":"2010","unstructured":"Taylor, R.N., Medvidovic, N., Dashofy, E.M.: Software Architecture: Foundations, Theory, and Practice. Wiley, Hoboken (2010)"},{"issue":"3","key":"56_CR27","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"HLS Younes","year":"2006","unstructured":"Younes, H.L.S., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transfer 8(3), 216\u2013228 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"56_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Computer Aided Verification","author":"HLS Younes","year":"2002","unstructured":"Younes, H.L.S., Simmons, R.G.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 223. Springer, Heidelberg (2002)"},{"key":"56_CR29","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Doctoral dissertation, Carnegie Mellon University (2004)"},{"issue":"5","key":"56_CR30","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":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47166-2_56","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,14]],"date-time":"2019-09-14T04:10:31Z","timestamp":1568434231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47166-2_56"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471655","9783319471662"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47166-2_56","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}