{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,3]],"date-time":"2026-03-03T15:54:11Z","timestamp":1772553251673,"version":"3.50.1"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319489919","type":"print"},{"value":"9783319489926","type":"electronic"}],"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-48992-6_14","type":"book-chapter","created":{"date-parts":[[2016,11,2]],"date-time":"2016-11-02T05:25:50Z","timestamp":1478064350000},"page":"185-200","source":"Crossref","is-referenced-by-count":22,"title":["Statistical Model Checking of Dynamic Software Architectures"],"prefix":"10.1007","author":[{"given":"Everton","family":"Cavalcante","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean","family":"Quilbeuf","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,11,3]]},"reference":[{"key":"14_CR1","unstructured":"The Go programming language. https:\/\/golang.org\/"},{"key":"14_CR2","unstructured":"PLASMA-Lab. https:\/\/project.inria.fr\/plasma-lab\/"},{"key":"14_CR3","doi-asserted-by":"crossref","unstructured":"Arnold, A., Boyer, B., Legay, A.: Contracts and behavioral patterns for SoS: the EU IP DANSE approach. In: Larsen, K.G., Legay, A., Nyman, U. (eds.) Proceedings of the 1st Workshop on Advances in Systems of Systems, EPTCS, vol. 133, pp. 47\u201360 (2013)","DOI":"10.4204\/EPTCS.133.6"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/978-3-642-40196-1_12","volume-title":"Quantitative Evaluation of Systems","author":"B Boyer","year":"2013","unstructured":"Boyer, B., Corre, K., Legay, A., Sedwards, S.: PLASMA-lab: a flexible, distributable statistical model checking library. In: Joshi, K., Siegle, M., Stoelinga, M., D\u2019Argenio, P.R. (eds.) QEST 2013. LNCS, vol. 8054, pp. 160\u2013164. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-40196-1_12"},{"key":"14_CR5","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, USA (2015)","DOI":"10.1109\/WICSA.2015.21"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 $$ -ADL descriptions to implementations in the Go language. In: Avgeriou, P., Zdun, U. (eds.) ECSA 2014. LNCS, vol. 8627, pp. 130\u2013145. Springer, Switzerland (2014). doi: 10.1007\/978-3-319-09970-5_13"},{"issue":"4","key":"14_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":"14_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)"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-540-24622-0_8"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"Holzmann, G.J.: The logic of bugs. In: 10th ACM SIGSOFT Symposium on Foundations of Software Engineering, pp. 81\u201387. ACM, New York (2002)","DOI":"10.1145\/587051.587064"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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 - PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 498\u2013503. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-28756-5_37"},{"issue":"3","key":"14_CR12","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."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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). doi: 10.1007\/978-3-642-16612-9_11"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Legay, A., Sedwards, S.: On statistical model checking with PLASMA. In: Proceedings of the 2014 Theoretical Aspects of Software Engineering Conference, pp. 139\u2013145. IEEE Computer Society, Washington, DC (2014)","DOI":"10.1109\/TASE.2014.20"},{"issue":"2","key":"14_CR15","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 $$ -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"},{"issue":"3","key":"14_CR16","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/986710.986728","volume":"29","author":"F Oquendo","year":"2004","unstructured":"Oquendo, F.: $$\\pi $$ -ADL: an architecture description language based on the higher-order typed $$\\pi $$ -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":"14_CR17","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, DC (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1007\/978-3-319-47166-2_56","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques","author":"J Quilbeuf","year":"2016","unstructured":"Quilbeuf, J., Cavalcante, E., Traonouez, L.M., Oquendo, F., Batista, T., Legay, A.: A logic for statistical model checking of dynamic software architectures. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 806\u2013820. Springer, Heidelberg (2016). doi: 10.1007\/978-3-319-47166-2_56"},{"issue":"5","key":"14_CR19","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","Software Architecture"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-48992-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T22:36:26Z","timestamp":1498343786000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-48992-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319489919","9783319489926"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-48992-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}