{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T04:19:36Z","timestamp":1745986776801,"version":"3.40.4"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642357367"},{"type":"electronic","value":"9783642357374"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-35737-4_1","type":"book-chapter","created":{"date-parts":[[2013,1,10]],"date-time":"2013-01-10T01:12:22Z","timestamp":1357780342000},"page":"1-18","source":"Crossref","is-referenced-by-count":2,"title":["Abstraction and Verification of Properties of a Real-Time Java"],"prefix":"10.1007","author":[{"given":"Nadezhda","family":"Baklanova","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Strecker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","unstructured":"Baklanova, N., Strecker, M., F\u00e9raud, L.: Resource sharing conflicts checking in multithreaded Java programs. In: Journ\u00e9es FAC 2012 (2012)"},{"key":"1_CR2","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1016\/j.tcs.2005.11.019","volume":"354","author":"E. Fersman","year":"2006","unstructured":"Fersman, E., Mokrushin, L., Pettersson, P., Yi, W.: Schedulability analysis of fixed-priority systems using timed automata. Theor. Comput. Sci.\u00a0354, 301\u2013317 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR3","unstructured":"B\u00f8gholm, T., Kragh-Hansen, H., Olsen, P.: Model based schedulability analysis of real-time systems. Master\u2019s thesis, Aalborg University (2008)"},{"key":"1_CR4","doi-asserted-by":"crossref","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 (2008)","DOI":"10.1145\/1434790.1434807"},{"issue":"13","key":"1_CR5","doi-asserted-by":"publisher","first-page":"1583","DOI":"10.1002\/cpe.1728","volume":"23","author":"N. Hakimipour","year":"2011","unstructured":"Hakimipour, N., Strooper, P., Wellings, A.: A model-based development approach for the verification of real-time java code. Concurrency and Computation: Practice and Experience\u00a023(13), 1583\u20131606 (2011)","journal-title":"Concurrency and Computation: Practice and Experience"},{"key":"1_CR6","doi-asserted-by":"crossref","unstructured":"Herber, P., Pockrandt, M., Glesner, S.: Transforming systemc transaction level models into uppaal timed automata. In: 2011 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 161\u2013170 (2011)","DOI":"10.1109\/MEMCOD.2011.5970523"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Cordovilla, M., Boniol, F., Noulard, E., Pagetti, C.: Multiprocessor schedulability analyser. In: Chu, W.C., Wong, W.E., Palakal, M.J., Hung, C.C. (eds.) SAC, pp. 735\u2013741. ACM (2011)","DOI":"10.1145\/1982185.1982345"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Ravn, A.P., Schoeberl, M.: Cyclic executive for safety-critical java on chip-multiprocessors. In: Kalibera, T., Vitek, J. (eds.) JTRES. ACM International Conference Proceeding Series, pp. 63\u201369. ACM (2010)","DOI":"10.1145\/1850771.1850779"},{"key":"1_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-642-15769-1_28","volume-title":"Static Analysis","author":"M. Vechev","year":"2010","unstructured":"Vechev, M., Yahav, E., Raman, R., Sarkar, V.: Automatic Verification of Determinism for Structured Parallel Programs. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 455\u2013471. Springer, Heidelberg (2010)"},{"key":"1_CR10","unstructured":"Tofan, B., Schellhorn, G., B\u00e4umler, S., Reif, W.: Embedding rely-guarantee reasoning in temporal logic. Technical Report 2010-07, Informatik (2010)"},{"key":"1_CR11","unstructured":"The Real-Time for Java Expert Group: The Real-Time Specification for Java (2006)"},{"key":"1_CR12","unstructured":"The Open Group JSR: JSR-302 Safety Critical Java Technology Specification (2010), http:\/\/jcp.org\/en\/jsr\/detail?id=308"},{"key":"1_CR13","unstructured":"Henties, T., Hunt, J.J., Locke, D., Nilsen, K., Schoeberl, M., Vitek, J.: Java for safety-critical applications. In: 2nd International Workshop on the Certification of Safety-Critical Software Controlled Systems, SafeCert 2009 (March 2009)"},{"key":"1_CR14","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126, 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","first-page":"87","volume-title":"ACPN 2003","author":"J.E. Bengtsson","year":"2004","unstructured":"Bengtsson, J.E., Yi, W.: Timed Automata: Semantics, Algorithms and Tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) ACPN 2003. LNCS, vol.\u00a03098, pp. 87\u2013124. Springer, Heidelberg (2004), http:\/\/dx.doi.org\/10.1007\/978-3-540-27755-2_3"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, pp. 414\u2013425 (June 1990)","DOI":"10.1109\/LICS.1990.113766"},{"key":"1_CR17","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"issue":"1","key":"1_CR18","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1109\/JPROC.2002.805825","volume":"91","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: a time-triggered language for embedded programming. Proceedings of the IEEE\u00a091(1), 84\u201399 (2003)","journal-title":"Proceedings of the IEEE"}],"container-title":["Communications in Computer and Information Science","ICT in Education, Research, and Industrial Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-35737-4_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,29]],"date-time":"2025-04-29T16:44:13Z","timestamp":1745945053000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-35737-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642357367","9783642357374"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-35737-4_1","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2013]]}}}