{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,1]],"date-time":"2023-05-01T15:26:42Z","timestamp":1682954802113},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2014,7,30]],"date-time":"2014-07-30T00:00:00Z","timestamp":1406678400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2015,4]]},"DOI":"10.1007\/s10009-014-0331-4","type":"journal-article","created":{"date-parts":[[2014,7,29]],"date-time":"2014-07-29T14:31:25Z","timestamp":1406644285000},"page":"187-199","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Schedulability of Herschel revisited using statistical model checking"],"prefix":"10.1007","volume":"17","author":[{"given":"Alexandre","family":"David","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marius","family":"Miku\u010dionis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,7,30]]},"reference":[{"key":"331_CR1","doi-asserted-by":"crossref","first-page":"189","DOI":"10.1023\/A:1008047130023","volume":"15","author":"H Ben-Abdallah","year":"1998","unstructured":"Ben-Abdallah, H., Choi, J.-Y., Clarke, D., Kim, Y.S., Lee, I., Xie, H.-L.: A process algebraic approach to the schedulability analysis of real-time systems. Real-Time Syst. 15, 189\u2013219 (1998). doi: 10.1023\/A:1008047130023","journal-title":"Real-Time Syst."},{"key":"331_CR2","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 1579, pp. 193\u2013207. Springer, Berlin (1999)","DOI":"10.1007\/3-540-49059-0_14"},{"key":"331_CR3","doi-asserted-by":"crossref","unstructured":"Bulychev, P.E., David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Checking and distributing statistical model checking. NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 449\u2013463. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-28891-3_39"},{"key":"331_CR4","unstructured":"Bradley, S., Henderson, W., Kendall, D.: Using timed automata for response time analysis of distributed real-time systems. In: Systems, 24th IFAC\/IFIP Workshop on Real-Time Programming WRTP 99, pp. 143\u2013148 (1999)"},{"key":"331_CR5","unstructured":"Bohnenkamp, H.C., Hermanns, H., Klaren, R., Mader, A., Usenko, Y.S.: Synthesis and stochastic assessment of schedules for lacquer production. In: First International Conference on the Quantitative Evaluation of Systems, 2004. QEST 2004. Proceedings. pp. 28\u201337 (2004)"},{"key":"331_CR6","doi-asserted-by":"crossref","unstructured":"Brekling, A., Hansen, M.R., Madsen, J.: MoVES\u2014a framework for modelling and verifying embedded systems. In: International Conference on Microelectronics (ICM), pp. 149\u2013152 (2009)","DOI":"10.1109\/ICM.2009.5418667"},{"key":"331_CR7","unstructured":"Burns, A.: Preemptive priority based scheduling: an appropriate engineering approach. In: Principles of Real-Time Systems, pp. 225\u2013248. Prentice Hall, Englewood Cliffs (1994)"},{"key":"331_CR8","doi-asserted-by":"crossref","unstructured":"Christensen, S., Kristensen, L., Mailund, T.: A sweep-line method for state space exploration. In: Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2001, pp. 450\u2013464. Springer, London (2001)","DOI":"10.1007\/3-540-45319-9_31"},{"key":"331_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"138","DOI":"10.1007\/3-540-44618-4_12","volume-title":"CONCUR","author":"F Cassez","year":"2000","unstructured":"Cassez, F., Larsen, K.G.: The impressive power of stopwatches. In: Palamidessi, C. (ed.) CONCUR. Lecture Notes in Computer Science, vol. 1877, pp. 138\u2013152. Springer, Berlin (2000)"},{"key":"331_CR10","doi-asserted-by":"crossref","unstructured":"David, A., Illum, J., Larsen, K.G., Skou, A.: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1. In: Nicolescu, G., Mosterman, P.J. (eds.) Model-Based Design for Embedded Systems, pp. 93\u2013119. CRC Press, Boca Raton (2010)","DOI":"10.1201\/9781420067859-c4"},{"key":"331_CR11","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B., Vliet, J.Van, Wang, Z.: Statistical model checking for networks of priced timed automata. FORMATS. LNCS, pp. 80\u201396. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-24310-3_7"},{"key":"331_CR12","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Wang, Z., Miku\u010dionis, M.: Time for real statistical model-checking: Statistical model-checking for real-time systems. In: CAV, LNCS. Springer, Berlin (2011)","DOI":"10.1007\/978-3-642-22110-1_27"},{"key":"331_CR13","doi-asserted-by":"crossref","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M.: Schedulability of Herschel-Planck revisited using statistical model checking. ISoLA (2). LNCS, vol. 7610, pp. 293\u2013307. Springer, Berlin (2012)","DOI":"10.1007\/978-3-642-34032-1_28"},{"issue":"8","key":"331_CR14","doi-asserted-by":"crossref","first-page":"1149","DOI":"10.1016\/j.ic.2007.01.009","volume":"205","author":"E Fersman","year":"2007","unstructured":"Fersman, E., Kr\u010d\u00e1l, P., Pettersson, P., Yi, W.: Task automata: Schedulability, decidability and undecidability. Inf. Comput. 205(8), 1149\u20131172 (2007)","journal-title":"Inf. Comput."},{"key":"331_CR15","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.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 2937, pp. 73\u201384. Springer, Berlin (2004)"},{"key":"331_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1007\/978-3-642-02658-4_52","volume-title":"Computer Aided Verification","author":"B Jeannet","year":"2009","unstructured":"Jeannet, B., Min\u00e9, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 5643, pp. 661\u2013667. Springer, Berlin (2009)"},{"issue":"5","key":"331_CR17","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1093\/comjnl\/29.5.390","volume":"29","author":"M Joseph","year":"1986","unstructured":"Joseph, M., Pandya, P.K.: Finding response times in a real-time system. Comput. J. 29(5), 390\u2013395 (1986)","journal-title":"Comput. J."},{"key":"331_CR18","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: Proc. of 6th Int. Conference on the Quantitative Evaluation of Systems (QEST), pp. 167\u2013176. IEEE Computer Society (2009)","DOI":"10.1109\/QEST.2009.11"},{"key":"331_CR19","doi-asserted-by":"crossref","unstructured":"Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: RV, Lecture Notes in Computer Science, vol. 6418, pp. 122\u2013135. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16612-9_11"},{"key":"331_CR20","doi-asserted-by":"crossref","unstructured":"Miku\u010dionis, M., Larsen, K.G., Rasmussen, J.I., Nielsen, B., Skou, A., Palm, S.U., Pedersen, J.S., Hougaard, P.: Schedulability analysis using Uppaal: Herschel-Planck case study. In: Margaria, T. (ed.) ISoLA 2010\u20134th International Symposium On Leveraging Applications of Formal Methods. Verification and Validation. Lecture Notes in Computer Science. Springer, Berlin (2010)","DOI":"10.1007\/978-3-642-16561-0_21"},{"key":"331_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1007\/978-3-642-04761-9_11","volume-title":"Automated Technology for Verification and Analysis","author":"D Rabih","year":"2009","unstructured":"Rabih, D., Pekergin, N.: Statistical model checking using perfect simulation. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, vol. 5799, pp. 120\u2013134. Springer, Berlin (2009)"},{"key":"331_CR22","unstructured":"Sokolsky, O., Lee, I., Clarke, D.: Schedulability analysis of AADL models. In: 20th International Parallel and Distributed Processing Symposium, 2006. IPDPS 2006, pp. 8 (2006)"},{"key":"331_CR23","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":"331_CR24","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.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 223\u2013235. Springer, Berlin (2002)"},{"key":"331_CR25","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)"}],"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-0331-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-014-0331-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-014-0331-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,13]],"date-time":"2019-08-13T08:55:14Z","timestamp":1565686514000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-014-0331-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7,30]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"alternative-id":["331"],"URL":"https:\/\/doi.org\/10.1007\/s10009-014-0331-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7,30]]}}}