{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:19:16Z","timestamp":1744258756084,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642340253"},{"type":"electronic","value":"9783642340260"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34026-0_25","type":"book-chapter","created":{"date-parts":[[2012,9,26]],"date-time":"2012-09-26T01:07:20Z","timestamp":1348621640000},"page":"327-341","source":"Crossref","is-referenced-by-count":15,"title":["Statistical Model Checking QoS Properties of Systems with SBIP"],"prefix":"10.1007","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Benoit","family":"Delahaye","sequence":"additional","affiliation":[]},{"given":"Cyrille","family":"Jegourel","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]},{"given":"Ayoub","family":"Nouri","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"25_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-13464-7_4","volume-title":"Formal Techniques for Distributed Systems","author":"A. Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical Abstraction and Model-Checking of Large Heterogeneous Systems. In: Hatcliff, J., Zucca, E. (eds.) FMOODS 2010, Part II. LNCS, vol.\u00a06117, pp. 32\u201346. Springer, Heidelberg (2010)"},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-16612-9_25","volume-title":"Runtime Verification","author":"A. Basu","year":"2010","unstructured":"Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an AFDX Infrastructure Using Simulations and Probabilities. In: Barringer, H., Falcone, Y., Finkbeiner, B., Havelund, K., Lee, I., Pace, G., Ro\u015fu, G., Sokolsky, O., Tillmann, N. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 330\u2013344. Springer, Heidelberg (2010)"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: SEFM 2006, pp. 3\u201312 (September 2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"25_CR4","unstructured":"Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: Present and future. In: RV. Springer (2010)"},{"key":"25_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22045-6_8","volume-title":"Software Composition","author":"S. Bensalem","year":"2011","unstructured":"Bensalem, S., de Silva, L., Griesmayer, A., Ingrand, F., Legay, A., Yan, R.: A Formal Approach for Incremental Construction with an Application to Autonomous Robotic Systems. In: Apel, S., Jackson, E. (eds.) SC 2011. LNCS, vol.\u00a06708, pp. 116\u2013132. Springer, Heidelberg (2011)"},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1007\/978-3-642-21461-5_4","volume-title":"Formal Techniques for Distributed Systems","author":"J. Bogdoll","year":"2011","unstructured":"Bogdoll, J., Ferrer Fioriti, L.M., Hartmanns, A., Hermanns, H.: Partial Order Methods for Statistical Model Checking and Simulation. In: Bruni, R., Dingel, J. (eds.) FORTE 2011 and FMOODS 2011. LNCS, vol.\u00a06722, pp. 59\u201374. Springer, Heidelberg (2011)"},{"key":"25_CR7","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (1999)"},{"key":"25_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-642-24690-6_15","volume-title":"Software Engineering and Formal Methods","author":"Y. Falcone","year":"2011","unstructured":"Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime Verification of Component-Based Systems. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol.\u00a07041, pp. 204\u2013220. Springer, Heidelberg (2011)"},{"key":"25_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-540-31980-1_18","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Grosu","year":"2005","unstructured":"Grosu, R., Smolka, S.A.: Monte Carlo Model Checking. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 271\u2013286. Springer, Heidelberg (2005)"},{"key":"25_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-46002-0_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K. Havelund","year":"2002","unstructured":"Havelund, K., Ro\u015fu, G.: Synthesizing Monitors for Safety Properties. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 342\u2013356. Springer, Heidelberg (2002)"},{"key":"25_CR11","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.\u00a02937, pp. 73\u201384. Springer, Heidelberg (2004)"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1080\/01621459.1963.10500830","volume":"58","author":"W. Hoeffding","year":"1963","unstructured":"Hoeffding, W.: Probability inequalities. Journal of the American Statistical Association\u00a058, 13\u201330 (1963)","journal-title":"Journal of the American Statistical Association"},{"key":"25_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"D.N. Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 69\u201385. Springer, Heidelberg (2008)"},{"key":"25_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-31424-7_26","volume-title":"Computer Aided Verification","author":"C. Jegourel","year":"2012","unstructured":"Jegourel, C., Legay, A., Sedwards, S.: Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 327\u2013342. Springer, Heidelberg (2012)"},{"key":"25_CR15","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 \u2013 PLASMA. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol.\u00a07214, pp. 498\u2013503. Springer, Heidelberg (2012)"},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: QEST, pp. 31\u201340. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.25"},{"key":"25_CR17","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker mrmc. In: QEST, pp. 167\u2013176. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"25_CR18","doi-asserted-by":"crossref","unstructured":"Krunz, M., Sass, R., Hughes, H.: Statistical characteristics and multiplexing of MPEG streams. In: INFOCOM, pp. 455\u2013462 (April 1995)","DOI":"10.1109\/INFCOM.1995.515909"},{"issue":"1","key":"25_CR19","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1145\/258623.258688","volume":"25","author":"Marwan Krunz","year":"1997","unstructured":"Krunz, M., Tripathi, S.K.: On the characterization of VBR MPEG streams. In: SIGMETRICS, pp. 192\u2013202 (June 1997)","journal-title":"ACM SIGMETRICS Performance Evaluation Review"},{"key":"25_CR20","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Prism 2.0: A tool for probabilistic model checking. In: QEST, pp. 322\u2013323. IEEE (2004)","DOI":"10.1109\/QEST.2004.1348048"},{"issue":"4","key":"25_CR21","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1145\/1276920.1276922","volume":"8","author":"Sophie 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 TCS\u00a08(4) (2007)","journal-title":"ACM Transactions on Computational Logic"},{"key":"25_CR22","unstructured":"Parzen, E.: Stochastic Processes. Holden Day (1962)"},{"key":"25_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D. Rabih El","year":"2009","unstructured":"El Rabih, D., Pekergin, N.: Statistical Model Checking Using Perfect Simulation. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol.\u00a05799, pp. 120\u2013134. Springer, Heidelberg (2009)"},{"key":"25_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/11817963_25","volume-title":"Computer Aided Verification","author":"G. Ro\u015fu","year":"2006","unstructured":"Ro\u015fu, G., Bensalem, S.: Allen Linear (Interval) Temporal Logic \u2013 Translation to LTL and Monitor Synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 263\u2013277. Springer, Heidelberg (2006)"},{"key":"25_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"issue":"2","key":"25_CR26","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A. Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics\u00a016(2), 117\u2013186 (1945)","journal-title":"Annals of Mathematical Statistics"},{"issue":"2","key":"25_CR27","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/BF00429748","volume":"3","author":"D. Wijesekera","year":"1996","unstructured":"Wijesekera, D., Srivastava, J.: Quality of Service (QoS) Metrics for Continuous Media. Multimedia Tools and Applications\u00a03(2), 127\u2013166 (1996)","journal-title":"Multimedia Tools and Applications"},{"key":"25_CR28","unstructured":"Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. PhD thesis, Carnegie Mellon (2005)"},{"key":"25_CR29","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Baier, C., Clarke, E.M.: Rare-event verification for stochastic hybrid systems. In: HSCC, pp. 217\u2013226. ACM (2012)","DOI":"10.1145\/2185632.2185665"},{"key":"25_CR30","doi-asserted-by":"crossref","unstructured":"Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to simulink\/stateflow verification. In: HSCC, pp. 243\u2013252. ACM (2010)","DOI":"10.21236\/ADA531406"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34026-0_25.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:24:36Z","timestamp":1744205076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34026-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642340253","9783642340260"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34026-0_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}