{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,1]],"date-time":"2026-05-01T11:09:18Z","timestamp":1777633758247,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642165603","type":"print"},{"value":"9783642165610","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-16561-0_21","type":"book-chapter","created":{"date-parts":[[2010,11,2]],"date-time":"2010-11-02T09:50:50Z","timestamp":1288691450000},"page":"175-190","source":"Crossref","is-referenced-by-count":35,"title":["Schedulability Analysis Using Uppaal: Herschel-Planck Case Study"],"prefix":"10.1007","author":[{"given":"Marius","family":"Miku\u010dionis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim Guldstrand","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jacob Illum","family":"Rasmussen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Brian","family":"Nielsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arne","family":"Skou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steen Ulrik","family":"Palm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan Storbank","family":"Pedersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Poul","family":"Hougaard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/3-540-46002-0_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T. Amnell","year":"2002","unstructured":"Amnell, T., Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: TIMES \u2013 a tool for modelling and implementation of embedded systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 460\u2013464. Springer, Heidelberg (2002)"},{"key":"21_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/978-3-540-30080-9_7","volume-title":"Formal Methods for the Design of Real-Time Systems","author":"G. Behrmann","year":"2004","unstructured":"Behrmann, G., David, A., Larsen, K.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol.\u00a03185, pp. 200\u2013236. Springer, Heidelberg (2004)"},{"key":"21_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1007\/978-3-540-73368-3_14","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"2007","unstructured":"Behrmann, G., Cougnard, A., David, A., Fleury, E., Larsen, K.G., Lime, D.: Uppaal-tiga: Time for playing games! In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 121\u2013125. Springer, Heidelberg (2007)"},{"key":"21_CR4","series-title":"ACM International Conference Proceeding Series","doi-asserted-by":"publisher","first-page":"106","DOI":"10.1145\/1434790.1434807","volume-title":"JTRES","author":"T. B\u00f8gholm","year":"2008","unstructured":"B\u00f8gholm, T., Kragh-Hansen, H., Olsen, P., Thomsen, B., Larsen, K.G.: Model-based schedulability analysis of safety critical hard real-time java programs. In: Bollella, G., Locke, C.D. (eds.) JTRES. ACM International Conference Proceeding Series, vol.\u00a0343, pp. 106\u2013114. ACM, New York (2008)"},{"key":"21_CR5","first-page":"225","volume-title":"Principles of Real-Time Systems","author":"A. Burns","year":"1994","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":"21_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1007\/3-540-45319-9_31","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Christensen","year":"2001","unstructured":"Christensen, S., Kristensen, L., Mailund, T.: A Sweep-Line method for state space exploration. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 450\u2013464. Springer, Heidelberg (2001), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/3-540-45319-9_31"},{"key":"21_CR7","first-page":"93","volume-title":"Model-Based Design for Embedded Systems","author":"A. David","year":"2010","unstructured":"David, A., Illum, J., Larsen, K.G., Skou, A.: Model-Based Framework for Schedulability Analysis Using UPPAAL 4.1. In: Model-Based Design for Embedded Systems, pp. 93\u2013119. CRC Press, Boca Raton (2010)"},{"key":"21_CR8","unstructured":"Fersman, E.: A generic approach to schedulability analysis of real-time systems. Acta Universitatis Upsaliensis (2003)"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","first-page":"215","volume-title":"FME 2002: Formal Methods - Getting IT Right","author":"L. Kristensen","year":"2002","unstructured":"Kristensen, L., Mailund, T.: A generalised Sweep-Line method for safety properties. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol.\u00a02391, pp. 215\u2013229. Springer, Heidelberg (2002), \n                    \n                      http:\/\/dx.doi.org\/10.1007\/3-540-45614-7_31"},{"key":"21_CR10","unstructured":"Palm, S.: Herschel-Planck ACC ASW: sizing, timing and schedulability analysis. Tech. rep., Terma A\/S (2006)"},{"key":"21_CR11","unstructured":"Terma A\/S: Herschel-Planck ACMS ACC ASW requirements specification. Tech. rep., Terma A\/S (Issue 4\/0)"},{"key":"21_CR12","unstructured":"Terma A\/S: Software timing and sizing budgets. Tech. rep., Terma A\/S (Issue 9)"},{"issue":"1","key":"21_CR13","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/s11241-007-9036-z","volume":"38","author":"L. Waszniowski","year":"2008","unstructured":"Waszniowski, L., Hanz\u00e1lek, Z.: Formal verification of multitasking applications based on timed automata model. Real-Time Systems\u00a038(1), 39\u201365 (2008)","journal-title":"Real-Time Systems"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification, and Validation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-16561-0_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,21]],"date-time":"2019-03-21T20:45:43Z","timestamp":1553201143000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-16561-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642165603","9783642165610"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-16561-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}