{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:21:02Z","timestamp":1759033262918,"version":"3.40.4"},"reference-count":48,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,3,30]],"date-time":"2014-03-30T00:00:00Z","timestamp":1396137600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10009-014-0313-6","type":"journal-article","created":{"date-parts":[[2014,3,29]],"date-time":"2014-03-29T14:51:45Z","timestamp":1396104705000},"page":"171-185","source":"Crossref","is-referenced-by-count":27,"title":["Statistical model checking QoS properties of systems with SBIP"],"prefix":"10.1007","volume":"17","author":[{"given":"Ayoub","family":"Nouri","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","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":[]}],"member":"297","published-online":{"date-parts":[[2014,3,30]]},"reference":[{"key":"313_CR1","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Caillaud, B., Delahaye, B., Legay, A.: Statistical abstraction and model-checking of large heterogeneous systems. In: FORTE, vol 6117 of LNCS, pp. 32\u201346. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"313_CR2","doi-asserted-by":"crossref","unstructured":"Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Sifakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: Proceedings of the First international conference on Runtime verification, RV\u201910, pp. 330\u2013344. Springer-Verlag, Berlin, Heidelberg (2010)","DOI":"10.1007\/978-3-642-16612-9_25"},{"key":"313_CR3","unstructured":"Basu, A., Bensalem, S., Gallien, M., Ingrand, F., Lesire, C., Nguyen, T.-H., Sifakis, J.: Incremental component-based construction and verification of a robotic system, In: ECAI (2008)"},{"key":"313_CR4","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling Heterogeneous Real-time Systems in BIP. In: SEFM06, pp. 3\u201312, Sep (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"313_CR5","first-page":"327","volume":"1","author":"S Bensalem","year":"2012","unstructured":"Bensalem, S., Bozga, M., Delahaye, B., J\u00e9gourel, C., Legay, A., Nouri, A.: Statistical model checking qos properties of systems with sbip. ISoLA 1, 327\u2013341 (2012)","journal-title":"ISoLA"},{"key":"313_CR6","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-finder: A tool for compositional deadlock detection and verification. In: Proceedings of the 21st International Conference on Computer Aided Verification, CAV \u201909, pp. 614\u2013619. Springer-Verlag, Berlin, Heidelberg (2009)","DOI":"10.1007\/978-3-642-02658-4_45"},{"key":"313_CR7","unstructured":"Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: Present and future. In: RV, vol. 6418 of LNCS. Springer, Berlin (2010)"},{"key":"313_CR8","unstructured":"Bensalem, S., Legay, A., Nouri, A., Peled, D.: Synthesizing distributed scheduling implementation for probabilistic component-based systems. In: MEMOCODE, pp. 87\u201396 (2013)"},{"key":"313_CR9","doi-asserted-by":"crossref","unstructured":"Bensalem, S., Silva, L., Griesmayer, A., Ingrand, F., Legay, A., Yan, R.: A formal approach for incremental construction with an application to autonomous robotic systems. In: SC\u201911, LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22045-6_8"},{"key":"313_CR10","unstructured":"Bip tools. http:\/\/www-verimag.imag.fr\/BIP-Tools,93.html"},{"key":"313_CR11","unstructured":"Bip2 language. http:\/\/www-verimag.imag.fr\/TOOLS\/DCS\/bip\/doc\/latest\/html\/"},{"key":"313_CR12","unstructured":"Bliudze, S., Sifakis, J.: The algebra of connectors-structuring interaction in bip. IEEE Trans. Comput. 57(10), 1315\u20131330 (2008)"},{"key":"313_CR13","doi-asserted-by":"crossref","unstructured":"Bogdoll, J., Fiorti, L.-M., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: FORTE, LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-21461-5_4"},{"key":"313_CR14","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"313_CR15","doi-asserted-by":"crossref","unstructured":"Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems. In: SEFM, pp. 204\u2013220 (2011)","DOI":"10.1007\/978-3-642-24690-6_15"},{"issue":"2","key":"313_CR16","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1023\/B:FORM.0000017718.28096.48","volume":"24","author":"B Finkbeiner","year":"2004","unstructured":"Finkbeiner, B., Sipma, H.: Checking finite traces using alternating automata. Form. Methods Syst. Des. 24(2), 101\u2013127 (2004)","journal-title":"Form. Methods Syst. Des."},{"key":"313_CR17","first-page":"53","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901). Lecture Notes in Computer Science, vol. 2102","author":"P Gastin","year":"2001","unstructured":"Gastin, P., Oddoux, D.: Fast LTL to B\u00fcchi automata translation. In: Berry, G., Comon, H., Finkel, A. (eds.) Proceedings of the 13th International Conference on Computer Aided Verification (CAV\u201901). Lecture Notes in Computer Science, vol. 2102, pp. 53\u201365. Springer, Paris (2001)"},{"key":"313_CR18","unstructured":"Giannakopoulou, D., Havelund, K.: Automata-based verification of temporal properties on running programs. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, ASE \u201901, pp. 412. IEEE Computer Society, Washington, DC (2001)"},{"key":"313_CR19","doi-asserted-by":"crossref","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: TACAS, vol. 3440 of LNCS, pp. 271\u2013286. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"313_CR20","doi-asserted-by":"crossref","unstructured":"Havelund, K., Rosu, G.: Synthesizing monitors for safety properties. In: TACAS, LNCS, pp. 342\u2013356. Springer, Berlin (2002)","DOI":"10.1007\/3-540-46002-0_24"},{"key":"313_CR21","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI, pp. 73\u201384 (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"313_CR22","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. J. Am. Stat. Assoc. 58, 13\u201330 (1963)","journal-title":"J. Am. Stat. Assoc."},{"key":"313_CR23","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: HVC, vol. 4899 of LNCS. Springer, Berlin (2007)"},{"key":"313_CR24","doi-asserted-by":"crossref","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: Cross entropy optimisation of importance sampling parameters for statistical model checking. In: CAV (2012)","DOI":"10.1007\/978-3-642-31424-7_26"},{"key":"313_CR25","doi-asserted-by":"crossref","unstructured":"J\u00e9gourel, C., Legay, A., Sedwards, S.: A platform for high performance statistical model checking-plasma. In: TACAS, LNCS, pp. 498\u2013503. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28756-5_37"},{"key":"313_CR26","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, Washington, DC (2009)","DOI":"10.1109\/QEST.2009.25"},{"key":"313_CR27","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, Washington, DC (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"313_CR28","doi-asserted-by":"crossref","unstructured":"Krunz, M., Sass, R., Hughes, H.: Statistical characteristics and multiplexing of MPEG streams. In: INFOCOM, pp. 455\u2013462 (1995)","DOI":"10.1109\/INFCOM.1995.515909"},{"key":"313_CR29","doi-asserted-by":"crossref","unstructured":"Krunz, M., Tripathi, S.K.: On the characterization of VBR MPEG streams. In: SIGMETRICS, pp. 192\u2013202 (1997)","DOI":"10.1145\/258623.258688"},{"key":"313_CR30","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":"313_CR31","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 TCS 8(4), 20 (2007)","journal-title":"ACM TCS"},{"key":"313_CR32","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B.: Statistical model checking: an overview. CoRR, abs\/1005.1327 (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"313_CR33","unstructured":"Nouri, A., Legay, A., Bensalem, S., Bozga, M.: Sbip: a statistical model checking extension for the bip framework. In: First Workshop on Statistical Model Checking (2013)"},{"key":"313_CR34","volume-title":"Stochastic Processes","author":"E Parzen","year":"1962","unstructured":"Parzen, E.: Stochastic Processes. Holden Day, Australia (1962)"},{"key":"313_CR35","doi-asserted-by":"crossref","unstructured":"Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: ATVA, vol. 5799 of LNCS, pp. 120\u2013134. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04761-9_11"},{"key":"313_CR36","doi-asserted-by":"crossref","unstructured":"Raman, B., Nouri, A., Gangadharan, D., Bozga, M., Basu, A., Maheshwari, M., Legay, A., Bensalem, S., Chakraborty, S.: Stochastic modeling and performance analysis of multimedia socs. In: ICSAMOS, pp. 145\u2013154 (2013)","DOI":"10.1109\/SAMOS.2013.6621117"},{"key":"313_CR37","doi-asserted-by":"crossref","unstructured":"Rosu, G., Bensalem, S.: Allen linear (interval) temporal logic: translation to ltl and monitor synthesis. In: CAV, vol. 4144 of LNCS, pp. 263\u2013277. Springer, Berlin (2006)","DOI":"10.1007\/11817963_25"},{"key":"313_CR38","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV, LNCS 3114, pp. 202\u2013215. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"313_CR39","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: On statistical model checking of stochastic systems. In: CAV, pp. 266\u2013280 (2005)","DOI":"10.1007\/11513988_26"},{"key":"313_CR40","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Alternating automata and program verification. In: In Computer Science Today. LNCS 1000, pp. 471\u2013485. Springer-Verlag, Berlin (1995)","DOI":"10.1007\/BFb0015261"},{"issue":"2","key":"313_CR41","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Ann. Math. Stat. 16(2), 117\u2013186 (1945)","journal-title":"Ann. Math. Stat."},{"issue":"2","key":"313_CR42","doi-asserted-by":"crossref","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 Appl. 3(2), 127\u2013166 (1996)","journal-title":"Multimedia Tools Appl."},{"key":"313_CR43","doi-asserted-by":"crossref","unstructured":"Wolper, P.: Lectures on formal methods and performance analysis. Chapter Constructing automata from temporal logic formulas: a tutorial, pp. 261\u2013277. Springer-Verlag New York Inc, New York (2002)","DOI":"10.1007\/3-540-44667-2_7"},{"key":"313_CR44","unstructured":"Ylies, F., Mohamad, J., Thanh-Hung, N., Marius, B., Saddek, B.: Runtime verification of component-based systems in the bip framework with formally-proved sound and complete instrumentation. SOSYM, pp. 1\u201327 (2013)"},{"key":"313_CR45","unstructured":"Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D thesis, Carnegie Mellon (2005)"},{"key":"313_CR46","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S., Clarke, E.M., Zuliani, P.: Statistical verification of probabilistic properties with unbounded until. In: SBMF, pp. 144\u2013160 (2010)","DOI":"10.1007\/978-3-642-19829-8_10"},{"key":"313_CR47","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":"313_CR48","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":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0313-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0313-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0313-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,2]],"date-time":"2025-05-02T06:12:59Z","timestamp":1746166379000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0313-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,3,30]]},"references-count":48,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["313"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0313-6","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2014,3,30]]}}}