{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T15:36:21Z","timestamp":1762875381847,"version":"3.38.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,5,21]],"date-time":"2011-05-21T00:00:00Z","timestamp":1305936000000},"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":[[2012,2]]},"DOI":"10.1007\/s10009-011-0201-2","type":"journal-article","created":{"date-parts":[[2011,5,19]],"date-time":"2011-05-19T22:07:45Z","timestamp":1305842865000},"page":"53-72","source":"Crossref","is-referenced-by-count":26,"title":["Statistical abstraction and model-checking of large heterogeneous systems"],"prefix":"10.1007","volume":"14","author":[{"given":"Ananda","family":"Basu","sequence":"first","affiliation":[]},{"given":"Saddek","family":"Bensalem","sequence":"additional","affiliation":[]},{"given":"Marius","family":"Bozga","sequence":"additional","affiliation":[]},{"given":"Beno\u00eet","family":"Delahaye","sequence":"additional","affiliation":[]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,5,21]]},"reference":[{"key":"201_CR1","unstructured":"ARINC 664, Aircraft Data Network, Part 7: Avionics Full Duplex Switched Ethernet (AFDX) Network (2005)"},{"key":"201_CR2","unstructured":"II61588: Precision clock synchronization protocol for networked measurement and control systems (2004)"},{"key":"201_CR3","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur R., Dill D.: A theory of timed automata. Theor. Comput. Sci. 126, 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"201_CR4","unstructured":"Basu, A., Bensalem, S., Bozga, M., Delahaye, B., Legay, A., Siffakis, E.: Verification of an afdx infrastructure using simulations and probabilities. In: Proceedings of 1st Conference on Runtime Verification (RV), Malta, 2010. Springer, Berlin (2010)"},{"key":"201_CR5","doi-asserted-by":"crossref","unstructured":"Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time systems in BIP. In: SEFM06, Pune, India. pp. 3\u201312 (2006)","DOI":"10.1109\/SEFM.2006.27"},{"key":"201_CR6","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 2010, pp. 32\u201348. LNCS 6117, Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-13464-7_4"},{"key":"201_CR7","unstructured":"Bensalem, S., Delahaye, B., Legay, A.: Statistical model checking: present and future. In: Proceedings of 1st Conference on Runtime Verification (RV), Malta, 2010. Springer, Berlin (2010)"},{"key":"201_CR8","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-4078-3","volume-title":"Introduction to Rare Event Simulation","author":"J. Bucklew","year":"2004","unstructured":"Bucklew J.: Introduction to Rare Event Simulation. Springer, Berlin (2004)"},{"key":"201_CR9","doi-asserted-by":"crossref","unstructured":"Charara, H., Fraboul, C.: Modelling and simulation of an avionics full duplex switched ethernet. In: Proceedings of the Advanced Industrial Conference on Telecommunications\/Service Assurance with Partial and Intermittent Resources Conference\/E-Learning on Telecommunication Workshop. IEEE (2005)","DOI":"10.1109\/AICT.2005.58"},{"key":"201_CR10","unstructured":"Charara, H., Scharbarg, J.L., Ermont, J., Fraboul, C.: Methods for bounding end-to-end delays on AFDX network. In: ECRTS. IEEE Computer Society (2006)"},{"key":"201_CR11","unstructured":"Clarke, E.M., Donz\u00e9, A., Legay, A.: Statistical model checking of mixed-analog circuits with an application to a third order delta-sigma modulator. In: HVC. LNCS, vol. 5394, pp. 149\u2013163. Springer, Berlin (to appear, 2008)"},{"key":"201_CR12","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Faeder, J.R., Langmead, C.J., Harris, L.A., Jha, S.K., Legay, A.: Statistical model checking in biolab: applications to the automated analysis of t-cell receptor signaling pathway. In: CMSB. LNCS, vol. 5307, pp. 231\u2013250. Springer, Berlin (2008)","DOI":"10.1007\/978-3-540-88562-7_18"},{"key":"201_CR13","doi-asserted-by":"crossref","unstructured":"Efron, B., Tibshirani, R.: An Introduction to the bootstrap. Hall\/CRC Press Monographs on Statistics and Applied Probability (1994)","DOI":"10.1201\/9780429246593"},{"key":"201_CR14","doi-asserted-by":"crossref","unstructured":"Grosu, R., Smolka, S.A.: Monte carlo model checking. In: TACAS. LNCS, vol. 3440, pp. 271\u2013286. Springer, Berlin (2005)","DOI":"10.1007\/978-3-540-31980-1_18"},{"key":"201_CR15","unstructured":"He, R., Jennings, P., Basu, S., Ghosh, A.P., Wu, H.: A bounded statistical approach for model checking of unbounded until properties. In: ASE 2010, 25th IEEE\/ACM International Conference on Automated Software Engineering, Antwerp, Belgium, September 20\u201324, 2010. pp. 225\u2013234. ACM (2010)"},{"key":"201_CR16","doi-asserted-by":"crossref","unstructured":"H\u00e9rault, T., Lassaigne, R., Magniette, F., Peyronnet, S.: Approximate probabilistic model checking. In: VMCAI. LNCS, vol. 2937, pp. 73\u201384. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-24622-0_8"},{"key":"201_CR17","doi-asserted-by":"crossref","first-page":"13","DOI":"10.2307\/2282952","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":"201_CR18","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. LNCS, vol. 4899. Springer, Berlin (2007)"},{"key":"201_CR19","doi-asserted-by":"crossref","unstructured":"Jennings, P., Ghosh, A.P., Basu, S.: A two-phase approximation for model checking probabilistic unbounded until properties of probabilistic systems. ACM Transactions on Software Engineering and Methodology (TOSEM) (2011)","DOI":"10.1145\/2211616.2211621"},{"key":"201_CR20","doi-asserted-by":"crossref","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: CMSB. LNCS, vol. 5688, pp. 218\u2013234. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-03845-7_15"},{"key":"201_CR21","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Zapreev, I.S.: Simulation-based ctmc model checking: An empirical evaluation. In: Proceedings of 6th International Conference on the Quantitative Evaluation of Systems (QEST). pp. 31\u201340. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.25"},{"key":"201_CR22","doi-asserted-by":"crossref","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. Log. 8(4) (2007)","DOI":"10.1145\/1276920.1276922"},{"issue":"2","key":"201_CR23","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1109\/90.298432","volume":"2","author":"A.K. Parekh","year":"1994","unstructured":"Parekh A.K., Gallagher R.G.: A generalized processor sharing approach to flow control in integrated services networks: the multiple node case. IEEE\/ACM Trans. Netw. 2(2), 137\u2013150 (1994)","journal-title":"IEEE\/ACM Trans. Netw."},{"key":"201_CR24","doi-asserted-by":"crossref","unstructured":"Rabih, D.E., Pekergin, N.: Statistical model checking using perfect simulation. In: Proceedings of 7th International Conference on Automated Technology for Verification and Analysis (ATVA). Lecture Notes in Computer Science, vol. 5799, pp. 120\u2013134. Springer, Berlin (2009)","DOI":"10.1007\/978-3-642-04761-9_11"},{"key":"201_CR25","doi-asserted-by":"crossref","unstructured":"Scharbarg, J.L., Fraboul, C.: Simulation for end-to-end delays distribution on a switched ethernet. In: ETFA. IEEE (2007)","DOI":"10.1109\/EFTA.2007.4416904"},{"key":"201_CR26","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: CAV. pp. 202\u2013215. LNCS 3114. Springer, Berlin (2004)","DOI":"10.1007\/978-3-540-27813-9_16"},{"key":"201_CR27","unstructured":"Steinkellner, S., Andersson, H., Lind, I., Krus, P.: Hosted simulation for heterogeneous aircraft system development. In: Proceedings of 26th International Congress of the Aeronautical Sciences (2008)"},{"issue":"2","key":"201_CR28","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."},{"key":"201_CR29","unstructured":"Younes, H.L.S.: Verification and planning for stochastic processes with asynchronous events. Ph.D. thesis, Carnegie Mellon (2005)"},{"key":"201_CR30","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S.: Error control for probabilistic model checking. In: VMCAI. pp. 142\u2013156. LNCS 3855. Springer, Berlin (2006)","DOI":"10.1007\/11609773_10"},{"issue":"3","key":"201_CR31","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H.L.S. Younes","year":"2006","unstructured":"Younes H.L.S., Kwiatkowska M.Z., Norman G., Parker D.: Numerical vs. statistical probabilistic model checking. STTT 8(3), 216\u2013228 (2006)","journal-title":"STTT"},{"issue":"9","key":"201_CR32","doi-asserted-by":"crossref","first-page":"1368","DOI":"10.1016\/j.ic.2006.05.002","volume":"204","author":"H.L.S. Younes","year":"2006","unstructured":"Younes H.L.S., Simmons R.G.: Statistical probabilistic model checking with a focus on time-bounded properties. Inf. Comput. 204(9), 1368\u20131409 (2006)","journal-title":"Inf. Comput."},{"key":"201_CR33","doi-asserted-by":"crossref","unstructured":"Zolotarev, V.M.: One-dimensional stable distribution. American Mathematical Society, Providence (1986)","DOI":"10.1090\/mmono\/065"}],"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-011-0201-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-011-0201-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-011-0201-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,5]],"date-time":"2025-03-05T17:52:02Z","timestamp":1741197122000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-011-0201-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,5,21]]},"references-count":33,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2012,2]]}},"alternative-id":["201"],"URL":"https:\/\/doi.org\/10.1007\/s10009-011-0201-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2011,5,21]]}}}